Polynomial native preprocessing intermediates at every admitted width

The program never reads physical width. Its complete execution at the derived minimum width therefore identifies every prefix at every larger admitted width. Every actual register and memory word, including address and arithmetic temporaries, has polynomial magnitude throughout.

Main results

• two_pow_width_le: the minimum-width word universe has polynomial magnitude.
• intermediates_polynomial: uniform polynomial bounds on every actual run-prefix word.
• space_polynomial: every actual run prefix has zero memory beyond the same polynomial range.

These native representation bounds are original and use the generic width-prefix API.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.two_pow_width_le (κ n : ℕ) : 2 ^ width κ n ≤ (n + 2) ^ (2720 * κ + 16456)

The derived minimum-width word universe is bounded by a fixed polynomial.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.intermediates_polynomial {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State 128} {steps : ℕ} (hr : WordRAM.Runs w (flatProgram κ) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s steps) : (∀ (i : Fin 128), s.data.regs i < (input.length + 2) ^ (2720 * κ + 16456)) ∧ ∀ (a : ℕ), s.data.mem a < (input.length + 2) ^ (2720 * κ + 16456)

Every register, temporary and memory word has polynomial magnitude at every admitted width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.space_polynomial {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State 128} {steps a : ℕ} (hr : WordRAM.Runs w (flatProgram κ) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s steps) (ha : (input.length + 2) ^ (2720 * κ + 16456) ≤ a) : s.data.mem a = 0

Every prefix uses a polynomial initial interval of memory, even at wider physical widths.