Complete initialized native ordinary 3SUM host

One finite program per fixed input-magnitude exponent and concrete certified finite Exact Triangle block starts at actual State.init. It computes preprocessing, reads all actual packed pointers and calls the caller-safe Convolution host. Its final raw Boolean is equivalent to the existing integer 3SUM predicate with distinct positions and repeated values permitted.

The result is conditional on the supplied actual finite code and its explicit callee contract. The slow exhaustive certified block provides a live instance; this theorem does not construct a fast backend or claim the final subquadratic endpoint.

Main results

• exec_input: complete actual structured execution, global logarithmic width and verdict.
• runs_input: actual halting flat execution and its actual pre-halt state witness.
• not_readsWidth: the complete ordinary host never reads physical width.

The composition and resource bookkeeping are original and reuse the existing finite reductions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.seven_le_cost {r : ℕ} (κ : ℕ) (c : Host.Callee r) (n : ℕ) : 7 ≤ cost κ c n

The complete charged budget always includes the seven small-branch instructions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.not_readsWidth {r : ℕ} (κ : ℕ) (c : Host.Callee r) : ¬(program κ c).ReadsWidth

The fixed ordinary host is independent of physical word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_input {κ w r : ℕ} (input : List ℤ) (c : Host.Callee r) (hw : width κ c.widthCoefficient input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : ∃ (y : WordRAM.Data (registerCount r)), WordRAM.ExecWithin w (program κ c) (WordRAM.Data.init (List.map WordRAM.Signed.encode input)) y (cost κ c input.length - 1) ∧ y.regs (controllerRegisters r answer) ≤ 1 ∧ (y.regs (controllerRegisters r answer) = 1 ↔ ThreeSum.HasSolution fun (i : Fin input.length) => input[i])

Actual execution from initialized signed input, uniformly over all admitted wider words.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.runs_input {κ w r : ℕ} (input : List ℤ) (c : Host.Callee r) (hw : width κ c.widthCoefficient input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : ∃ (y : WordRAM.Data (registerCount r)) (steps : ℕ), WordRAM.Executes w (flatProgram κ c) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) (y.regs (controllerRegisters r answer)) steps ∧ WordRAM.Runs w (flatProgram κ c) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := (program κ c).size, data := y } (steps - 1) ∧ steps ≤ cost κ c input.length ∧ y.regs (controllerRegisters r answer) ≤ 1 ∧ (y.regs (controllerRegisters r answer) = 1 ↔ ThreeSum.HasSolution fun (i : Fin input.length) => input[i]) ∧ WordRAM.Data.Bounded w y

Complete actual flat execution and actual pre-halt output-state witness. The output is raw 0 or 1; the input and every generated matrix cell use signed encoding.