Complete native Chan–He preprocessing from initialized input

Every parameter, sorted multiplicity table, frontend descriptor, prime bit, heavy list and packed output is computed by one finite native program for the fixed magnitude exponent. The output list is exactly the existing finite instances, including negative and small-input cases.

Main definitions

• cost: charged complete-program bound, including the final halt.

Main results

• exec_input: complete actual native execution and exact finite packed output.
• runs_input: native halting execution and the same actual pre-halt memory witness.

These initialized-input composition proofs are original; existing finite reduction mathematics, native kernels and native compilation APIs are reused without an algorithm or operation oracle.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.cost (κ n : ℕ) : ℕ

All actual native instructions, including the complete initialized frontend and final halt.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.exec_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : let n := input.length; have U := (n + 2) ^ κ; have m := ThreeSum.ChanHe.mPar n (2 * U); ∃ (out : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128), WordRAM.ExecWithin w (program κ) (WordRAM.Data.init (List.map WordRAM.Signed.encode input)) y (cost κ n - 1) ∧ (List.map (fun (p : ℕ × ThreeSum.ChanHe.Node) => p.2.oneArray (2 * U)) out = ThreeSum.ChanHe.instances n U fun (i : Fin n) => input[i]) ∧ Traversal.StoredNodes (2 * U) (2 * m ^ 2) (arena κ n y.mem).table out y.mem ∧ y.regs Traversal.outputCount = out.length ∧ y.regs Traversal.outputs = (arena κ n y.mem).table ∧ y.regs packedLength = 8 * m ^ 2

Complete actual native preprocessing, uniformly over every admitted sufficiently wide input.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.runs_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : let n := input.length; have U := (n + 2) ^ κ; have m := ThreeSum.ChanHe.mPar n (2 * U); ∃ (out : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128) (steps : ℕ), WordRAM.Executes w (flatProgram κ) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) out.length steps ∧ WordRAM.Runs w (flatProgram κ) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := (program κ).size, data := y } (steps - 1) ∧ steps ≤ cost κ n ∧ (List.map (fun (p : ℕ × ThreeSum.ChanHe.Node) => p.2.oneArray (2 * U)) out = ThreeSum.ChanHe.instances n U fun (i : Fin n) => input[i]) ∧ Traversal.StoredNodes (2 * U) (2 * m ^ 2) (arena κ n y.mem).table out y.mem ∧ y.regs Traversal.outputCount = out.length ∧ y.regs Traversal.outputs = (arena κ n y.mem).table ∧ y.regs packedLength = 8 * m ^ 2 ∧ WordRAM.Data.Bounded w y

The native flat program halts, and its actual pre-halt state retains the exact output.