Derived logarithmic width for native Chan–He preprocessing

The positive physical-width threshold depends only on the fixed magnitude exponent and actual input length. Its signed envelope covers every root, including all shared memory reservations.

Main definitions

• width: positive physical width sufficient for the complete preprocessing envelope.

Main results

• arena_ready: global logarithmic width derives the complete traversal fit contract.
• input_fits: the same width derives actual signed-encoded input fitting.

These coarse native resource bounds are original.

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

One positive logarithmic physical width for every native preprocessing component.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.width_eq (κ n : ℕ) : width κ n = (1300 * κ + 7865) * Nat.clog 2 (n + 2)

The threshold has a positive exponent-dependent coefficient and no dependence on input data.

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

Empty inputs and exponent zero also receive a strictly positive word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.three_le_width (κ n : ℕ) : 3 ≤ width κ n

The signed compiler's two representation bits are always available.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.frontend_width_le (κ n : ℕ) : Frontend.width κ n ≤ width κ n

The whole-frontend threshold is covered by the global preprocessing threshold.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.arena_ready {κ n w : ℕ} (hw : width κ n ≤ w) (retained : ℕ → ℕ) : (arena κ n retained).Ready (w - 2)

The global logarithmic width derives all local signed kernel fits and allocation bounds.

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

The actual native unsigned length header and every signed payload fit the derived width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.setup_fits {κ n w : ℕ} (hw : width κ n ≤ w) (retained : ℕ → ℕ) : have a := arena κ n retained; WordRAM.Fits w (a.floor + a.U + a.N + a.fuel + 16) ∧ WordRAM.Fits w ((Frontend.layout κ n).endpoint + a.m + 4) ∧ WordRAM.Fits w (3 ^ (a.fuel + 1)) ∧ WordRAM.Fits w 6

The same global width covers every scalar and address of the native layout controller.