Retained memory and pending children after a native emission

The actual pointer-table store is below the fresh heap and outside every live input block. These frame lemmas retain old arrays and controller parameters, and identify the three actual compact heavy buffers with the existing finite recursion's children.

Main results

• Emission.controls, Emission.loaded: retained caller registers and current entry.
• Emission.stored: preservation of any live array around the reserved gap.
• Emission.children_tasks: the exact ordered mathematical worklist after child pushes.

These memory-frame and representation proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.prefix_preserved {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (p : ℕ) (hp : p < x.regs heap) (hne : p ≠ x.regs outputs + x.regs outputCount) : y.mem p = x.mem p

An actual emission preserves each old-prefix cell except its one explicit table store.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.controls {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) {a : Arena} (hc : a.Controls x) : a.Controls y

All persistent caller parameters survive the actual complete visit.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.loaded {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (hl : e.Loaded x) : e.Loaded y

The current root record survives the visit until the actual child-preparation instructions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.stored {Q : Finset ℕ} {Λ : ℕ} {e d : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) {a : Arena} (ha : a.Separated) (hc : a.Controls x) (hs : d.Stored x.mem) (hg : d.Around a.stack (a.floor - a.stack)) (hend : ∀ (j : Fin 3), d.source j + (d.data j).length ≤ x.regs heap) (htable : x.regs outputs + x.regs outputCount < a.floor) : d.Stored y.mem

Old input columns below the stack or above the output table cannot be overwritten by the single native pointer store, and both actual kernels preserve the old prefix.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) : List Entry

Top-first native child entries with the three actual compact heavy buffers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_tasks {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) : List.map Entry.task h.children = Math.Task.children Q Λ (e.fuel - 1) e.task

Actual heavy-buffer readback represents exactly the existing ordered three-child recursion.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_valid {Q : Finset ℕ} {Λ n U : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (hv : e.Valid n U) (d : Entry) : d ∈ h.children → d.Valid n U

Each of the actual three heavy-child arrays retains the existing admissibility promises.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_stored {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (hs : e.Stored y.mem) (d : Entry) : d ∈ h.children → d.Stored y.mem

Each child reuses the two surviving original columns and one actual compact heavy buffer.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.heap_mono {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) : x.regs heap ≤ y.regs heap

The actual heap pointer advances past the old frontier.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_ends {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (hl : e.Loaded x) (hend : ∀ (j : Fin 3), e.source j + (e.data j).length ≤ x.regs heap) (d : Entry) : d ∈ h.children → ∀ (k : Fin 3), d.source k + (d.data k).length ≤ y.regs heap

Every actual child column lies below the advanced native allocation frontier.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_around {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) {base capacity : ℕ} (hg : e.Around base capacity) (hfloor : base + capacity ≤ x.regs heap) (d : Entry) : d ∈ h.children → d.Around base capacity

Every new heavy child begins above the reserved stack/table gap.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.children_words {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (hl : e.Loaded x) : childWords y 0 ++ childWords y 1 ++ childWords y 2 = List.flatMap Entry.words h.children

The exact native words prepared for the three pushes are the new semantic child records.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.stack {Q : Finset ℕ} {Λ w : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) {a : Arena} (ha : a.Separated) (hc : a.Controls x) (hy : WordRAM.Data.Bounded w y) (vs : List ℕ) (hr : WordRAM.Stack.Rep w a.stack a.capacity vs (WordRAM.Data.comap Traversal.registers x)) (htable : x.regs outputs + x.regs outputCount < x.regs heap) : WordRAM.Stack.Rep w a.stack a.capacity vs (WordRAM.Data.comap Traversal.registers y)

The complete visit retains the actual pending stack, including its native pointer and length registers; its sole external memory store lies above the stack reservation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.output {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) {a : Arena} (hc : a.Controls x) (ns : List (ℕ × ThreeSum.ChanHe.Node)) (hs : StoredNodes a.U a.N a.table ns x.mem) (hcount : x.regs outputCount = ns.length) (hbounds : ∀ (i : Fin ns.length), a.floor ≤ ns[↑i].1 ∧ ns[↑i].1 + 4 * a.N ≤ x.regs heap) (htable : a.table + ns.length < a.floor) (hfloor : a.floor ≤ x.regs heap) : StoredNodes a.U a.N a.table (ns ++ [((recordLayout x h.M).packed, Math.Task.node Q Λ e.task)]) y.mem

Append the actual newly emitted packed pointer and array to the retained output sequence.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission.math_step {Q : Finset ℕ} {Λ : ℕ} {e : Entry} {x y : WordRAM.Data 128} (h : Emission Q Λ e x y) (es : List Entry) (hf : e.fuel ≠ 0) (hn : ∀ (j : Fin 3), (e.data j).length ≠ 0) : Math.step Q Λ e.task (List.map Entry.task es) = (List.map Entry.task (h.children ++ es), some (Math.Task.node Q Λ e.task))

For a live entry, the actual heavy children and emitted node are the exact finite step.