Derived native frontend word width and charged cost

The physical unsigned width is four times the existing complete parameter width. This coarse positive logarithmic threshold covers all descriptor/payload addresses and native intermediates. The bit budget passed to radix is the explicit magnitude-derived label count, never physical width.

Main definitions

• layout: concrete runtime layout at fixed exponent and input length.
• width: positive logarithmic physical word-width threshold.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.layout (κ n : ℕ) : Layout

Layout computed from the actual unsigned input-length header and polynomial promise.

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

Physical unsigned width, including the two bits reserved when composing signed kernels.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.cost (κ n : ℕ) : ℕ

Concrete charged instruction bound, including the final halt.

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

The width coefficient is positive, including exponent zero and empty input.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.width_eq (κ n : ℕ) : width κ n = (80 * κ + 484) * Nat.clog 2 (n + 2)

The physical width is explicitly Cκ * clog₂(n+2) with a positive coefficient.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.array_budget_le (n U : ℕ) : Arrays.budget { n := n, digits := ThreeSum.labelBits (2 * U) } U ≤ ChanHe.Parameters.Math.budget n U ^ 4

All frontend arithmetic is bounded by the fourth power of the existing parameter budget.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.array_budget_fits {κ n w : ℕ} (hw : width κ n ≤ w) : WordRAM.Fits w (Arrays.budget (layout κ n) ((n + 2) ^ κ))

The derived physical width discharges the complete native frontend budget.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.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)

Input/header fitting follows from the same global magnitude and width promises.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.key_lt_two_pow {U : ℕ} (hU : 1 ≤ U) {z : ℤ} (hz : |z| ≤ ↑U) : WordRAM.Signed.encode z < 2 ^ ThreeSum.labelBits (2 * U)

The lower-level radix bit bound includes the largest signed key, even when κ=0.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.digits_bound (κ n : ℕ) : (layout κ n).digits ≤ (20 * κ + 121) * Nat.clog 2 (n + 2)

The explicit radix bit count has a logarithmic bound independent of admitted physical width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.array_budget_polynomial (κ n : ℕ) : Arrays.budget (layout κ n) ((n + 2) ^ κ) ≤ (n + 2) ^ (80 * κ + 480)

The entire allocated region and arithmetic budget are polynomial in actual input length.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.signed_output_fits {κ n w : ℕ} (hw : width κ n ≤ w) {z : ℤ} (hz : |z| ≤ ↑(2 * (n + 2) ^ κ)) : GenericRAM.Signed.Fits (w - 2) z

Every compact output integer fits the parent's signed kernel width physicalWidth-2. Thus the parent's native signed arithmetic compiler runs at exactly the physical width here.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.two_pow_width_le (κ n : ℕ) : 2 ^ width κ n ≤ (n + 2) ^ (160 * κ + 968)

A word at the canonical physical width has polynomial magnitude.