Polynomial words and space for every ordinary-host prefix #
The minimum derived physical width is logarithmic in the original input length. Since the actual program never reads physical width, its completed minimum-width execution identifies all prefixes at every wider admitted width, including all concrete callee scratch operations.
Main results #
two_pow_width_le: explicit fixed polynomial word universe.intermediates_polynomial: every actual register and memory word stays polynomially bounded.space_polynomial: all actual prefix memory is zero beyond that polynomial interval.
These native representation bounds are original and reuse the generic width-prefix theorem.
The fixed minimum-width word universe has polynomial magnitude in the original length.
theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.intermediates_polynomial {κ w r : ℕ} (input : List ℤ) (c : Host.Callee r) (hw : width κ c.widthCoefficient input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State (registerCount r)} {steps : ℕ} (hr : WordRAM.Runs w (flatProgram κ c) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s steps) :
(∀ (i : Fin (registerCount r)), s.data.regs i < (input.length + 2) ^ (2 * widthCoefficient κ c.widthCoefficient)) ∧ ∀ (a : ℕ), s.data.mem a < (input.length + 2) ^ (2 * widthCoefficient κ c.widthCoefficient)
All actual prefix words are polynomial, uniformly at every admitted physical width.
theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.space_polynomial {κ w r : ℕ} (input : List ℤ) (c : Host.Callee r) (hw : width κ c.widthCoefficient input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) {s : WordRAM.State (registerCount r)} {steps a : ℕ} (hr : WordRAM.Runs w (flatProgram κ c) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) s steps) (ha : (input.length + 2) ^ (2 * widthCoefficient κ c.widthCoefficient) ≤ a) :
Every actual prefix uses only a fixed polynomial initial interval of memory.