Native initialized-input Chan–He preprocessing program

The complete finite instruction program first executes the native frontend and parameter computation. It builds the prime bitmap by actual trial division, computes concrete stack and output-table reservations, and loads and traverses every actual six-word frontend descriptor. The ternary reservation is computed by a native multiplication loop, not supplied by a caller.

This module defines the executable program. PreprocessingInput, PreprocessingWidth and PreprocessingTime prove initialized-input execution, derived width and charged global bounds.

Main definitions

• program: one finite 128-register program per fixed magnitude exponent.
• flatProgram: the complete native program with its final count-returning halt.
• loadRoot, forest: actual descriptor loads and the outer native root loop.

Main results

• not_readsWidth: runtime physical width never controls the program's computation.
• size_program: code size depends only on the fixed exponent.

The code and layout computations are original. Output metadata is unsigned; payload words use the existing signed encoding. No solver, collision, primality or operation-count oracle is used.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.descriptors : Fin 128

Saved frontend descriptor base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.roots : Fin 128

Saved number of roots.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.current : Fin 128

Index of the next root.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.levels : Fin 128

The computed recursion fuel shared by all roots.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.inputMagnitude : Fin 128

The computed original-input magnitude.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.candidateLimit : Fin 128

The computed candidate-prime bound.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.labels : Fin 128

The computed label-bit parameter.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.packedLength : Fin 128

Common packed length in words, retained as unsigned output metadata.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.firstFree : Fin 128

One-past-end frontend address; the shared prime bitmap begins here.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.stride : Fin 128

Six words per frontend root descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.one : Fin 128

Outer-controller constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.zero : Fin 128

Outer-controller constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.address : Fin 128

Descriptor-loading address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.power : Fin 128

Computed ternary-tree reservation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.remaining : Fin 128

Remaining reservation multiplications.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.outputCapacity : Fin 128

Reserved number of unsigned output pointers.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.scalar : Fin 128

Setup constant, first seven and then three.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.four : Fin 128

The constant four converts packed words to groups.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.heapFloor : Fin 128

Initial heap frontier, above the complete stack and pointer-table reservations.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.primeRegisters (i : Fin 15) : Fin 128

The complete 15-register prime builder runs in the low registers.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.snapshot : WordRAM.Code WordRAM.Basis.standard 128

Save every frontend/parameter output that the reused traversal registers will overwrite.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.preparePrimes : WordRAM.Code WordRAM.Basis.standard 128

Deliver the actual native prime-table inputs.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.setupTraversal : WordRAM.Code WordRAM.Basis.standard 128

Compute the traversal ABI and concrete stack reservation, retaining the outer metadata.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.powerBody : WordRAM.Code WordRAM.Basis.standard 128

One actual multiplication and decrement per ternary-reservation level.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.reserve : WordRAM.Code WordRAM.Basis.standard 128

Compute 3^(fuel+1) by a finite native loop.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.finishLayout : WordRAM.Code WordRAM.Basis.standard 128

Reserve all output pointers before the initial fresh heap frontier.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.loadRoot : WordRAM.Code WordRAM.Basis.standard 128

Load all six descriptor words in their actual length/pointer order, with the shared fuel.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.body : WordRAM.Code WordRAM.Basis.standard 128

Traverse the actually loaded root, then advance the actual descriptor index.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.forest : WordRAM.Code WordRAM.Basis.standard 128

Enumerate every frontend root, including the exact empty and multiplicity boundary roots.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.afterFrontend : WordRAM.Code WordRAM.Basis.standard 128

Complete native preprocessing after the native initialized-input frontend.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.program (κ : ℕ) : WordRAM.Code WordRAM.Basis.standard 128

One finite native program per fixed magnitude exponent, independent of input length/width.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.flatProgram (κ : ℕ) : WordRAM.Program WordRAM.Basis.standard 128

Complete flat native program; it returns the unsigned output count.

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

Physical width never determines radix passes, prime candidates, recursion fuel or code.

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

The finite controller adds a fixed code suffix to the exponent-dependent frontend.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.body_preserves (i : Fin 128) : 109 ≤ ↑i → i ≠ current → i ≠ address → WordRAM.Code.Preserves i body

Only the current index and address scratch among registers 109–127 change during a root.