Semantic entries of the native Chan–He work stack

An entry pairs the seven unsigned stack words with the three signed integer lists stored at their bases. Memory readback reuses Block.Realizes; set contents use List.toFinset; and the mathematical task is the existing Chan–He recursion. This is a proof invariant for native code, not an additional machine or execution semantics.

Main definitions

• Entry: fuel, three native bases and their represented integer lists.
• Entry.words, Entry.task: native serialization and the existing mathematical task.
• Entry.Stored, Entry.Loaded: block readback and the current record's register ABI.

Main results

• Entry.image_read: the injective-array API represents exactly the listed finite set.
• Entry.read_injOn: duplicate-free lists meet the actual modulus/node call premise.
• Entry.Stored.input: exact signed-encoded native array readback.
• Entry.loaded_words: the seven register words match the pending entry's serialization.

The native worklist invariants and composition proofs are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry : Type

One pending native record and the integer arrays represented by its pointers and lengths.

• fuel : ℕ

  Remaining recursion levels.

• source : Fin 3 → ℕ

  The three data bases.

• data : Fin 3 → List ℤ

  The lists stored at those bases, in their actual enumeration order.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.words (e : Entry) : List ℕ

Seven unsigned stack words in the exact native pop order.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.task (e : Entry) : Math.Task

The unchanged finite recursion task represented by an entry.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.read (e : Entry) (j : Fin 3) (i : ℕ) : ℤ

Total extension of the compact list for the existing native array APIs.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored (e : Entry) (mem : ℕ → ℕ) : Prop

Each signed-encoded list occupies its concrete block, using the generic memory API.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Loaded (e : Entry) (x : WordRAM.Data 128) : Prop

The current seven record registers contain this entry's actual unsigned metadata.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.child (e : Entry) (j : Fin 3) (base : ℕ) (zs : List ℤ) : Entry

Replace exactly one column by its actual compact heavy list and decrease the fuel.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.length_words (e : Entry) : e.words.length = 7

A pending entry always occupies seven physical stack cells, including empty arrays.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.read_eq (e : Entry) (j : Fin 3) (i : ℕ) (hi : i < (e.data j).length) : e.read j i = (e.data j)[i]

Inside its valid range the total read function is the actual list element.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.image_read (e : Entry) (j : Fin 3) : Finset.image (e.read j) (Finset.range (e.data j).length) = (e.data j).toFinset

The finite-set input of each existing array kernel is exactly the entry's listed set.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.read_injOn (e : Entry) (j : Fin 3) (h : (e.data j).Nodup) : Set.InjOn (e.read j) ↑(Finset.range (e.data j).length)

A duplicate-free compact list meets the actual native collision-counting premise.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored.input {e : Entry} {mem : ℕ → ℕ} (h : e.Stored mem) (j : Fin 3) (i : ℕ) (hi : i < (e.data j).length) : mem (e.source j + i) = WordRAM.Signed.encode (e.read j i)

Exact readback in the native array-call format, derived from the generic block realization.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored.congr {e : Entry} {before after : ℕ → ℕ} (h : e.Stored before) (hf : ∀ (j : Fin 3), ∀ i < (e.data j).length, after (e.source j + i) = before (e.source j + i)) : e.Stored after

Readback transfers along a memory equality on the three live blocks.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored.of_prefix {e : Entry} {before after : ℕ → ℕ} (h : e.Stored before) {frontier : ℕ} (hsrc : ∀ (j : Fin 3), e.source j + (e.data j).length ≤ frontier) (hf : ∀ a < frontier, after a = before a) : e.Stored after

A prefix frame preserves every pending list whose block ends before the fresh allocation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.loaded_words {e : Entry} {x : WordRAM.Data 128} (h : e.Loaded x) : [x.regs (slot 0), x.regs (slot 1), x.regs (slot 2), x.regs (slot 3), x.regs (slot 4), x.regs (slot 5), x.regs (slot 6)] = e.words

The seven actual register words match the exact work-stack serialization.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.task_child (e : Entry) (j : Fin 3) (base : ℕ) (zs : List ℤ) : (e.child j base zs).task = { fuel := e.fuel - 1, sets := Function.update e.task.sets j zs.toFinset }

Replacing a native column changes exactly the corresponding mathematical set.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.child_words {e : Entry} {x : WordRAM.Data 128} (h : e.Loaded x) (bases : Fin 3 → ℕ) (zs : Fin 3 → List ℤ) (hb : ∀ (j : Fin 3), x.regs (heavyBase j) = bases j) (hn : ∀ (j : Fin 3), x.regs (heavyLength j) = (zs j).length) (j : Fin 3) : childWords x j = (e.child j (bases j) (zs j)).words

The native child-record words represent exactly the changed data block, with the two other columns and their original enumeration orders preserved.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Valid (e : Entry) (n U : ℕ) : Prop

The size and magnitude assumptions are the existing finite three-set admissibility notion; duplicate-free enumeration is the additional native-array obligation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Valid.length_le {e : Entry} {n U : ℕ} (h : e.Valid n U) (j : Fin 3) : (e.data j).length ≤ n

Native input lengths equal finite-set cardinalities under the duplicate-free obligation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Valid.natAbs_le {e : Entry} {n U : ℕ} (h : e.Valid n U) (j : Fin 3) (i : ℕ) (hi : i < (e.data j).length) : (e.read j i).natAbs ≤ U

The existing finite-set magnitude promise bounds every actual native array element.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Valid.child {e : Entry} {n U : ℕ} (h : e.Valid n U) (j : Fin 3) (base : ℕ) (zs : List ℤ) (hnd : zs.Nodup) (hsub : zs.toFinset ⊆ (e.data j).toFinset) : (e.child j base zs).Valid n U

Replacing a column by a duplicate-free subset preserves the existing size/magnitude promises.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored.child {e : Entry} {mem : ℕ → ℕ} (h : e.Stored mem) (j : Fin 3) (base : ℕ) (zs : List ℤ) (hz : { base := base, length := zs.length }.Realizes mem fun (i : Fin { base := base, length := zs.length }.length) => WordRAM.Signed.encode zs[↑i]) : (e.child j base zs).Stored mem

A child reuses both untouched data blocks and the actual newly written heavy block.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.task_children (e : Entry) (Q : Finset ℕ) (Λ : ℕ) (bases : Fin 3 → ℕ) (zs : Fin 3 → List ℤ) (hz : ∀ (j : Fin 3), (zs j).toFinset = ThreeSum.ChanHe.heavy (e.task.sets j) (Math.Task.node Q Λ e.task).M) : [(e.child 0 (bases 0) (zs 0)).task, (e.child 1 (bases 1) (zs 1)).task, (e.child 2 (bases 2) (zs 2)).task] = Math.Task.children Q Λ (e.fuel - 1) e.task

Actual heavy lists and bases give exactly the existing ordered three-child worklist.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.length_serialized (es : List Entry) : (List.flatMap Entry.words es).length = 7 * es.length

The native word-stack length records exactly seven cells per pending entry.