Complete native distinct-position 3SUM frontend

One finite 128-register program per fixed exponent starts from ordinary native initialized signed input. It computes (n+2)^κ, sorts with an explicit magnitude-derived bit count, retains full multiplicities, and writes six-word descriptors of compact injective arrays. Reading the descriptors gives exactly the existing ThreeSum.inputs, in its existing order, including empty arrays and the two multiplicity triples at lengths zero, one and two.

The mathematical definitions are reused from the frontend adaptation of anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, PaperStatements.lean lines 1358–1376. In particular twiceSet contains positive 2*a. Native programs, layout and charged proofs here are original; no source machine is imported. This is the frontend component, not complete Chan–He preprocessing or a subquadratic solver.

Main definitions

• program: native code depending only on the fixed polynomial exponent.
• layout: six-word descriptors followed by disjoint capacity-n+1 payload blocks.
• width, cost: derived positive logarithmic width and all charged instructions.

Main results

• exec_input: initialized-input execution, exact slots/frame and full multiplicities.
• runs_input: exact existing-root readback and complete native halting execution.
• cost_bound: explicit uniform logarithmic-square instruction bound.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.not_readsWidth (κ : ℕ) : ¬(program κ).ReadsWidth

Physical word width is never read, so it never determines the radix iteration count.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.size_program (κ : ℕ) : (program κ).size = κ + 71 + construct.size

Code size depends only on the fixed exponent; the assembled final halt adds one.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.runs_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : ∃ (y : WordRAM.Data 128) (steps : ℕ), WordRAM.Executes w ((program κ).program descriptorCount) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) (layout κ input.length).count steps ∧ WordRAM.Runs w ((program κ).program descriptorCount) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := (program κ).size, data := y } (steps - 1) ∧ steps ≤ cost κ input.length ∧ (readRoots (layout κ input.length) y.mem = ThreeSum.inputs ((input.length + 2) ^ κ) fun (i : Fin input.length) => input[i]) ∧ y.regs descriptorBase = (layout κ input.length).descriptors ∧ y.regs descriptorCount = (layout κ input.length).count ∧ y.regs heapEnd = (layout κ input.length).endpoint ∧ WordRAM.Data.Bounded w y

The complete finite program halts with its descriptor count, and following its descriptors gives exactly the existing frontend list. The memory witness is the actual native state just before the final halt. No slot, bit budget, sorting result or fit is advice.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.intermediates_polynomial {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State 128} {steps : ℕ} (hr : WordRAM.Runs w ((program κ).program descriptorCount) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s steps) : (∀ (i : Fin 128), s.data.regs i < (input.length + 2) ^ (160 * κ + 968)) ∧ ∀ (a : ℕ), s.data.mem a < (input.length + 2) ^ (160 * κ + 968)

Every run prefix at every admitted width uses polynomially bounded words. This includes all memory words and registers, rather than merely the final output or a pair-count metric.