Logarithmic physical width for the complete ordinary host

The coefficient depends only on the fixed magnitude exponent and the concrete finite callee. It covers the native computation of the preprocessing word envelope, the disjoint matrix arena, and the callee's actual logarithmic-width obligation. No width depends on input values.

Main definitions

• widthCoefficient, width: positive uniform physical-width threshold.

Main results

• preprocessing_width_le: reuse the complete preprocessing threshold.
• margin_fits: polynomial envelope with three extra signed representation bits.
• callee_width: the actual free pointer, filler and side satisfy the concrete callee contract.

These coarse polynomial bounds are original.

def Cslib.Algorithms.WordRAM.ThreeSum.Decision.widthCoefficient (κ d : ℕ) : ℕ

A constant for fixed exponent and concrete callee, independent of length and word width.

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

Positive logarithmic physical width, including empty inputs.

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

This native width is positive for every length and exponent.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.preprocessing_width_le (κ d n : ℕ) : ChanHe.Preprocessing.width κ n ≤ width κ d n

The complete preprocessing's physical threshold is covered.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.four_le_width (κ d n : ℕ) : 4 ≤ width κ d n

Enough physical bits remain for the signed compiler's two bits and its signed range.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.margin_fits {κ d n w : ℕ} (hw : width κ d n ≤ w) : WordRAM.Fits (w - 3) ((n + 2) ^ (envelopeExponent κ + 5))

A polynomial envelope for every local caller arithmetic result fits with a signed margin.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.reservation_margin (κ n : ℕ) : 32 * (n + 2) ^ envelopeExponent κ ≤ (n + 2) ^ (envelopeExponent κ + 5)

Thirty-two times the reservation remains within the small extra polynomial margin.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.callee_width {κ d n N w : ℕ} (hN : N < (n + 2) ^ envelopeExponent κ) (hw : width κ d n ≤ w) : d * Nat.clog 2 (2 * (n + 2) ^ envelopeExponent κ + 3 * (Host.sideLength N * Host.sideLength N) + (2 * (n + 2) ^ envelopeExponent κ + 1) + Host.sideLength N + 2) ≤ w

The actual matrix arena, filler and side meet the finite callee's width guarantee.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.signed_margin {κ d n w : ℕ} (hw : width κ d n ≤ w) (z : ℤ) (hz : |z| ≤ ↑((n + 2) ^ (envelopeExponent κ + 5))) : GenericRAM.Signed.Fits (w - 2) z

Every integer in the polynomial margin fits the signed source width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.reservation_fits {κ d n w : ℕ} (hw : width κ d n ≤ w) : WordRAM.Fits w ((n + 2) ^ envelopeExponent κ) ∧ WordRAM.Fits w (envelopeExponent κ) ∧ WordRAM.Fits w (n + 2) ∧ WordRAM.Fits w 3

The runtime exponent and every power-loop result fit without an extra input premise.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.caller_fits {κ d n N w : ℕ} (hN : N < (n + 2) ^ envelopeExponent κ) (hw : width κ d n ≤ w) : have V := (n + 2) ^ envelopeExponent κ; (∀ s < 2 * Host.sideLength N, GenericRAM.Signed.Fits (w - 2) ↑(2 * (Host.sideLength N * Host.sideLength N) + s + 1)) ∧ GenericRAM.Signed.Fits (w - 2) (2 * ↑V + 1) ∧ GenericRAM.Signed.Fits (w - 2) (-(2 * ↑V + 1)) ∧ (∀ (z : ℤ), |z| ≤ ↑V → GenericRAM.Signed.Fits (w - 2) z) ∧ WordRAM.Fits w (2 * V + 3 * (Host.sideLength N * Host.sideLength N)) ∧ WordRAM.Fits w (4 * V + 2) ∧ WordRAM.Fits w (4 * N + 4) ∧ WordRAM.Fits w (2 * V)

All local caller premises follow from the single global logarithmic threshold.