Original-size prefix bounds and the per-record thin saving

The initialized code has physical-width-independent polynomial words and memory support at every admitted wider width. Its charge is the actual producer preparation plus the selected record's actual thin product. Summing all products, solving ExactTriangle and reconstructing witnesses remain separate; no aggregate subcubic claim is made here.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.wordBound (n D g p A : ℕ) : ℕ

Explicit input-derived bound for all prefix words and the address support, independent of any larger admitted physical width. This is a reservation, not a bulk initialization.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.wordBound_le_pow {n D g p A κ : ℕ} (hn : 1 ≤ n) (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : wordBound n D g p A ≤ (n + 2) ^ (514 * κ + 11812)

The prefix bound is polynomial in original size for the usual original scalar/weight envelopes, with an explicit fixed exponent for each magnitude exponent κ.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.bounded_reachable_original {W m n g p A k : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ MatrixMultiplication.Schonhage.D m) (hg : 1 ≤ g) (hp : 0 < p) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (MatrixMultiplication.Schonhage.D m) g p A ≤ W) {s : WordRAM.State 320} (hr : WordRAM.Runs W (entryProgram.program Reg.result) (WordRAM.State.init (PreparationInput.input n (MatrixMultiplication.Schonhage.D m) g p values)) s k) : (∀ (i : Fin 320), s.data.regs i < wordBound n (MatrixMultiplication.Schonhage.D m) g p A) ∧ (∀ (a : ℕ), s.data.mem a < wordBound n (MatrixMultiplication.Schonhage.D m) g p A) ∧ ∀ (a : ℕ), wordBound n (MatrixMultiplication.Schonhage.D m) g p A ≤ a → s.data.mem a = 0

Every actual native prefix at every admitted width has input-derived bounded words and zero memory beyond the same bound. The real halting run at the minimum admitted width and the existing width-independent prefix theorem derive the result.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.initialized_time_le {m n g p : ℕ} (values : List ℤ) (qs : List (Fin n × Fin n)) (hD : 16 ≤ MatrixMultiplication.Schonhage.D m) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hg : 1 ≤ g) (hp : p ∈ (MatrixMultiplication.Schonhage.D m).sqrtPrimeWindow) (hQ : qs.length * 2 ^ m ≤ n ^ 2) : ↑(preparationTime n (MatrixMultiplication.Schonhage.D m) g p values + timeBound qs + 1) ≤ 690 * ↑n ^ 2 * ↑(MatrixMultiplication.Schonhage.D m) * ↑g + 34603008 * ↑(19 * m + 1) * ↑n ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18)

Complete producer preparation plus one actual record product, including the final halt. The per-record sparsity is supplied by its actual native chunk, not an aggregate solver oracle.