Native ordinary 3SUM controller

The fixed program executes preprocessing, reads its raw table/count/common-length registers, and passes each actual payload pointer to the existing Convolution host. Matrices and solver workspace begin above twice the preprocessing's polynomial word envelope. No packed input is copied or replaced; the concrete callee must keep the entire lower prefix.

Inputs shorter than three positions return false directly. This is an intentional final verdict shortcut; it does not claim that their exact preprocessing instance lists are empty.

Main definitions

• registerCount, preprocessingRegisters, hostRegisters, controllerRegisters: fixed banks.
• envelopeExponent: exponent of the reused preprocessing word bound.
• program, flatProgram: actual finite controller and its raw Boolean-returning halt.

These native control/layout choices are original. The fast solver and final exponent 1.9992 remain separate; correctness and resource proofs are supplied in the consumer modules.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.registerCount (r : ℕ) : ℕ

Fixed register count for preprocessing, one Convolution host/callee and sixteen controls.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.preprocessingRegisters (r : ℕ) (i : Fin 128) : Fin (registerCount r)

The complete original preprocessing bank.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.hostRegisters (r : ℕ) (i : Fin (64 + (r + 7))) : Fin (registerCount r)

A disjoint bank for the actual Convolution host and supplied finite callee.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.controllerRegisters (r : ℕ) (i : Fin 16) : Fin (registerCount r)

Outer controls survive both preprocessing and every Convolution call.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.inputLength : Fin 16

Saved actual input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.scale : Fin 16

Base n+2 of the polynomial reservation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.envelope : Fin 16

Computed polynomial word envelope.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.remaining : Fin 16

Remaining native multiplications.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.one : Fin 16

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.two : Fin 16

Constant two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.three : Fin 16

Boundary-case threshold.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.table : Fin 16

Actual preprocessing pointer-table base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.count : Fin 16

Actual preprocessing output count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.length : Fin 16

Actual common packed length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.current : Fin 16

Next actual table entry.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.answer : Fin 16

Accumulated raw Boolean.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.source : Fin 16

Actual pointed-to signed payload.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.address : Fin 16

Load-address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.workspace : Fin 16

Caller-owned matrix workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Decision.zero : Fin 16

Constant zero.

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

Exactly the exponent already proved for every preprocessing word.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.readLength : WordRAM.Code WordRAM.Basis.standard 16

Read only the ordinary raw length header and initialize the small-case verdict.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.setup {r : ℕ} (κ : ℕ) : WordRAM.Code WordRAM.Basis.standard (registerCount r)

Save the actual preprocessing ABI and initialize the polynomial-reservation loop.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.powerBody : WordRAM.Code WordRAM.Basis.standard 16

Every multiplication and loop decrement is an actual charged instruction.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.power : WordRAM.Code WordRAM.Basis.standard 16

Compute the fixed-exponent reservation by native iteration.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.reserve : WordRAM.Code WordRAM.Basis.standard 16

Keep every catalogue/array cell below the matrix workspace.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.loadSource : WordRAM.Code WordRAM.Basis.standard 16

Fetch the next actual pointer; no mathematical layout function supplies runtime advice.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.callSetup {r : ℕ} : WordRAM.Code WordRAM.Basis.standard (registerCount r)

Deliver four raw arguments to the caller-owned Convolution entry point.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.finish {r : ℕ} : WordRAM.Code WordRAM.Basis.standard (registerCount r)

Accumulate the actual Convolution return and advance one pointer.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.body {r : ℕ} (c : Host.Callee r) : WordRAM.Code WordRAM.Basis.standard (registerCount r)

One complete native pointed-to Convolution call.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.calls {r : ℕ} (c : Host.Callee r) : WordRAM.Code WordRAM.Basis.standard (registerCount r)

Visit all actually emitted packed instances.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.large {r : ℕ} (κ : ℕ) (c : Host.Callee r) : WordRAM.Code WordRAM.Basis.standard (registerCount r)

Actual preprocessing and all caller-safe solver calls on inputs with at least three entries.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.program {r : ℕ} (κ : ℕ) (c : Host.Callee r) : WordRAM.Code WordRAM.Basis.standard (registerCount r)

One finite standard-code body per fixed input exponent and concrete finite callee.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.flatProgram {r : ℕ} (κ : ℕ) (c : Host.Callee r) : WordRAM.Program WordRAM.Basis.standard (registerCount r)

The single final halt returns the raw accumulated Boolean.