Thin-regime native instruction bound

Main results

• BandPreparation.runs_thin: actual initialized native execution, including the halt, within 81920*(L+1)*N²/(4^m)^(1/18) at L=19m, N≥(4^m)^18.
• BandPreparation.width_exists: original magnitude and parameter inequalities are jointly satisfiable for every finite input bound, including positive thin parameters.

The result concerns shared-band preparation and encoding only. Pruned queries, products and the whole ordinary 3SUM endpoint remain separate obligations.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.runs_thin {w m N : ℕ} (hw : 0 < w) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (A : ℤ) (hA : 0 ≤ A) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ A) (hmag : ↑(7 ^ (19 * m)) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget (19 * m) m N)) : ∃ (n : ℕ), WordRAM.Executes (w + 2) (program.program catalogue) (WordRAM.State.init (input (19 * m) m N X Y)) (catalogueBase (19 * m) m N) n ∧ ↑n ≤ 81920 * ↑(19 * m + 1) * ↑N ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18)

All charged preparation and encoder instructions, including the final halt, satisfy the finite thin-regime saving. Both the coefficient and polynomial exponent are fixed.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.width_exists (L m N : ℕ) (A : ℤ) (hA : 0 ≤ A) : ∃ (w : ℕ), 0 < w ∧ ↑(7 ^ L) * A < 2 ^ (w - 1) ∧ WordRAM.Fits (w + 2) (wordBudget L m N)

A concrete, deliberately generous width witnesses simultaneous signed-magnitude and unsigned-address fits. This proves nonvacuity without enumerating a thin matrix.