Exact native frontend entries for Chan–He traversal

The semantic entries use the actual frontend payload bases and decoded compact lists. Native readback follows from the frontend's canonical encoding theorem. Their output is exactly the existing finite Chan–He node list; no new 3SUM predicate or padded input is introduced.

Main definitions

• entry, entries: semantic records of the actual six-word frontend descriptors.

Main results

• entry_stored: exact signed-encoded payload readback.
• entry_valid, entry_ends: admissibility and containment in the concrete frontend allocation.
• entries_output: exact equality with the existing finite node list, in order.

These native representation bridges are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry (l : Frontend.Layout) (U f : ℕ) (rs : List (ℕ × ℕ)) (t : ℕ) : Traversal.Entry

One actual frontend descriptor, with the shared runtime fuel and concrete payload bases.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entries (l : Frontend.Layout) (U : ℕ) (rs : List (ℕ × ℕ)) : List Traversal.Entry

All actual frontend roots in their existing enumeration order.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry_slot {l : Frontend.Layout} {t : ℕ} (ht : t < l.count) (j : Fin 3) : 3 * t + ↑j < l.arrays

Each concrete root column is a valid physical frontend slot.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry_length_le (l : Frontend.Layout) (U f : ℕ) (rs : List (ℕ × ℕ)) (hcard : rs.length ≤ l.n) (t : ℕ) (j : Fin 3) : ((entry l U f rs t).data j).length ≤ l.n + 1

A root column occupies at most its actual n+1-word payload capacity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry_stored {input : List ℤ} {rs : List (ℕ × ℕ)} {l : Frontend.Layout} {U f t : ℕ} {mem : ℕ → ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (h : Frontend.Output l U rs mem) (ht : t < l.count) : (entry l U f rs t).Stored mem

The actual native frontend payload is exactly the signed encoding expected by traversal.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry_valid {input : List ℤ} {rs : List (ℕ × ℕ)} (l : Frontend.Layout) (U f t : ℕ) (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hnd : (List.map Prod.fst rs).Nodup) (hcard : rs.length ≤ l.n) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) : (entry l U f rs t).Valid (l.n + 1) (2 * U)

Frontend roots satisfy the existing admissibility notion, including singleton zero at n=0.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entry_ends (l : Frontend.Layout) (U f : ℕ) (rs : List (ℕ × ℕ)) (hcard : rs.length ≤ l.n) {t : ℕ} (ht : t < l.count) (j : Fin 3) : (entry l U f rs t).source j + ((entry l U f rs t).data j).length ≤ l.endpoint

Every actual root payload ends inside the frontend's concrete allocation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.entries_output {input : List ℤ} {rs : List (ℕ × ℕ)} {U : ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) : have l := { n := input.length, digits := ThreeSum.labelBits (2 * U) }; Traversal.Math.output (ThreeSum.ChanHe.mPar input.length (2 * U)).primesLE l.digits (List.map Traversal.Entry.task (entries l U rs)) = ThreeSum.ChanHe.allNodes input.length U fun (i : Fin input.length) => input[i]

Traversing these exact entries produces precisely the unchanged finite Chan–He node list.