Composing actual preprocessing with every Convolution call

The original initialized preprocessing execution supplies its actual pointer table, count and common packed length. Its uniform polynomial word theorem bounds the pointers and signed cells. The charged native controller then runs the complete caller-safe host on every stored payload.

Main definitions

• instanceLength, instanceBound: existing finite reduction length and count bound.
• cost: complete host bound with the actual packed length and concrete callee time.

Main results

• exec_large: exact existing distinct-position verdict from the actual preprocessing bank.

This native composition is original and reuses the finite Chan–He reduction correctness theorem. A fast Exact Triangle backend and the final 1.9992 endpoint remain separate obligations.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.instanceLength (κ n : ℕ) : ℕ

The exact common packed length already produced by native preprocessing.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.instanceBound (κ n : ℕ) : ℕ

The existing finite count bound, with the same original-input magnitude.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.cost {r : ℕ} (κ : ℕ) (c : Host.Callee r) (n : ℕ) : ℕ

Every preprocessing, pointer, matrix, callee and control instruction, including halt. The callee is charged at the packed side and coarse polynomial filler actually passed to it.

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

Complete ordinary execution after the saved-header prefix, with no solver oracle.