Native parameters for Chan–He preprocessing

Original native programs and proofs. The parameter meanings are the existing finite mathematical Chan–He definitions, with magnitude bound 2U after the distinct-position frontend. All loops and arithmetic are instructions; the program is fixed for each exponent κ.

Main definitions

• Parameters.program: read the input header and compute the exact parameters.
• Parameters.Output: identify the unsigned output registers.

Main results

• Parameters.runs_input: native execution from signed-encoded input with derived fits.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.Math.budget (n U : ℕ) : ℕ

A bound covering arithmetic, unsuccessful loop tests, and all output words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.len : Fin 24

Unsigned input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.magnitude : Fin 24

Original magnitude bound U.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.digits : Fin 24

Label bits for magnitude bound 2U.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.height : Fin 24

Recursion height.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.fuel : Fin 24

Recursion fuel.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.want : Fin 24

Number of desired primes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.primeBound : Fin 24

Upper bound on candidate primes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.packedLen : Fin 24

Common packed convolution length, 8m².

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.padding : Fin 24

Magnitude of the padding for the doubled frontend bound, 4U+1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.one : Fin 24

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.two : Fin 24

Constant two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.three : Fin 24

Constant three.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.four : Fin 24

Constant four.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.five : Fin 24

Constant five.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.eight : Fin 24

Constant eight.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.base : Fin 24

Input length plus two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.quotient : Fin 24

Consumed logarithm argument.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.logLen : Fin 24

Floor logarithm of input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.root : Fin 24

Integer square root of input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.wantSucc : Fin 24

Number of desired primes plus one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.temp : Fin 24

Arithmetic scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.nextRoot : Fin 24

Successor square-root counter.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.square : Fin 24

Square of that counter.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.rootBound : Fin 24

Square-root test bound.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.Output (n U : ℕ) (x : WordRAM.Data 24) : Prop

Exact mathematical outputs; every output is an ordinary unsigned word.

• len : x.regs Parameters.len = n
• magnitude : x.regs Parameters.magnitude = U
• digits : x.regs Parameters.digits = ThreeSum.labelBits (2 * U)
• height : x.regs Parameters.height = ThreeSum.ChanHe.height n
• fuel : x.regs Parameters.fuel = ThreeSum.ChanHe.fuel n
• want : x.regs Parameters.want = ThreeSum.ChanHe.wPar n (2 * U)
• primeBound : x.regs Parameters.primeBound = ThreeSum.ChanHe.mPar n (2 * U)
• packedLen : x.regs Parameters.packedLen = 8 * ThreeSum.ChanHe.mPar n (2 * U) ^ 2
• padding : x.regs Parameters.padding = 4 * U + 1

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.setup : WordRAM.Code WordRAM.Basis.standard 24

One header load, constants, and the polynomial base.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.power : ℕ → WordRAM.Code WordRAM.Basis.standard 24

Unroll only the fixed exponent, never the input length or word width.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.logRegisters (dst : Fin 24) : Fin 4 → Fin 24

Register selection for a floor/ceiling logarithm with output dst.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.sqrtRegisters : Fin 6 → Fin 24

Register selection for successive squares.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.calculate : WordRAM.Code WordRAM.Basis.standard 24

The instruction sequence after the power computation.

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

Fixed 24-register native code for each fixed polynomial magnitude exponent.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.time (κ n U : ℕ) : ℕ

An explicit charged bound, including all header reads, copies and setup. Halt adds one.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.exec {w : ℕ} (κ : ℕ) (x : WordRAM.Data 24) (hfit : WordRAM.Fits w (Math.budget (x.mem 0) ((x.mem 0 + 2) ^ κ))) : ∃ (y : WordRAM.Data 24), WordRAM.ExecWithin w (program κ) x y (time κ (x.mem 0) ((x.mem 0 + 2) ^ κ)) ∧ Output (x.mem 0) ((x.mem 0 + 2) ^ κ) y ∧ y.mem = x.mem

Read the native unsigned header and compute all parameters, preserving every memory cell. This local theorem is discharged from a logarithmic width in runs_input.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.Math.scale (n U : ℕ) : ℕ

A polynomial scale for bounding every parameter intermediate.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.Math.budget_le_scale (n U : ℕ) : budget n U ≤ scale n U ^ 20

A coarse polynomial bound; it also covers final unsuccessful root/log iterations.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.Math.budget_polynomial (κ n : ℕ) : budget n ((n + 2) ^ κ) ≤ (n + 2) ^ (20 * κ + 120)

A single polynomial bound, with exponent affine in the fixed magnitude exponent.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.width (κ n : ℕ) : ℕ

Positive logarithmic word-width threshold for the complete parameter computation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.width_pos (κ n : ℕ) : 0 < width κ n

The width requirement is satisfiable even at empty input and exponent zero.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.budget_fits {κ n w : ℕ} (hw : width κ n ≤ w) : WordRAM.Fits w (Math.budget n ((n + 2) ^ κ))

Every local fit premise follows from the positive logarithmic width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.inputFits {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : WordRAM.InputFits w (List.map WordRAM.Signed.encode input)

Signed-encoded inputs and the unsigned length header fit at the same width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.time_bound (κ n : ℕ) : time κ n ((n + 2) ^ κ) ≤ 5 * n.sqrt + (400 * κ + 3000) * Nat.clog 2 (n + 2)

Explicit Oκ(√n + log(n+2)) instruction bound, valid also at n = 0,1,2.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.runs_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : ∃ (y : WordRAM.Data 24), ∃ t ≤ 5 * input.length.sqrt + (400 * κ + 3000) * Nat.clog 2 (input.length + 2), WordRAM.Runs w ((program κ).program packedLen) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := (program κ).size, data := y } t ∧ Output input.length ((input.length + 2) ^ κ) y ∧ y.mem = (WordRAM.Data.init (List.map WordRAM.Signed.encode input)).mem ∧ WordRAM.Data.Bounded w y

Native run from actual signed input initialization. No parameters or arithmetic routines are supplied as advice. The returned state identifies all outputs and keeps all input memory. The flat program has 24 registers and depends only on κ; halting adds one instruction.

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

The number of native instructions in the finite structured code is affine in κ.

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

The code is the same at every word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters.intermediates_polynomial {κ : ℕ} (input : List ℤ) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State 24} {t : ℕ} (hr : WordRAM.Runs (width κ input.length) ((program κ).program packedLen) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s t) : (∀ (i : Fin 24), s.data.regs i < (input.length + 2) ^ (40 * κ + 242)) ∧ ∀ (a : ℕ), s.data.mem a < (input.length + 2) ^ (40 * κ + 242)

Canonical-width executions use only polynomially bounded integers, including memory addresses, loop counters, and final unsuccessful tests.