Complete native Chan–He traversal from a supplied root

The finite 128-register program initializes its actual stack and constants, pushes the supplied seven-word root and executes the complete bounded traversal. Every emitted array is the existing finite node's oneArray, in preorder. The protected frontend prefix survives for later roots.

Main definitions

• RootInput: concrete native array, metadata and disjoint-memory obligations of a root call.

Main results

• root_exec: complete actual native execution with exact output and a charged bound.

These native composition proofs are original. The initialized-input forest and global logarithmic-width/subquadratic-cost composition remain separate obligations.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.RootInput (a : Arena) (w : ℕ) (e : Entry) (ns : List (ℕ × ThreeSum.ChanHe.Node)) (x : WordRAM.Data 128) : Prop

Concrete caller obligations before the complete native root program initializes its stack.

• bounded : WordRAM.Data.Bounded (w + 2) x

  Initial actual words fit.

• controls : a.Controls x

  Persistent caller metadata.

• loaded : e.Loaded x

  Exact root register metadata.

• stored : e.Stored x.mem

  Exact root data readback.

• valid : e.Valid a.n a.U

  Duplicate-free existing three-set admissibility.

• bitmap : a.Bitmap x.mem

  The actual prime bitmap is ready.

• around : e.Around a.stack (a.floor - a.stack)

  Original arrays avoid the complete reserved stack and output-table gap.

• ends (j : Fin 3) : e.source j + (e.data j).length ≤ x.regs heap

  All root arrays end below the fresh allocation.

• fuel : e.fuel = a.fuel

  The supplied fuel agrees with the fixed stack reservation.

• floor : a.floor ≤ x.regs heap

  The initial fresh allocation lies above the reserved gap.

• heapBudget : x.regs heap + Math.work e.fuel * allocationSize a.n a.m a.N ≤ a.ceiling

  The full tree's transitions reserve sufficient fresh memory.

• count : x.regs outputCount = ns.length

  Actual accumulated output count.

• tableBudget : ns.length + Math.work e.fuel ≤ a.outputCapacity

  The full tree's transitions reserve sufficient output-pointer cells.

• output : StoredNodes a.U a.N a.table ns x.mem

  Existing output retains its exact native readback.

• outputBounds (i : Fin ns.length) : a.floor ≤ ns[↑i].1 ∧ ns[↑i].1 + 4 * a.N ≤ x.regs heap

  Existing packed arrays lie above the gap and below the fresh allocation.

• protectedMemory (p : ℕ) : p < a.stack → x.mem p = a.retained p

  The entire frontend prefix is available.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.root_exec {a : Arena} {w : ℕ} (e : Entry) (ns : List (ℕ × ThreeSum.ChanHe.Node)) (x : WordRAM.Data 128) (ha : a.Separated) (hw : a.Ready w) (h : RootInput a w e ns x) : ∃ (out : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) oneRoot x y (rootTime e.fuel a.n a.m a.N) ∧ Cursor.Invariant a w (List.map Prod.snd ns ++ Math.Task.output a.m.primesLE a.Λ e.task) { pending := [], emitted := out } y ∧ List.map Prod.snd out = List.map Prod.snd ns ++ Math.Task.output a.m.primesLE a.Λ e.task ∧ (∀ p < a.stack, y.mem p = x.mem p) ∧ ∀ (i : Fin 128), 109 ≤ ↑i → y.regs i = x.regs i

Execute the fixed complete native root program. There are no supplied kernel executions: all calls are proved from the actual arrays, bitmap, finite bounds and one signed envelope. The caller chooses m, Λ and fuel. Setting m = mPar n U, Λ = labelBits U and e.fuel = fuel n makes e.task.output (Nat.primesLE a.m) a.Λ the existing Chan–He reduction n U of the root sets; the initialized-input bridge is in PreprocessingEntries.