diff --git a/Complexity.lean b/Complexity.lean
index c56d26719c..f9dd073120 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -53,6 +53,10 @@ public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Alphabets
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BandBounds
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Batch
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxPartition
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffEncoding
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffExponent
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffParameters
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxValues
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Boxes
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxesFromLeaves
@@ -335,6 +339,25 @@ public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxBa
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxBatch.Program
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxBatch.Resources
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxBatch.Width
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Admission
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Arguments
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Bounds
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Charges
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Exec
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Front
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.FrontProgram
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Geometry
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Input
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Layout
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Program
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Resources
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Restore
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.State
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Thin
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Tile
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Tiles
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Width
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxQuery
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxQuery.Bounds
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxQuery.CompleteLeaf
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoff.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoff.lean
new file mode 100644
index 0000000000..d98aa1da57
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoff.lean
@@ -0,0 +1,239 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxValues
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Tiling
+public import Mathlib.Basic.Real.Basic
+import Mathlib.Algebra.Order.Field.GeomSum
+import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.GCongr
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
+
+/-!
+# Finite preprocessing/query tradeoff for shared box tables
+
+A threshold trades a geometric tail of the completed-leaf counts `beta` against a
+weighted binomial prefix of the query counts `alpha`. The all-tile estimate charges
+one retained box value for each box of each tile, while the query estimate charges
+all requested occurrences separately. Neither estimate is a machine-running-time law.
+
+## Main definitions
+
+* `BoxTradeoff.rho`: geometric decay rate determined by the original depths.
+
+## Main results
+
+* `BoxTradeoff.sum_beta_le`: geometric tail estimate for retained-table construction.
+* `BoxTradeoff.sum_alpha_le`: weighted binomial prefix estimate for one sparse query.
+* `BoxTradeoff.total_boxes_le`: sum of retained-box counts over the actual finite tile set.
+
+## References
+
+Adapted from [AlmanWilliams2026, equation (7) and Section 4.4], specifically
+[Theorem30.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Theorem30.lean)
+lines 53–102 and 253–287, and
+[ParameterSteps.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/ParameterSteps.lean)
+lines 147–172, at the pinned primary formal source. Both files were checked against
+that revision. The tile estimate uses this library's padded dimension and therefore
+has factor `4*padN²`; a separate band-size premise gives factor `16*N²`. This is a
+constant-factor weakening of the source's finer unpadded tile estimate. The source's
+analytic encoding-term domination, logarithmic estimates and final exponents are not
+claimed here. No source machine or execution semantics is imported.
+-/
+
+public section
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+
+open Finset
+
+/-- Every threshold admits a fully fixed box with no P0 coordinates, even at depth zero. -/
+theorem card_boxes_pos (L m t : ℕ) : 0 < (boxes L m t).card := by
+  apply Finset.card_pos.mpr
+  refine ⟨Cube.ofLeaf (fun _ => Term.P 0 0), mem_boxes.mpr ?_⟩
+  simp [IsBox, Cube.P0Levels_ofLeaf, P0Levels]
+
+/-- The ratio envelope `9m/(L-m+1)`, with subtraction in the real numbers. -/
+@[expose] noncomputable def rho (L m : ℕ) : ℝ := 9 * (m : ℝ) / ((L : ℝ) - m + 1)
+
+/-- The decay rate is nonnegative whenever the total depth contains the inner depth. -/
+theorem rho_nonneg {L m : ℕ} (hm : m ≤ L) : 0 ≤ rho L m := by
+  have hm' : (m : ℝ) ≤ L := by exact_mod_cast hm
+  exact div_nonneg (by positivity) (by linarith)
+
+/-- The source's depth condition makes the geometric tail summable, including `m = 0`. -/
+theorem rho_lt_one {L m : ℕ} (hL : 10 * m ≤ L) : rho L m < 1 := by
+  have hL' : (10 : ℝ) * m ≤ L := by exact_mod_cast hL
+  have hm : (0 : ℝ) ≤ m := Nat.cast_nonneg _
+  rw [rho, div_lt_one (by linarith)]
+  linarith
+
+private theorem beta_step {L m d : ℕ} (hm : m ≤ L) (hd : d + 1 ≤ m) :
+    (beta L m (d + 1) : ℝ) ≤ rho L m * (beta L m d : ℝ) := by
+  have hm' : (m : ℝ) ≤ L := by exact_mod_cast hm
+  have hd' : (d : ℝ) + 1 ≤ m := by exact_mod_cast hd
+  have hb : (0 : ℝ) < beta L m d := by exact_mod_cast beta_pos hm d
+  have hratio := congrArg (fun q : ℚ => (q : ℝ))
+    (beta_ratio hm (d + 1) (by omega) hd)
+  push_cast at hratio
+  have hbound : 9 * ((m : ℝ) - ((d : ℝ) + 1) + 1) /
+      ((L : ℝ) - (m : ℝ) + ((d : ℝ) + 1)) ≤ rho L m := by
+    exact div_le_div₀ (by positivity) (by linarith) (by linarith) (by linarith)
+  rw [← hratio, div_le_iff₀ hb] at hbound
+  exact hbound
+
+/-- Equation (7): the order-`d` completed-leaf count decays from the order-zero count `M`.
+The inequality holds for every `m ≤ L`; summability is needed only for the tail theorem. -/
+theorem beta_le {L m : ℕ} (hm : m ≤ L) (d : ℕ) (hd : d ≤ m) :
+    (beta L m d : ℝ) ≤ rho L m ^ d * (M L m : ℝ) := by
+  induction d with
+  | zero => simp [beta_zero_eq_M]
+  | succ d ih =>
+    calc (beta L m (d + 1) : ℝ) ≤ rho L m * (beta L m d : ℝ) := beta_step hm hd
+      _ ≤ rho L m * (rho L m ^ d * (M L m : ℝ)) :=
+        mul_le_mul_of_nonneg_left (ih (by omega)) (rho_nonneg hm)
+      _ = rho L m ^ (d + 1) * (M L m : ℝ) := by ring
+
+/-- Theorem 30's retained-table estimate: all completed leaves through order `m`
+above a threshold are bounded by a convergent geometric tail. No threshold premise
+is required; an empty tail also satisfies this bound. -/
+theorem sum_beta_le {L m : ℕ} (t : ℕ) (hL : 10 * m ≤ L) :
+    ∑ d ∈ Icc t m, (beta L m d : ℝ) ≤
+      (M L m : ℝ) * (rho L m ^ t / (1 - rho L m)) := by
+  calc ∑ d ∈ Icc t m, (beta L m d : ℝ)
+      ≤ ∑ d ∈ Icc t m, rho L m ^ d * (M L m : ℝ) :=
+        sum_le_sum fun d hd => beta_le (by omega) d (mem_Icc.mp hd).2
+    _ = (M L m : ℝ) * ∑ d ∈ Ico t (m + 1), rho L m ^ d := by
+      rw [← sum_mul, mul_comm, Ico_add_one_right_eq_Icc]
+    _ ≤ (M L m : ℝ) * (rho L m ^ t / (1 - rho L m)) :=
+      mul_le_mul_of_nonneg_left
+        (geom_sum_Ico_le_of_lt_one (rho_nonneg (by omega)) (rho_lt_one hL))
+        (Nat.cast_nonneg _)
+
+/-- A box table has at most `m+1` descriptors for each completed-leaf choice. Combined
+with the geometric tail, this bounds its actual finite number of retained values. -/
+theorem card_boxes_le_geometric {L m t : ℕ} (hL : 10 * m ≤ L) (ht : t ≤ m) :
+    ((boxes L m t).card : ℝ) ≤
+      ((m : ℝ) + 1) * ((M L m : ℝ) * (rho L m ^ t / (1 - rho L m))) := by
+  have hc : ((boxes L m t).card : ℝ) ≤
+      ((m : ℝ) + 1) * ∑ d ∈ Icc t m, (beta L m d : ℝ) := by
+    exact_mod_cast card_boxes_le L m t (by omega) ht
+  exact hc.trans (mul_le_mul_of_nonneg_left (sum_beta_le t hL) (by positivity))
+
+/-- All tiles share the same geometry but each computes its own retained values.
+This counts all those values against the actual padded outer dimension. -/
+theorem total_boxes_le {L m t N : ℕ} (hL : 10 * m ≤ L) (ht : t ≤ m) :
+    ((tiles L m N).card : ℝ) * ((boxes L m t).card : ℝ) ≤
+      4 * ((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m)) * (padN L m N : ℝ) ^ 2 := by
+  have hc := card_boxes_le_geometric hL ht
+  have htiles : ((tiles L m N).card : ℝ) * (M L m : ℝ) ≤
+      4 * (padN L m N : ℝ) ^ 2 := by exact_mod_cast card_tiles_mul_M_le L m N
+  have hdecay : 0 ≤ rho L m ^ t / (1 - rho L m) :=
+    div_nonneg (pow_nonneg (rho_nonneg (by omega)) _) (by linarith [rho_lt_one hL])
+  calc ((tiles L m N).card : ℝ) * ((boxes L m t).card : ℝ)
+      ≤ ((tiles L m N).card : ℝ) *
+          (((m : ℝ) + 1) * ((M L m : ℝ) * (rho L m ^ t / (1 - rho L m)))) :=
+        mul_le_mul_of_nonneg_left hc (Nat.cast_nonneg _)
+    _ = (((tiles L m N).card : ℝ) * (M L m : ℝ)) *
+        (((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m))) := by ring
+    _ ≤ (4 * (padN L m N : ℝ) ^ 2) *
+        (((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m))) :=
+      mul_le_mul_of_nonneg_right htiles (mul_nonneg (by positivity) hdecay)
+    _ = _ := by ring
+
+/-- If one band fits the original outer dimension, the retained-table count is bounded
+by `N²` without using a source execution or asymptotic hypothesis. -/
+theorem total_boxes_le_unpadded {L m t N : ℕ} (hL : 10 * m ≤ L) (ht : t ≤ m)
+    (hN : K0 L m * N0 L m ≤ N) :
+    ((tiles L m N).card : ℝ) * ((boxes L m t).card : ℝ) ≤
+      16 * ((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m)) * (N : ℝ) ^ 2 := by
+  have hpad : (padN L m N : ℝ) ≤ 2 * (N : ℝ) := by
+    exact_mod_cast padN_le_two_mul L m N hN
+  have hdecay : 0 ≤ rho L m ^ t / (1 - rho L m) :=
+    div_nonneg (pow_nonneg (rho_nonneg (by omega)) _) (by linarith [rho_lt_one hL])
+  calc ((tiles L m N).card : ℝ) * ((boxes L m t).card : ℝ)
+      ≤ 4 * ((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m)) *
+          (padN L m N : ℝ) ^ 2 := total_boxes_le hL ht
+    _ ≤ 4 * ((m : ℝ) + 1) * (rho L m ^ t / (1 - rho L m)) * (2 * (N : ℝ)) ^ 2 :=
+      mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (Nat.cast_nonneg _) hpad 2)
+        (by positivity)
+    _ = _ := by ring
+
+/-- Weighted binomial-prefix estimate from Section 4.4. With `x=8`, this gives
+`Σ(d≤t) alpha(m,d) ≤ 72^t*(9/8)^m`; every wanted occurrence incurs this count. -/
+theorem sum_alpha_le {x : ℝ} (hx : 0 < x) (h9x : 1 ≤ 9 * x) {m t : ℕ} (ht : t ≤ m) :
+    ∑ d ∈ range (t + 1), (alpha m d : ℝ) ≤ (9 * x) ^ t * (1 + 1 / x) ^ m := by
+  have hterm : ∀ d ∈ range (t + 1), (alpha m d : ℝ) ≤
+      (9 * x) ^ t * ((1 / x) ^ d * 1 ^ (m - d) * (m.choose d : ℝ)) := by
+    intro d hd
+    have hpow : (9 * x) ^ d ≤ (9 * x) ^ t :=
+      pow_le_pow_right₀ h9x (by rw [mem_range] at hd; omega)
+    calc (alpha m d : ℝ) =
+        (9 * x) ^ d * ((1 / x) ^ d * 1 ^ (m - d) * (m.choose d : ℝ)) := by
+          rw [alpha, one_pow, mul_one, ← mul_assoc, ← mul_pow,
+            show 9 * x * (1 / x) = 9 by field_simp]
+          push_cast
+          ring
+      _ ≤ (9 * x) ^ t * ((1 / x) ^ d * 1 ^ (m - d) * (m.choose d : ℝ)) := by
+        gcongr
+  calc ∑ d ∈ range (t + 1), (alpha m d : ℝ)
+      ≤ ∑ d ∈ range (t + 1),
+          (9 * x) ^ t * ((1 / x) ^ d * 1 ^ (m - d) * (m.choose d : ℝ)) :=
+        sum_le_sum hterm
+    _ ≤ ∑ d ∈ range (m + 1),
+        (9 * x) ^ t * ((1 / x) ^ d * 1 ^ (m - d) * (m.choose d : ℝ)) :=
+      sum_le_sum_of_subset_of_nonneg (range_subset_range.2 (by omega))
+        fun _ _ _ => by positivity
+    _ = (9 * x) ^ t * (1 + 1 / x) ^ m := by rw [← mul_sum, ← add_pow, add_comm]
+
+/-- The Section 4.4 query-count estimate at the concrete rational weight `x=8`. -/
+theorem sum_alpha_le_seventytwo {m t : ℕ} (ht : t ≤ m) :
+    ∑ d ∈ range (t + 1), (alpha m d : ℝ) ≤ (72 : ℝ) ^ t * (9 / 8 : ℝ) ^ m := by
+  have h := sum_alpha_le (x := 8) (by norm_num) (by norm_num) ht
+  norm_num at h
+  exact h
+
+/-- At the source's `L=21m`, the ratio is strictly below `9/20` and its tail factor below `2`. -/
+theorem rho_twentyone (m : ℕ) :
+    rho (21 * m) m < 9 / 20 ∧ 1 / (1 - rho (21 * m) m) < 2 := by
+  have heq : rho (21 * m) m = 9 * (m : ℝ) / (20 * (m : ℝ) + 1) := by
+    rw [rho]
+    push_cast
+    congr 1
+    ring
+  have hlt : rho (21 * m) m < 9 / 20 := by
+    rw [heq, div_lt_div_iff₀ (by positivity) (by norm_num)]
+    linarith
+  refine ⟨hlt, ?_⟩
+  rw [div_lt_iff₀ (by linarith)]
+  linarith
+
+/-- Concrete rational-base preprocessing decay at `L=21m`. The threshold remains
+explicit so an actual native parameter calculation can choose it independently. -/
+theorem sum_beta_twentyone (m t : ℕ) :
+    ∑ d ∈ Icc t m, (beta (21 * m) m d : ℝ) ≤
+      2 * (M (21 * m) m : ℝ) * (9 / 20 : ℝ) ^ t := by
+  obtain ⟨hrho, hfactor⟩ := rho_twentyone m
+  have hpow : rho (21 * m) m ^ t ≤ (9 / 20 : ℝ) ^ t :=
+    pow_le_pow_left₀ (rho_nonneg (by omega)) hrho.le _
+  have hdecay : rho (21 * m) m ^ t / (1 - rho (21 * m) m) ≤
+      (9 / 20 : ℝ) ^ t * 2 := by
+    rw [div_eq_mul_one_div]
+    exact mul_le_mul hpow hfactor.le
+      (one_div_nonneg.mpr (by linarith)) (by positivity)
+  calc ∑ d ∈ Icc t m, (beta (21 * m) m d : ℝ)
+      ≤ (M (21 * m) m : ℝ) *
+          (rho (21 * m) m ^ t / (1 - rho (21 * m) m)) := sum_beta_le t (by omega)
+    _ ≤ (M (21 * m) m : ℝ) * ((9 / 20 : ℝ) ^ t * 2) :=
+      mul_le_mul_of_nonneg_left hdecay (Nat.cast_nonneg _)
+    _ = _ := by ring
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffEncoding.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffEncoding.lean
new file mode 100644
index 0000000000..65ace230b9
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffEncoding.lean
@@ -0,0 +1,254 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffParameters
+import Complexity.Algorithms.MatrixMultiplication.Schonhage.BandBounds
+import Mathlib.Data.Nat.Choose.Vandermonde
+import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.Tactic.GCongr
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Rational saving for the actual shared encoding count
+
+At `m=9k`, `L=189k`, the size premise `D^18 ≤ N` makes a band fit the original
+outer dimension and bounds the total shared encoding length by
+`4*N²*(9/20)^k`. Geometry construction happens once and can use this same bound.
+
+This is an original algebraic specialization of the encoding calculation in
+[AlmanWilliams2026, proof of Corollary 26]. It replaces the source's entropy-style
+binomial lower bound and analytic estimates by `21^m ≤ binom(21m,m) ≤ 64^m`
+and one integer base comparison. It proves finite counts, with no source machine,
+execution or assumed running time, and does not assert the final 3SUM exponent.
+
+## Main results
+
+* `BoxTradeoff.bandSize_twentyone_le`: the original size bound admits each band.
+* `BoxTradeoff.encodings_ninth_blocks`: shared encoding count with a rational saving.
+* `BoxTradeoff.nativeShape_ninth_blocks`: the complete finite native-ledger shape.
+* `BoxTradeoff.decay_sixteenth`: an integer-power saving relative to the inner dimension.
+-/
+
+public section
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+
+open Finset
+
+private theorem twentyone_pow_le_choose (m : ℕ) : 21 ^ m ≤ (21 * m).choose m := by
+  induction m with
+  | zero => simp
+  | succ m ih =>
+    have hterm : (21 * m).choose m * 21 ≤ (21 * m + 21).choose (m + 1) := by
+      have h := Finset.single_le_sum (f := fun p : ℕ × ℕ =>
+        (21 * m).choose p.1 * Nat.choose 21 p.2)
+        (fun _ _ => Nat.zero_le _) (show (m, 1) ∈ Finset.antidiagonal (m + 1) by simp)
+      rw [← Nat.add_choose_eq] at h
+      simpa using h
+    calc 21 ^ (m + 1) = 21 ^ m * 21 := pow_succ _ _
+      _ ≤ (21 * m).choose m * 21 := Nat.mul_le_mul_right _ ih
+      _ ≤ (21 * (m + 1)).choose (m + 1) := by
+        simpa only [Nat.mul_add, Nat.mul_one] using hterm
+
+private theorem choose_twentyone_mul_le (m : ℕ) : (21 * m).choose m ≤ 64 ^ m := by
+  have hterm : (21 * m).choose m * 20 ^ (20 * m) ≤ 21 ^ (21 * m) := by
+    have h := Finset.single_le_sum
+      (f := fun i : ℕ => (1 : ℕ) ^ i * 20 ^ (21 * m - i) * (21 * m).choose i)
+      (fun _ _ => Nat.zero_le _) (show m ∈ range (21 * m + 1) by simp; omega)
+    have hp := add_pow (1 : ℕ) 20 (21 * m)
+    simp only [Nat.cast_id] at hp
+    rw [← hp] at h
+    rw [show 21 * m - m = 20 * m by omega] at h
+    simpa only [one_pow, one_mul, show (1 : ℕ) + 20 = 21 by decide, Nat.mul_comm] using h
+  have hbase : 21 ^ 21 ≤ 64 * 20 ^ 20 := by norm_num
+  have hpow := Nat.pow_le_pow_left hbase m
+  have hbig : 21 ^ (21 * m) ≤ 64 ^ m * 20 ^ (20 * m) := by
+    simpa only [pow_mul, mul_pow] using hpow
+  exact Nat.le_of_mul_le_mul_right (hterm.trans hbig) (Nat.pow_pos (by decide))
+
+/-- A band at the improved depth `L=21m` fits under the source's original size condition.
+The proof uses only integer binomial and power bounds. -/
+theorem bandSize_twentyone_le (m : ℕ) :
+    K0 (21 * m) m * N0 (21 * m) m ≤ D m ^ 18 := by
+  have hK : K0 (21 * m) m ≤ 8 ^ m := by
+    have hs := (K0_sq_le_K (21 * m) m).trans (choose_twentyone_mul_le m)
+    change K0 (21 * m) m ^ 2 ≤ 64 ^ m at hs
+    have heq : 64 ^ m = (8 ^ m) ^ 2 := by rw [← pow_mul, Nat.mul_comm, pow_mul]; norm_num
+    rw [heq] at hs
+    exact (Nat.pow_le_pow_iff_left (by decide : 2 ≠ 0)).mp hs
+  calc K0 (21 * m) m * N0 (21 * m) m
+      ≤ 8 ^ m * N0 (21 * m) m := Nat.mul_le_mul_right _ hK
+    _ = (8 * 3 ^ 20) ^ m := by
+      rw [N0, show 21 * m - m = 20 * m by omega, pow_mul, mul_pow]
+    _ ≤ (4 ^ 18) ^ m := Nat.pow_le_pow_left (by norm_num) _
+    _ = D m ^ 18 := by rw [D, ← pow_mul, ← pow_mul, Nat.mul_comm]
+
+/-- The source size premise automatically discharges the finite retained-box band's
+admission hypothesis for the block parameters. -/
+theorem boxes_ninth_blocks_of_size (k N : ℕ) (hN : D (9 * k) ^ 18 ≤ N) :
+    ((tiles (189 * k) (9 * k) N).card : ℝ) *
+        ((boxes (189 * k) (9 * k) k).card : ℝ) ≤
+      32 * ((9 * k : ℕ) + 1 : ℝ) * (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  apply boxes_ninth_blocks
+  have h := (bandSize_twentyone_le (9 * k)).trans hN
+  simpa only [show 21 * (9 * k) = 189 * k by omega] using h
+
+/-- All shared band encodings together retain the same finite saving as the boxes and
+queries. The size premise is on the original dimensions; no encoding-cost law is supplied. -/
+theorem encodings_ninth_blocks (k N : ℕ) (hN : D (9 * k) ^ 18 ≤ N) :
+    (numBands (189 * k) (9 * k) N : ℝ) * (10 : ℝ) ^ (189 * k) ≤
+      4 * (N : ℝ) ^ 2 * (9 / 20 : ℝ) ^ k := by
+  let B := numBands (189 * k) (9 * k) N
+  let K0' := K0 (189 * k) (9 * k)
+  let N0' := N0 (189 * k) (9 * k)
+  have heq : 189 * k = 21 * (9 * k) := by omega
+  have hband : K0' * N0' ≤ N := by
+    dsimp only [K0', N0']
+    simpa only [← heq] using (bandSize_twentyone_le (9 * k)).trans hN
+  have hpad : (B : ℝ) * ((K0' : ℝ) * (N0' : ℝ)) ≤ 2 * (N : ℝ) := by
+    have h := padN_le_two_mul (189 * k) (9 * k) N hband
+    change B * (K0' * N0') ≤ 2 * N at h
+    exact_mod_cast h
+  have hK : (21 : ℝ) ^ (9 * k) ≤ 4 * (K0' : ℝ) ^ 2 := by
+    have h := (twentyone_pow_le_choose (9 * k)).trans (K_le_four_mul_K0_sq (21 * (9 * k)) (9 * k))
+    simpa only [K0', heq] using (show (21 : ℝ) ^ (9 * k) ≤
+      4 * (K0 (21 * (9 * k)) (9 * k) : ℝ) ^ 2 by exact_mod_cast h)
+  have hcount : (B : ℝ) ^ 2 * (21 : ℝ) ^ (9 * k) * (N0' : ℝ) ^ 2 ≤
+      16 * (N : ℝ) ^ 2 := by
+    calc (B : ℝ) ^ 2 * (21 : ℝ) ^ (9 * k) * (N0' : ℝ) ^ 2
+        ≤ (B : ℝ) ^ 2 * (4 * (K0' : ℝ) ^ 2) * (N0' : ℝ) ^ 2 := by gcongr
+      _ = 4 * ((B : ℝ) * ((K0' : ℝ) * (N0' : ℝ))) ^ 2 := by ring
+      _ ≤ 4 * (2 * (N : ℝ)) ^ 2 :=
+        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (by positivity) hpad 2) (by norm_num)
+      _ = _ := by ring
+  have hbase : (10 : ℝ) ^ 378 ≤
+      (21 : ℝ) ^ 9 * (3 : ℝ) ^ 360 * (4 : ℝ) ^ 324 * (9 / 20 : ℝ) ^ 2 := by
+    have hn : (10 : ℕ) ^ 378 * 400 ≤ 21 ^ 9 * 3 ^ 360 * 4 ^ 324 * 81 := by
+      decide +kernel
+    rw [show (9 / 20 : ℝ) ^ 2 = 81 / 400 by norm_num,
+      ← mul_div_assoc, le_div_iff₀ (by norm_num)]
+    exact_mod_cast hn
+  have hpowered : (10 : ℝ) ^ (378 * k) ≤ (21 : ℝ) ^ (9 * k) *
+      (3 : ℝ) ^ (360 * k) * (4 : ℝ) ^ (324 * k) * (9 / 20 : ℝ) ^ (2 * k) := by
+    simpa only [mul_pow, ← pow_mul] using pow_le_pow_left₀ (by positivity) hbase k
+  have hT : ((10 : ℝ) ^ (189 * k)) ^ 2 ≤ (21 : ℝ) ^ (9 * k) *
+      (N0' : ℝ) ^ 2 * ((D (9 * k) ^ 18 : ℕ) : ℝ) ^ 2 * ((9 / 20 : ℝ) ^ k) ^ 2 := by
+    have eT : ((10 : ℝ) ^ (189 * k)) ^ 2 = (10 : ℝ) ^ (378 * k) := by
+      rw [← pow_mul]; congr 1; omega
+    have eN0 : (N0' : ℝ) ^ 2 = (3 : ℝ) ^ (360 * k) := by
+      dsimp only [N0', N0]
+      rw [show 189 * k - 9 * k = 180 * k by omega, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul]
+      congr 1
+      omega
+    have eD : ((D (9 * k) ^ 18 : ℕ) : ℝ) ^ 2 = (4 : ℝ) ^ (324 * k) := by
+      rw [D, Nat.cast_pow, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, ← pow_mul]
+      congr 1
+      omega
+    rw [eT, eN0, eD, ← pow_mul, show k * 2 = 2 * k by omega]
+    exact hpowered
+  have hNr : ((D (9 * k) ^ 18 : ℕ) : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
+  have hsq : ((B : ℝ) * (10 : ℝ) ^ (189 * k)) ^ 2 ≤
+      (4 * (N : ℝ) ^ 2 * (9 / 20 : ℝ) ^ k) ^ 2 := by
+    calc ((B : ℝ) * (10 : ℝ) ^ (189 * k)) ^ 2
+        = (B : ℝ) ^ 2 * ((10 : ℝ) ^ (189 * k)) ^ 2 := mul_pow _ _ _
+      _ ≤ (B : ℝ) ^ 2 * ((21 : ℝ) ^ (9 * k) * (N0' : ℝ) ^ 2 *
+          ((D (9 * k) ^ 18 : ℕ) : ℝ) ^ 2 * ((9 / 20 : ℝ) ^ k) ^ 2) :=
+        mul_le_mul_of_nonneg_left hT (by positivity)
+      _ ≤ (B : ℝ) ^ 2 * ((21 : ℝ) ^ (9 * k) * (N0' : ℝ) ^ 2 *
+          (N : ℝ) ^ 2 * ((9 / 20 : ℝ) ^ k) ^ 2) := by gcongr
+      _ = ((B : ℝ) ^ 2 * (21 : ℝ) ^ (9 * k) * (N0' : ℝ) ^ 2) *
+          ((N : ℝ) ^ 2 * ((9 / 20 : ℝ) ^ k) ^ 2) := by ring
+      _ ≤ (16 * (N : ℝ) ^ 2) * ((N : ℝ) ^ 2 * ((9 / 20 : ℝ) ^ k) ^ 2) :=
+        mul_le_mul_of_nonneg_right hcount (by positivity)
+      _ = _ := by ring
+  exact le_of_sq_le_sq hsq (by positivity)
+
+/-- The common finite decay is stronger than a sixteenth-root saving in the original
+inner dimension. This integer-power inequality needs no logarithm approximation. -/
+theorem decay_sixteenth (k : ℕ) :
+    ((9 / 20 : ℝ) ^ k) ^ 16 * (D (9 * k) : ℝ) ≤ 1 := by
+  have hbase : (9 / 20 : ℝ) ^ 16 * (4 : ℝ) ^ 9 ≤ 1 := by norm_num
+  have h := pow_le_pow_left₀ (by positivity) hbase k
+  rw [D, Nat.cast_pow, Nat.cast_ofNat]
+  simpa only [mul_pow, ← pow_mul, Nat.mul_comm, one_pow] using h
+
+private theorem matrix_words_ninth_blocks (k N : ℕ) (hN : D (9 * k) ^ 18 ≤ N) :
+    (N : ℝ) * (D (9 * k) : ℝ) ≤ (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  have hbase : (4 : ℝ) ^ 9 ≤ (4 : ℝ) ^ 162 * (9 / 20 : ℝ) := by norm_num
+  have hpow := pow_le_pow_left₀ (by positivity) hbase k
+  have hD : (D (9 * k) : ℝ) ≤ (9 / 20 : ℝ) ^ k * ((D (9 * k) ^ 18 : ℕ) : ℝ) := by
+    dsimp only [D]
+    push_cast
+    rw [← pow_mul, show 9 * k * 18 = 162 * k by omega]
+    simpa only [mul_pow, ← pow_mul, mul_comm] using hpow
+  have hNr : ((D (9 * k) ^ 18 : ℕ) : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
+  calc (N : ℝ) * (D (9 * k) : ℝ)
+      ≤ (N : ℝ) * ((9 / 20 : ℝ) ^ k * ((D (9 * k) ^ 18 : ℕ) : ℝ)) :=
+        mul_le_mul_of_nonneg_left hD (Nat.cast_nonneg _)
+    _ ≤ (N : ℝ) * ((9 / 20 : ℝ) ^ k * (N : ℝ)) := by gcongr
+    _ = _ := by ring
+
+/-- Every finite term in the native routed-product ledger has a common rational saving.
+The natural expression counts original matrix words, routing occurrences, one shared
+geometry span, all retained tables and every query term. Coefficients of an actual
+instruction ledger can multiply this estimate; no running-time premise is assumed. -/
+theorem nativeShape_ninth_blocks (k N Q : ℕ) (hN : D (9 * k) ^ 18 ≤ N)
+    (hQ : Q * 2 ^ (9 * k) ≤ N ^ 2) :
+    ((1 + N * D (9 * k) + Q + 2 ^ (189 * k) +
+      (numBands (189 * k) (9 * k) N + 1) * 10 ^ (189 * k) +
+      numBands (189 * k) (9 * k) N ^ 2 * ((boxes (189 * k) (9 * k) k).card + 1) +
+      Q * (∑ d ∈ range (k + 1), alpha (9 * k) d) : ℕ) : ℝ) ≤
+      80 * ((9 * k : ℕ) + 1 : ℝ) * (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  let B := numBands (189 * k) (9 * k) N
+  let C := (boxes (189 * k) (9 * k) k).card
+  let gain := (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2
+  have hNpos : 0 < N := (Nat.pow_pos (Nat.pow_pos (by decide))).trans_le hN
+  have hB : 1 ≤ B := numBands_pos (by omega) hNpos
+  have hC : (1 : ℝ) ≤ C := by exact_mod_cast card_boxes_pos (189 * k) (9 * k) k
+  have hND : (N : ℝ) * (D (9 * k) : ℝ) ≤ gain := matrix_words_ninth_blocks k N hN
+  have hunit : 1 ≤ gain := by
+    have hpos : 0 < N * D (9 * k) := Nat.mul_pos hNpos (Nat.pow_pos (by decide))
+    have hone : (1 : ℝ) ≤ (N : ℝ) * (D (9 * k) : ℝ) := by exact_mod_cast hpos
+    exact hone.trans hND
+  have hqueries : (Q : ℝ) * ∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ) ≤ gain :=
+    queries_ninth_blocks k N Q hQ
+  have hprefix : (1 : ℝ) ≤ ∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ) := by
+    have h := Finset.single_le_sum (f := fun d => (alpha (9 * k) d : ℝ))
+      (fun _ _ => Nat.cast_nonneg _) (show 0 ∈ range (k + 1) by simp)
+    simpa only [alpha, Nat.choose_zero_right, pow_zero, Nat.mul_one, Nat.cast_one] using h
+  have hQ' : (Q : ℝ) ≤ gain := by
+    have hstep : (Q : ℝ) ≤ (Q : ℝ) *
+        ∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ) := by
+      simpa only [mul_one] using mul_le_mul_of_nonneg_left hprefix (Nat.cast_nonneg Q)
+    exact hstep.trans hqueries
+  have henc : (B : ℝ) * (10 : ℝ) ^ (189 * k) ≤ 4 * gain := by
+    simpa only [B, gain, mul_assoc, mul_left_comm, mul_comm] using encodings_ninth_blocks k N hN
+  have hspan : (10 : ℝ) ^ (189 * k) ≤ 4 * gain := by
+    have hB' : (1 : ℝ) ≤ B := by exact_mod_cast hB
+    have hstep : (10 : ℝ) ^ (189 * k) ≤ (B : ℝ) * (10 : ℝ) ^ (189 * k) := by
+      simpa only [one_mul] using mul_le_mul_of_nonneg_right hB'
+        (show 0 ≤ (10 : ℝ) ^ (189 * k) by positivity)
+    exact hstep.trans henc
+  have htwo : (2 : ℝ) ^ (189 * k) ≤ 4 * gain :=
+    (pow_le_pow_left₀ (by norm_num) (by norm_num : (2 : ℝ) ≤ 10) _).trans hspan
+  have htables : (B : ℝ) ^ 2 * (C : ℝ) ≤ 32 * ((9 * k : ℕ) + 1 : ℝ) * gain := by
+    simpa only [card_tiles, Nat.cast_pow, gain, mul_assoc] using boxes_ninth_blocks_of_size k N hN
+  have htiles : (B : ℝ) ^ 2 ≤ (B : ℝ) ^ 2 * (C : ℝ) := by
+    simpa only [mul_one] using mul_le_mul_of_nonneg_left hC (sq_nonneg (B : ℝ))
+  have hnonneg : 0 ≤ gain := by dsimp only [gain]; positivity
+  have hm : (0 : ℝ) ≤ (9 * k : ℕ) := Nat.cast_nonneg _
+  push_cast
+  dsimp only [B, C, gain] at *
+  push_cast at htables hm
+  nlinarith only [hunit, hND, hQ', henc, hspan, htwo, htables, htiles, hqueries,
+    mul_nonneg hm hnonneg]
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffExponent.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffExponent.lean
new file mode 100644
index 0000000000..f70bde19f5
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffExponent.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffEncoding
+public import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Tactic.NormNum
+
+/-!
+# An exact rational certificate for exponent 0.064
+
+The integer inequality `9^125*4^72 ≤ 20^125` implies
+`(9/20)^k ≤ (4^(9k))^(-8/125)`. Applied to the checked finite ledger shape, this
+converts its rational decay to an inner-dimension power saving of `0.064`.
+
+This is an original algebraic block-parameter proof of a quantitative step used in
+[AlmanWilliams2026, proof of Corollary 26]. It uses no logarithm approximation or
+source running-time law. Polynomial factors in the depth remain explicit; their
+asymptotic absorption and the final ordinary-3SUM exponent are separate obligations.
+
+## Main results
+
+* `BoxTradeoff.decay_le_rpow`: rational decay bounded by an exact real power.
+* `BoxTradeoff.nativeShape_ninth_blocks_rpow`: the complete finite shape with that power saving.
+-/
+
+public section
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+
+open Finset
+
+/-- The common rational decay gives a `D^(-0.064)` saving at the block parameters.
+The numerical comparison is certified by exact natural-number computation. -/
+theorem decay_le_rpow (k : ℕ) :
+    (9 / 20 : ℝ) ^ k ≤ (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) := by
+  have hD : (0 : ℝ) < D (9 * k) := by exact_mod_cast Nat.pow_pos (by decide : 0 < 4)
+  have hbase : (9 / 20 : ℝ) ^ 125 * (4 : ℝ) ^ 72 ≤ 1 := by
+    have hn : (9 : ℕ) ^ 125 * 4 ^ 72 ≤ 20 ^ 125 := by decide +kernel
+    rw [div_pow, div_mul_eq_mul_div, div_le_one (by positivity)]
+    exact_mod_cast hn
+  have hprod : ((9 / 20 : ℝ) ^ k) ^ 125 * (D (9 * k) : ℝ) ^ 8 ≤ 1 := by
+    have h := pow_le_pow_left₀ (by positivity) hbase k
+    rw [D, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, ← pow_mul,
+      show 9 * k * 8 = 72 * k by omega, show k * 125 = 125 * k by omega]
+    simpa only [mul_pow, ← pow_mul, one_pow] using h
+  have hright : ((D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ))) ^ 125 =
+      ((D (9 * k) : ℝ) ^ 8)⁻¹ := by
+    rw [← Real.rpow_mul_natCast hD.le,
+      show (-(8 / 125 : ℝ)) * ((125 : ℕ) : ℝ) = -(8 : ℝ) by norm_num,
+      Real.rpow_neg hD.le]
+    norm_num
+  apply le_of_pow_le_pow_left₀ (n := 125) (by decide) (by positivity)
+  rw [hright, inv_eq_one_div, le_div_iff₀ (pow_pos hD 8)]
+  exact hprod
+
+/-- The complete finite native-ledger shape has an exact `D^(-0.064)` saving,
+with its depth factor and original dimension/occurrence hypotheses retained. -/
+theorem nativeShape_ninth_blocks_rpow (k N Q : ℕ) (hN : D (9 * k) ^ 18 ≤ N)
+    (hQ : Q * 2 ^ (9 * k) ≤ N ^ 2) :
+    ((1 + N * D (9 * k) + Q + 2 ^ (189 * k) +
+      (numBands (189 * k) (9 * k) N + 1) * 10 ^ (189 * k) +
+      numBands (189 * k) (9 * k) N ^ 2 * ((boxes (189 * k) (9 * k) k).card + 1) +
+      Q * (∑ d ∈ range (k + 1), alpha (9 * k) d) : ℕ) : ℝ) ≤
+      80 * ((9 * k : ℕ) + 1 : ℝ) * (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) *
+        (N : ℝ) ^ 2 := by
+  exact (nativeShape_ninth_blocks k N Q hN hQ).trans
+    (mul_le_mul_of_nonneg_right
+      (mul_le_mul_of_nonneg_left (decay_le_rpow k) (by positivity)) (sq_nonneg _))
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffParameters.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffParameters.lean
new file mode 100644
index 0000000000..6852e1f7ac
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxTradeoffParameters.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+import Mathlib.Tactic.GCongr
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Explicit natural thresholds and a rational finite saving
+
+The source's switch `ceil(m/9)` is computed by the natural expression `(m+8)/9`.
+At the block parameters `m=9k`, `L=189k`, it is exactly `k`. Both the retained boxes
+and all query occurrences then have a common rational decay factor `(9/20)^k`.
+The query estimate needs the occurrence sparsity bound `Q*2^m ≤ N²`, so duplicates
+remain charged. The table estimate needs one band to fit the original dimension.
+
+These are finite specializations of the estimates in `BoxTradeoff`, at the parameters
+used by [AlmanWilliams2026, Corollary 26]. Restricting to multiples of nine makes this
+finite saving algebraic; it is an original specialization of the primary proof rather
+than its full analytic corollary. No total encoding/preprocessing bound or final
+algorithmic exponent is asserted here.
+-/
+
+public section
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+
+open Finset
+
+/-- An executable natural expression for the source's switching order `ceil(m/9)`. -/
+@[expose] def ninthThreshold (m : ℕ) : ℕ := (m + 8) / 9
+
+/-- The executable threshold is within the valid original order range, including `m=0`. -/
+theorem ninthThreshold_le (m : ℕ) : ninthThreshold m ≤ m := by
+  unfold ninthThreshold
+  omega
+
+/-- Nine times the rounded-up threshold covers the original inner depth. -/
+theorem le_nine_mul_ninthThreshold (m : ℕ) : m ≤ 9 * ninthThreshold m := by
+  unfold ninthThreshold
+  omega
+
+/-- The natural expression rounds up by fewer than nine units. -/
+theorem nine_mul_ninthThreshold_lt (m : ℕ) : 9 * ninthThreshold m < m + 9 := by
+  unfold ninthThreshold
+  omega
+
+@[simp] theorem ninthThreshold_nine_mul (k : ℕ) : ninthThreshold (9 * k) = k := by
+  unfold ninthThreshold
+  omega
+
+/-- At block parameters, the per-query finite count has an explicit rational exponential base. -/
+theorem sum_alpha_ninth_blocks (k : ℕ) :
+    ∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ) ≤
+      ((72 : ℝ) * (9 / 8 : ℝ) ^ 9) ^ k := by
+  have h := sum_alpha_le_seventytwo (m := 9 * k) (t := k) (by omega)
+  simpa only [pow_mul, mul_pow] using h
+
+/-- Under the original-occurrence sparsity bound, all sparse query terms share the
+same rational decay factor as the retained-box estimates. No query count is assumed free. -/
+theorem queries_ninth_blocks (k N Q : ℕ) (hQ : Q * 2 ^ (9 * k) ≤ N ^ 2) :
+    (Q : ℝ) * (∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ)) ≤
+      (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  have hQr : (Q : ℝ) * (2 : ℝ) ^ (9 * k) ≤ (N : ℝ) ^ 2 := by exact_mod_cast hQ
+  have he : ((72 : ℝ) * (9 / 8 : ℝ) ^ 9) ^ k =
+      ((72 : ℝ) * (9 / 16 : ℝ) ^ 9) ^ k * (2 : ℝ) ^ (9 * k) := by
+    rw [pow_mul, ← mul_pow]
+    congr 1
+    norm_num
+  have hbase : (72 : ℝ) * (9 / 16 : ℝ) ^ 9 ≤ 9 / 20 := by norm_num
+  calc (Q : ℝ) * (∑ d ∈ range (k + 1), (alpha (9 * k) d : ℝ))
+      ≤ (Q : ℝ) * (((72 : ℝ) * (9 / 8 : ℝ) ^ 9) ^ k) :=
+        mul_le_mul_of_nonneg_left (sum_alpha_ninth_blocks k) (Nat.cast_nonneg _)
+    _ = ((Q : ℝ) * (2 : ℝ) ^ (9 * k)) *
+        (((72 : ℝ) * (9 / 16 : ℝ) ^ 9) ^ k) := by rw [he]; ring
+    _ ≤ (N : ℝ) ^ 2 * (((72 : ℝ) * (9 / 16 : ℝ) ^ 9) ^ k) :=
+      mul_le_mul_of_nonneg_right hQr (by positivity)
+    _ ≤ (N : ℝ) ^ 2 * (9 / 20 : ℝ) ^ k :=
+      mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (by positivity) hbase _) (by positivity)
+    _ = _ := by ring
+
+/-- The all-tile retained-value count has the same rational decay at the block parameters.
+Its explicit band-size premise is weaker than an assumed asymptotic execution bound. -/
+theorem boxes_ninth_blocks (k N : ℕ)
+    (hN : K0 (189 * k) (9 * k) * N0 (189 * k) (9 * k) ≤ N) :
+    ((tiles (189 * k) (9 * k) N).card : ℝ) *
+        ((boxes (189 * k) (9 * k) k).card : ℝ) ≤
+      32 * ((9 * k : ℕ) + 1 : ℝ) * (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  have heq : 189 * k = 21 * (9 * k) := by omega
+  obtain ⟨hrho, hfactor⟩ := rho_twentyone (9 * k)
+  have hpow : rho (21 * (9 * k)) (9 * k) ^ k ≤ (9 / 20 : ℝ) ^ k :=
+    pow_le_pow_left₀ (rho_nonneg (by omega)) hrho.le _
+  have hdecay : rho (189 * k) (9 * k) ^ k / (1 - rho (189 * k) (9 * k)) ≤
+      (9 / 20 : ℝ) ^ k * 2 := by
+    rw [heq, div_eq_mul_one_div]
+    exact mul_le_mul hpow hfactor.le
+      (one_div_nonneg.mpr (by linarith)) (by positivity)
+  have h := total_boxes_le_unpadded (L := 189 * k) (m := 9 * k) (t := k)
+    (by omega) (by omega) hN
+  calc ((tiles (189 * k) (9 * k) N).card : ℝ) *
+        ((boxes (189 * k) (9 * k) k).card : ℝ)
+      ≤ 16 * ((9 * k : ℕ) + 1 : ℝ) *
+          (rho (189 * k) (9 * k) ^ k / (1 - rho (189 * k) (9 * k))) * (N : ℝ) ^ 2 := by
+        simpa only [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_add, Nat.cast_one] using h
+    _ ≤ 16 * ((9 * k : ℕ) + 1 : ℝ) * ((9 / 20 : ℝ) ^ k * 2) * (N : ℝ) ^ 2 := by
+      gcongr
+    _ = _ := by ring
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct.lean
new file mode 100644
index 0000000000..a98e8d162e
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Thin
+
+/-!
+# Routed native box products with one shared geometry
+
+One fixed 160-register standard WordRAM program takes original matrices, raw coordinate
+occurrences and an ordinary threshold. Actual routing computes wanted codes, tile spans
+and a stable permutation. The actual band producer computes shared leaf encodings.
+Box geometry is constructed once; each tile constructs its retained values and executes
+its actual sparse query batch, then copies answers for original-order reconstruction.
+The full original input and outside memory are restored. Signed input and raw nonnegative
+input modes share the same mathematical matrix product; the latter executes conversion.
+
+## Main definitions
+
+* `BoxProduct.program`: complete native routing, shared preparation, all tiles and restoration.
+* `BoxProduct.input`: original matrices/coordinates with an appended ordinary threshold word.
+* `BoxProduct.timeBound`: actual instruction ledger with geometry charged once.
+* `BoxProduct.admissionWidth`: sufficient width from original scalar and magnitude envelopes.
+
+## Main results
+
+* `BoxProduct.exec`: caller-safe actual execution with exact matrix products and complete frame.
+* `BoxProduct.runs_wide`: initialized prefix and charged halt sharing the same answer memory.
+* `BoxProduct.prefix_bounded`: original-input bounds at every wider execution prefix.
+* `BoxProduct.timeBound_le`: complete charged time controlled by the finite work shape.
+* `BoxProduct.runs_thin`: actual initialized thin-product execution with charged finite saving.
+* `BoxProduct.thin_timeBound_rpow`: finite `D^(-8/125)` saving at block parameters,
+  with all polynomial depth factors and original-occurrence sparsity explicit.
+
+The improved finite estimate uses `L=189k`, `m=9k`, `t=k`, `D=4^m`, `D^18≤N`, and
+`Q*2^m≤N²`, where `Q` counts original query occurrences, including duplicates. It adapts
+the finite Section 4 estimates through `BoxTradeoff` and uses an original algebraic block
+specialization. It imports no source machine, solver or runtime law. Polynomial-factor
+absorption, Exact Triangle replacement and ordinary-3SUM exponent 1.9992 remain separate.
+-/
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Admission.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Admission.lean
new file mode 100644
index 0000000000..3315b5f3d8
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Admission.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Layout
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Admission
+
+/-!
+# Original scalar and magnitude admission for routed box products
+
+The same original allocation envelope covers the existing router/producer/copy routines.
+The original matrix-entry magnitude covers both their signed arithmetic and the new
+box-table and sparse-query arithmetic on actual shared band encodings.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM
+
+/-- The old router, producer and reconstruction use a smaller original scalar envelope. -/
+theorem old_fits {W L m t N Q : ℕ} (h : Fits W (wordBudget L m t N Q)) :
+    Fits W (QueriedProduct.wordBudget L m N Q) :=
+  h.of_le (by unfold wordBudget; omega)
+
+/-- Every old signed producer admission follows from the common original-entry envelope. -/
+theorem old_magnitude {w L A : ℕ} (h : magnitudeBound L A < 2 ^ (w - 1)) :
+    QueriedProduct.magnitudeBound L A < 2 ^ (w - 1) := by
+  unfold magnitudeBound at h
+  omega
+
+/-- Original matrix entries admit the new sparse-query envelope for both shared encodings. -/
+theorem box_magnitude {w L A : ℕ} (hw : 0 < w)
+    (h : magnitudeBound L A < 2 ^ (w - 1)) :
+    GenericRAM.Signed.Fits w
+      (BoxQuery.magnitudeBound L (encodedBound L A) (encodedBound L A) : ℕ) := by
+  have hb : BoxQuery.magnitudeBound L (encodedBound L A) (encodedBound L A) <
+      2 ^ (w - 1) := by unfold magnitudeBound at h; omega
+  refine ⟨hw, ?_, by exact_mod_cast hb⟩
+  have hnonneg : 0 ≤
+      (BoxQuery.magnitudeBound L (encodedBound L A) (encodedBound L A) : ℤ) := by positivity
+  have hpow : 0 ≤ (2 : ℤ) ^ (w - 1) := by positivity
+  omega
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Arguments.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Arguments.lean
new file mode 100644
index 0000000000..ebc677743c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Arguments.lean
@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.State
+
+/-!
+# Actual span capture and complete box-ABI restoration
+
+The existing checked native span arithmetic is reused. Its computed low pointers are
+captured before those registers are repurposed, and every scalar read by the retained
+box constructor is restored. Scratch values from earlier queries may be arbitrary.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+private theorem exec_batchArguments {w Q O n R : ℕ} (x : Data 160)
+    (hq : x.regs (QueriedProduct.bank PrunedQuery.queries) = Q)
+    (hn : x.regs (QueriedProduct.bank PrunedQuery.queryCount) = n)
+    (ho : x.regs (QueriedProduct.bank PrunedQuery.output) = O)
+    (hr : x.regs Reg.results = R) (hfit : Fits w (Q + n)) :
+    ∃ y, ExecWithin w batchArguments x y 5 ∧
+      (y.comap boxBank).regs BoxBatch.Reg.next = Q ∧
+      (y.comap boxBank).regs BoxBatch.Reg.stop = Q + n ∧
+      (y.comap boxBank).regs BoxBatch.Reg.output = R ∧
+      y.regs QueriedProduct.Reg.destination = O ∧ y.regs QueriedProduct.Reg.length = n ∧
+      y.mem = x.mem := by
+  change x.regs (13 : Fin 160) = Q at hq
+  change x.regs (14 : Fin 160) = n at hn
+  change x.regs (15 : Fin 160) = O at ho
+  let y := ((((x.set (boxBank BoxBatch.Reg.next) Q).set (boxBank BoxBatch.Reg.stop)
+    (Q + n)).set (boxBank BoxBatch.Reg.output) R).set QueriedProduct.Reg.destination O).set
+      QueriedProduct.Reg.length n
+  have eq : QueriedProduct.bank PrunedQuery.queries = (13 : Fin 160) := rfl
+  have en : QueriedProduct.bank PrunedQuery.queryCount = (14 : Fin 160) := rfl
+  have eo : QueriedProduct.bank PrunedQuery.output = (15 : Fin 160) := rfl
+  have eNext : boxBank BoxBatch.Reg.next = (43 : Fin 160) := rfl
+  have eStop : boxBank BoxBatch.Reg.stop = (44 : Fin 160) := rfl
+  have eOut : boxBank BoxBatch.Reg.output = (45 : Fin 160) := rfl
+  have he : ExecWithin w batchArguments x y 5 := by
+    simp only [batchArguments, eq, en, eo, eNext, eStop, eOut]
+    ram_eval [y, eNext, eStop, eOut, hq, hn, ho, hr, hfit, Reg.results,
+      QueriedProduct.Reg.destination, QueriedProduct.Reg.length, Fin.mk.injEq]
+  refine ⟨y, he, ?_, ?_, ?_, ?_, ?_, rfl⟩
+  all_goals simp [y, Data.comap_regs, boxBank, BoxBatch.Reg.next, BoxBatch.Reg.stop,
+    BoxBatch.Reg.output, QueriedProduct.Reg.destination, QueriedProduct.Reg.length]
+
+private theorem exec_restoreBoxArguments {w L m t N Q AA BB : ℕ} (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N Q x) (hb : Parameters L m t N Q x)
+    (hA : (x.comap QueriedProduct.bank).regs PrunedQuery.arrayA = AA)
+    (hB : (x.comap QueriedProduct.bank).regs PrunedQuery.arrayB = BB)
+    (hfit : Fits w (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin w restoreBoxArguments x y 18 ∧ y.mem = x.mem ∧
+      BoxTable.CatalogueParameters L (m - t) (directoryBase L m N Q)
+        (recordBase L m t N Q) (y.comap boxBank) ∧
+      (y.comap boxBank).regs BoxTable.Reg.inner = m ∧
+      (y.comap boxBank).regs BoxTable.Reg.threshold = t ∧
+      (y.comap boxBank).regs BoxTable.Reg.values = valueBase L m t N Q ∧
+      (y.comap boxBank).regs BoxTable.Reg.count = (boxes L m t).card ∧
+      (y.comap boxBank).regs BoxTable.Reg.arrayA = AA ∧
+      (y.comap boxBank).regs BoxTable.Reg.arrayB = BB := by
+  obtain ⟨c, hc, c0, c1, c10, c9, c3, cm, _⟩ := BoxTable.exec_constants (x.comap boxBank)
+    (hfit.of_le (by unfold wordBudget; omega))
+  let u := c.extend boxBank x
+  have hu := hc.rename boxBank_injective
+  have up : QueriedProduct.Parameters L m N Q u := hp.reframe
+    (fun i hi => boxBank_extend_high c x i (by omega))
+  have ub : Parameters L m t N Q u := hb.extend c
+  have uA : u.regs (QueriedProduct.bank PrunedQuery.arrayA) = AA :=
+    (hu.regs_eq (by decide)).trans hA
+  have uB : u.regs (QueriedProduct.bank PrunedQuery.arrayB) = BB :=
+    (hu.regs_eq (by decide)).trans hB
+  have fH : Fits w (m - t) := hfit.of_le (by unfold wordBudget; omega)
+  have fS : Fits w (m - t + 1) := hfit.of_le (by unfold wordBudget; omega)
+  have fST : Fits w ((m - t + 1) * 10 ^ L) := hfit.of_le (by unfold wordBudget; omega)
+  let v := (((((u.set (boxBank BoxTable.Reg.arrayA) AA).set (boxBank BoxTable.Reg.arrayB) BB).set
+    (boxBank BoxTable.Reg.levels) L).set (boxBank BoxTable.Reg.inner) m).set
+      (boxBank BoxTable.Reg.threshold) t).set (boxBank BoxTable.Reg.height) (m - t)
+  let v₁ := ((((v.set (boxBank BoxTable.Reg.span) (10 ^ L)).set
+    (boxBank BoxTable.Reg.directory) (directoryBase L m N Q)).set
+    (boxBank BoxTable.Reg.records) (recordBase L m t N Q)).set
+    (boxBank BoxTable.Reg.values) (valueBase L m t N Q)).set
+    (boxBank BoxTable.Reg.count) (boxes L m t).card
+  let y := (v₁.set (boxBank BoxTable.Reg.slots) (m - t + 1)).set
+    (boxBank BoxTable.Reg.slots) ((m - t + 1) * 10 ^ L)
+  have eA : boxBank BoxTable.Reg.arrayA = (17 : Fin 160) := rfl
+  have eB : boxBank BoxTable.Reg.arrayB = (18 : Fin 160) := rfl
+  have eL : boxBank BoxTable.Reg.levels = (9 : Fin 160) := rfl
+  have eM : boxBank BoxTable.Reg.inner = (10 : Fin 160) := rfl
+  have eT : boxBank BoxTable.Reg.threshold = (11 : Fin 160) := rfl
+  have eH : boxBank BoxTable.Reg.height = (12 : Fin 160) := rfl
+  have eSpan : boxBank BoxTable.Reg.span = (13 : Fin 160) := rfl
+  have eD : boxBank BoxTable.Reg.directory = (14 : Fin 160) := rfl
+  have eR : boxBank BoxTable.Reg.records = (15 : Fin 160) := rfl
+  have eV : boxBank BoxTable.Reg.values = (16 : Fin 160) := rfl
+  have eK : boxBank BoxTable.Reg.count = (21 : Fin 160) := rfl
+  have eS : boxBank BoxTable.Reg.slots = (19 : Fin 160) := rfl
+  have eOldA : QueriedProduct.bank PrunedQuery.arrayA = (11 : Fin 160) := rfl
+  have eOldB : QueriedProduct.bank PrunedQuery.arrayB = (12 : Fin 160) := rfl
+  change u.regs (11 : Fin 160) = AA at uA
+  change u.regs (12 : Fin 160) = BB at uB
+  have hy : ExecWithin w restoreBoxArguments x y 18 := by
+    simp only [restoreBoxArguments, eA, eB, eL, eM, eT, eH, eSpan, eD, eR, eV, eK, eS, eOldA, eOldB]
+    refine (hu.seq (T₂ := 13) ?_).mono (by omega)
+    change ExecWithin w _ u y 13
+    ram_eval [y, v₁, v, eA, eB, eL, eM, eT, eH, eSpan, eD, eR, eV, eK, eS,
+      up.depth, up.inner, up.leaves, up.one, ub.threshold, ub.directory, ub.records,
+      ub.values, ub.count, uA, uB, fH, fS, fST, Reg.threshold, Reg.directory,
+      Reg.records, Reg.values, Reg.count, QueriedProduct.Reg.depth, QueriedProduct.Reg.inner,
+      QueriedProduct.Reg.leaves, QueriedProduct.Reg.one, Fin.mk.injEq]
+  have eOne : boxBank BoxTable.Reg.one = (32 : Fin 160) := rfl
+  have eTen : boxBank BoxTable.Reg.ten = (33 : Fin 160) := rfl
+  have eNine : boxBank BoxTable.Reg.nine = (34 : Fin 160) := rfl
+  have eThree : boxBank BoxTable.Reg.three = (35 : Fin 160) := rfl
+  have eNil : boxBank BoxTable.Reg.nil = (42 : Fin 160) := rfl
+  have hc0 : u.regs (42 : Fin 160) = 0 := (boxBank_injective.extend_apply _ _ _).trans c0
+  have hc1 : u.regs (32 : Fin 160) = 1 := (boxBank_injective.extend_apply _ _ _).trans c1
+  have hc10 : u.regs (33 : Fin 160) = 10 := (boxBank_injective.extend_apply _ _ _).trans c10
+  have hc9 : u.regs (34 : Fin 160) = 9 := (boxBank_injective.extend_apply _ _ _).trans c9
+  have hc3 : u.regs (35 : Fin 160) = 3 := (boxBank_injective.extend_apply _ _ _).trans c3
+  refine ⟨y, hy, cm, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · constructor
+    all_goals simp [y, v₁, v, Data.comap_regs, eA, eB, eL, eM, eT, eH, eSpan,
+      eD, eR, eV, eK, eS, eOne, eTen, eNine, eThree, eNil, hc0, hc1, hc10, hc9, hc3]
+  all_goals simp [y, v₁, v, Data.comap_regs, eA, eB, eL, eM, eT, eH, eSpan,
+    eD, eR, eV, eK, eS]
+
+set_option maxRecDepth 4096 in
+-- The fixed caller frame check unfolds the existing 32-member 160-register protocol.
+/-- Actual checked span arithmetic and complete box argument restoration, including the
+saved query cursors and real temporary-to-grouped copy arguments. -/
+theorem exec_tileArguments {w L m t N Q j a b : ℕ} (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N Q x) (hb : Parameters L m t N Q x)
+    (hx : x.regs QueriedProduct.Reg.index = j) (hj : j < numBands L m N ^ 2)
+    (ha : x.mem (QueriedProduct.offsetBase L m N Q + j) = a)
+    (hstop : x.mem (QueriedProduct.offsetBase L m N Q + j + 1) = b)
+    (hab : a ≤ b) (hbQ : b ≤ Q) (hfit : Fits w (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin w tileArguments x y 44 ∧
+      QueriedProduct.Parameters L m N Q y ∧ Parameters L m t N Q y ∧ y.mem = x.mem ∧
+      y.regs QueriedProduct.Reg.index = j ∧
+      BoxTable.CatalogueParameters L (m - t) (directoryBase L m N Q)
+        (recordBase L m t N Q) (y.comap boxBank) ∧
+      (y.comap boxBank).regs BoxTable.Reg.inner = m ∧
+      (y.comap boxBank).regs BoxTable.Reg.threshold = t ∧
+      (y.comap boxBank).regs BoxTable.Reg.values = valueBase L m t N Q ∧
+      (y.comap boxBank).regs BoxTable.Reg.count = (boxes L m t).card ∧
+      (y.comap boxBank).regs BoxTable.Reg.arrayA =
+        BandPreparation.catalogueBase L m N + j / numBands L m N * 10 ^ L ∧
+      (y.comap boxBank).regs BoxTable.Reg.arrayB =
+        BandPreparation.catalogueBase L m N +
+          (numBands L m N + j % numBands L m N) * 10 ^ L ∧
+      (y.comap boxBank).regs BoxBatch.Reg.next = QueriedProduct.codeBase L m N Q + a ∧
+      (y.comap boxBank).regs BoxBatch.Reg.stop = QueriedProduct.codeBase L m N Q + b ∧
+      (y.comap boxBank).regs BoxBatch.Reg.output = resultBase L m t N Q ∧
+      y.regs QueriedProduct.Reg.destination = QueriedProduct.groupedBase L m N Q + a ∧
+      y.regs QueriedProduct.Reg.length = b - a := by
+  obtain ⟨u, hu, up, um, ui, _, uL, uA, uB, uq, un, uo, _⟩ :=
+    QueriedProduct.exec_tileArguments x hp hx hj ha hstop hab hbQ (old_fits hfit)
+  have ub : Parameters L m t N Q u := by
+    exact ⟨(hu.regs_eq (by decide)).trans hb.threshold,
+      (hu.regs_eq (by decide)).trans hb.directory, (hu.regs_eq (by decide)).trans hb.records,
+      (hu.regs_eq (by decide)).trans hb.values, (hu.regs_eq (by decide)).trans hb.count,
+      (hu.regs_eq (by decide)).trans hb.results⟩
+  have fq : Fits w (QueriedProduct.codeBase L m N Q + a + (b - a)) := by
+    apply allocated_fits hfit
+    have h10 := Nat.zero_le (10 ^ L)
+    unfold memoryEnd resultBase stackBase valueBase recordBase directoryBase
+      QueriedProduct.memoryEnd QueriedProduct.stampBase QueriedProduct.scratchBase
+      QueriedProduct.outputBase QueriedProduct.groupedBase QueriedProduct.originalBase
+    omega
+  obtain ⟨v, hv, vn, vs, vo, vd, vl, vm⟩ := exec_batchArguments u uq un uo ub.results fq
+  have vp : QueriedProduct.Parameters L m N Q v := up.of_frame (by
+    intro i hi
+    exact hv.regs_eq (by decide +revert))
+  have vb : Parameters L m t N Q v := by
+    exact ⟨(hv.regs_eq (by decide)).trans ub.threshold,
+      (hv.regs_eq (by decide)).trans ub.directory, (hv.regs_eq (by decide)).trans ub.records,
+      (hv.regs_eq (by decide)).trans ub.values, (hv.regs_eq (by decide)).trans ub.count,
+      (hv.regs_eq (by decide)).trans ub.results⟩
+  have vA : (v.comap QueriedProduct.bank).regs PrunedQuery.arrayA = _ :=
+    (hv.regs_eq (by decide)).trans uA
+  have vB : (v.comap QueriedProduct.bank).regs PrunedQuery.arrayB = _ :=
+    (hv.regs_eq (by decide)).trans uB
+  obtain ⟨y, hy, ym, yc, yi, yt, yV, yK, yA, yB⟩ :=
+    exec_restoreBoxArguments v vp vb vA vB hfit
+  have he : ExecWithin w tileArguments x y 44 := hu.seq (hv.seq hy)
+  refine ⟨y, he, hp.of_frame (by intro i hi; exact he.regs_eq (by decide +revert)),
+    ?_, ym.trans (vm.trans um), ?_, yc, yi, yt, yV, yK, yA, yB, ?_, ?_, ?_, ?_, ?_⟩
+  · exact ⟨(he.regs_eq (by decide)).trans hb.threshold,
+      (he.regs_eq (by decide)).trans hb.directory, (he.regs_eq (by decide)).trans hb.records,
+      (he.regs_eq (by decide)).trans hb.values, (he.regs_eq (by decide)).trans hb.count,
+      (he.regs_eq (by decide)).trans hb.results⟩
+  · exact (hy.regs_eq (by decide)).trans ((hv.regs_eq (by decide)).trans ui)
+  · exact (hy.regs_eq (by decide)).trans vn
+  · have hs := (hy.regs_eq (by decide)).trans vs
+    simpa only [Data.comap_regs, Nat.add_assoc, Nat.add_sub_of_le hab] using hs
+  · exact (hy.regs_eq (by decide)).trans vo
+  · exact (hy.regs_eq (by decide)).trans vd
+  · exact (hy.regs_eq (by decide)).trans vl
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Bounds.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Bounds.lean
new file mode 100644
index 0000000000..5480f8caae
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Bounds.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.FrontProgram
+public import Mathlib.Data.Nat.Log
+
+/-!
+# Original-input width admission for routed native box products
+
+A binary ceiling logarithm of original magnitude and allocation envelopes admits the
+whole fixed program. The threshold is data read from the original input; physical
+width is never read. Minimum-width words have an explicit original-input envelope.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM
+
+/-- Sufficient physical width derived from original dimensions, threshold and entry magnitude. -/
+@[expose] def admissionWidth (L m t N Q A : ℕ) : ℕ :=
+  Nat.clog 2 (magnitudeBound L A + wordBudget L m t N Q + 1) + 3
+
+/-- Width admission is positive even for zero-size matrices and zero-magnitude entries. -/
+theorem admissionWidth_pos (L m t N Q A : ℕ) : 0 < admissionWidth L m t N Q A := by
+  unfold admissionWidth
+  omega
+
+/-- Original-input logarithmic admission derives all separate scalar and signed budgets. -/
+theorem admission_bounds {W L m t N Q A : ℕ}
+    (hW : admissionWidth L m t N Q A ≤ W) :
+    0 < W - 2 ∧ magnitudeBound L A < 2 ^ ((W - 2) - 1) ∧
+      Fits W (wordBudget L m t N Q) := by
+  have hl := Nat.le_pow_clog (by decide : 1 < (2 : ℕ))
+    (magnitudeBound L A + wordBudget L m t N Q + 1)
+  have he : Nat.clog 2 (magnitudeBound L A + wordBudget L m t N Q + 1) ≤ (W - 2) - 1 := by
+    unfold admissionWidth at hW
+    omega
+  have hp := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) he
+  refine ⟨by unfold admissionWidth at hW; omega, by omega, ?_⟩
+  change wordBudget L m t N Q < 2 ^ W
+  have hp' := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) (by omega :
+    Nat.clog 2 (magnitudeBound L A + wordBudget L m t N Q + 1) ≤ W)
+  omega
+
+/-- Original-input word/support envelope, independent of larger admitted physical widths. -/
+@[expose] def wordBound (L m t N Q A : ℕ) : ℕ :=
+  16 * (magnitudeBound L A + wordBudget L m t N Q + 1)
+
+/-- Every minimum-admission word is strictly below the same original-input envelope. -/
+theorem pow_admissionWidth_lt_wordBound (L m t N Q A : ℕ) :
+    2 ^ admissionWidth L m t N Q A < wordBound L m t N Q A := by
+  let budget := magnitudeBound L A + wordBudget L m t N Q + 1
+  have hbudget : 1 < budget := by dsimp only [budget]; unfold wordBudget; omega
+  have hl : 0 < Nat.clog 2 budget := Nat.clog_pos (by decide) hbudget
+  have hp := Nat.pow_pred_clog_lt_self (by decide : 1 < (2 : ℕ)) hbudget
+  have he : Nat.clog 2 budget = (Nat.clog 2 budget).pred + 1 :=
+    (Nat.succ_pred_eq_of_pos hl).symm
+  change 2 ^ (Nat.clog 2 budget + 3) < 16 * budget
+  rw [he, show (Nat.clog 2 budget).pred + 1 + 3 = (Nat.clog 2 budget).pred + 4 by omega,
+    pow_add]
+  norm_num only [pow_succ, pow_zero, Nat.reduceMul] at *
+  omega
+
+set_option maxRecDepth 8192 in
+-- This closed structural check traverses both fixed producer/router/box program trees.
+/-- Complete native code, including halt, has constant size independently of all inputs. -/
+theorem program_size_le (bits : Bool) : (program bits).size + 1 ≤ 32768 := by
+  cases bits <;> decide +kernel
+
+set_option maxRecDepth 8192 in
+-- This is a finite syntactic check of the actual renamed kernels in the fixed program.
+/-- Neither input mode reads physical width. -/
+theorem not_readsWidth (bits : Bool) : ¬(program bits).ReadsWidth := by
+  cases bits <;> decide +kernel
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Charges.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Charges.lean
new file mode 100644
index 0000000000..73623339ce
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Charges.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.FrontProgram
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Tactic.Linarith
+
+/-!
+# Original-input instruction ledger for one-geometry box products
+
+One geometry construction is charged before the tile loop. Each tile pays for its
+actual retained values, every wanted occurrence, result copying and loop control.
+Routing, shared encodings, reconstruction and input restoration remain explicit terms.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open scoped BigOperators
+
+/-- Uniform sparse-batch charge for one original wanted-code occurrence. -/
+@[expose] def batchUnit (L m t : ℕ) : ℕ :=
+  258 * (L + 1) * (∑ d ∈ Finset.range (t + 1), alpha m d) + 34
+
+/-- Actual retained table, sparse queries, result copying and outer control for one tile. -/
+@[expose] def tileCharge {N : ℕ} (L m t : ℕ) (qs : List (Fin N × Fin N)) (j : ℕ) : ℕ :=
+  328 * (boxes L m t).card +
+    Nat.count (fun i => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) i = j) qs.length *
+      (batchUnit L m t + 7) + 65
+
+/-- Actual frontend, one shared geometry, all tile calls, reconstruction and input restoration.
+The final halt is charged separately. Every query occurrence contributes to its own tile. -/
+@[expose] def timeBound {N : ℕ} (L m t : ℕ) (qs : List (Fin N × Fin N)) : ℕ :=
+  frontTime L m N qs.length + (BoxTable.geometryTime L m t + 17) +
+    ((∑ j ∈ Finset.range (numBands L m N ^ 2), tileCharge L m t qs j) + 2) +
+    (9 * qs.length + 3) + (7 * QueriedProduct.inputEnd m N qs.length + 12)
+
+private theorem sum_bucket_counts (key : ℕ → ℕ) (Q T : ℕ) :
+    (∑ j ∈ Finset.range T, Nat.count (fun i => key i = j) Q) =
+      Nat.count (fun i => key i < T) Q := by
+  induction T with
+  | zero => simp
+  | succ T ih => rw [Finset.sum_range_succ, ih, CountingSort.count_lt_succ]
+
+/-- Every original occurrence is charged exactly once, even when coordinates repeat. -/
+theorem sum_tileCharge {L m N : ℕ} (hm : m ≤ L) (t : ℕ)
+    (qs : List (Fin N × Fin N)) :
+    (∑ j ∈ Finset.range (numBands L m N ^ 2), tileCharge L m t qs j) =
+      numBands L m N ^ 2 * (328 * (boxes L m t).card + 65) +
+        qs.length * (batchUnit L m t + 7) := by
+  have hkey (i : ℕ) (hi : i < qs.length) :
+      (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) i < numBands L m N ^ 2 :=
+    Wanted.tileKey_lt hm _ (Wanted.inputPairs_lt qs i hi).1 (Wanted.inputPairs_lt qs i hi).2
+  have hcount := sum_bucket_counts (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length
+    (numBands L m N ^ 2)
+  rw [Nat.count_of_forall hkey] at hcount
+  simp only [tileCharge, Finset.sum_add_distrib, Finset.sum_const,
+    Finset.card_range, smul_eq_mul, ← Finset.sum_mul, hcount]
+  ring
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Exec.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Exec.lean
new file mode 100644
index 0000000000..b3c635a9aa
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Exec.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Restore
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Geometry
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Tiles
+
+/-!
+# Complete native routed products using one shared box geometry
+
+Original matrix/coordinate/threshold words suffice for the actual full program. Routing,
+shared encodings, geometry, retained values, sparse query batches and answer reconstruction
+all execute on the same state. The complete original input and outside memory are restored.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+open scoped BigOperators
+
+private theorem buffer_order (L m t N Q : ℕ) :
+    BandPreparation.memoryEnd L m N ≤ directoryBase L m N Q ∧
+    QueriedProduct.snapshotBase L m N Q + QueriedProduct.inputEnd m N Q ≤
+      QueriedProduct.groupedBase L m N Q ∧
+    QueriedProduct.inputEnd m N Q < QueriedProduct.groupedBase L m N Q ∧
+    QueriedProduct.groupedBase L m N Q + Q = QueriedProduct.outputBase L m N Q ∧
+    QueriedProduct.outputBase L m N Q + Q ≤ directoryBase L m N Q ∧
+    directoryBase L m N Q ≤ valueBase L m t N Q ∧
+    valueBase L m t N Q ≤ memoryEnd L m t N Q := by
+  have hs := QueriedProduct.producers_le_snapshot L m N Q
+  have hT := Nat.zero_le (10 ^ L)
+  dsimp only [memoryEnd, resultBase, stackBase, valueBase, recordBase, directoryBase,
+    QueriedProduct.memoryEnd, QueriedProduct.stampBase, QueriedProduct.scratchBase,
+    QueriedProduct.outputBase, QueriedProduct.groupedBase, QueriedProduct.originalBase,
+    QueriedProduct.codeBase, QueriedProduct.offsetBase]
+  omega
+
+/-- One fixed native program computes exact original-order signed matrix products from
+only original words. Neither routing, encoding, box geometry, execution nor time is supplied. -/
+theorem exec {w L m t N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (ht : t ≤ m) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (x : Data 160)
+    (hinput : ∀ a, 0 < a → a < QueriedProduct.inputEnd m N qs.length → x.mem a =
+      (State.init (QueriedProduct.input bits L X Y qs) : State 160).data.mem a)
+    (hthreshold : x.mem (QueriedProduct.inputEnd m N qs.length) = t)
+    (hX : ∀ i k, |X i k| ≤ (A : ℤ)) (hY : ∀ k j, |Y k j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j))
+    (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    ∃ y, ExecWithin (w + 2) (program bits) x y (timeBound L m t qs) ∧
+      QueriedProduct.Parameters L m N qs.length y ∧ y.regs Reg.threshold = t ∧
+      (∀ i : Fin qs.length, y.mem (QueriedProduct.outputBase L m N qs.length + i.val) =
+        Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, ¬(QueriedProduct.inputEnd m N qs.length + 1 ≤ a ∧
+        a < memoryEnd L m t N qs.length) → y.mem a = x.mem a) := by
+  obtain ⟨hBand, hSnap, hInput, hGroup, hOut, hDV, hEnd⟩ := buffer_order L m t N qs.length
+  obtain ⟨r, old, hr, rp, rt, rg, re, rv, ro, rs, rf⟩ :=
+    exec_front hw hm bits X Y qs x hinput hthreshold hX hY hbits hmag hfit
+  obtain ⟨g, hg, gp, gb, gi, gg, gf⟩ := exec_prepareGeometry r rp rt hfit
+  have ggroups : QueriedProduct.SavedGroups L m N qs.length old g.mem :=
+    rg.reframe (fun p hp hb => gf p (by omega))
+  have genc : QueriedProduct.EncodedBands hm X Y g.mem :=
+    re.reframe (fun p hp => gf p (by omega))
+  have gs (j : ℕ) (hj : j < QueriedProduct.inputEnd m N qs.length) :
+      g.mem (QueriedProduct.snapshotBase L m N qs.length + j) = x.mem j := by
+    rw [gf _ (by omega)]
+    exact rs j hj
+  obtain ⟨v, hv, vp, vb, vg, _, _, va, vf⟩ :=
+    exec_evaluateTiles hw hm ht X Y qs old g gp gb gi ggroups genc gg
+      (fun i => (rv i).1) ro hX hY hmag hfit
+  have vs (j : ℕ) (hj : j < QueriedProduct.inputEnd m N qs.length) :
+      v.mem (QueriedProduct.snapshotBase L m N qs.length + j) = x.mem j := by
+    rw [vf _ (by omega) (by omega)]
+    exact gs j hj
+  obtain ⟨o, ho, op, oa, oframe⟩ := QueriedProduct.exec_reconstruct X Y qs old v vp vg
+    (fun i => (rv i).2) va (old_fits hfit)
+  have ot : o.regs Reg.threshold = t := (ho.regs_eq (by decide)).trans vb.threshold
+  have os (j : ℕ) (hj : j < QueriedProduct.inputEnd m N qs.length) :
+      o.mem (QueriedProduct.snapshotBase L m N qs.length + j) = x.mem j := by
+    rw [oframe _ (Or.inl (by omega))]
+    exact vs j hj
+  obtain ⟨y, hy, yp, ym⟩ := exec_restoreInput o op ot hfit
+  refine ⟨y, ?_, yp, (hy.regs_eq (by decide)).trans ot, ?_, ?_⟩
+  · exact (hr.seq (hg.seq (hv.seq (ho.seq hy)))).mono (by unfold timeBound; omega)
+  · intro i
+    rw [ym, Function.update_of_ne (by omega), ArrayCopy.copyPrefix_outside (by omega)]
+    exact oa i
+  · intro a ha
+    by_cases hi : a < QueriedProduct.inputEnd m N qs.length
+    · rw [ym, Function.update_of_ne (by omega)]
+      have hread := ArrayCopy.copyPrefix_read (mem := o.mem)
+        (src := QueriedProduct.snapshotBase L m N qs.length) (dst := 0) hi
+      simpa only [Nat.zero_add] using hread.trans (os a hi)
+    · by_cases heq : a = QueriedProduct.inputEnd m N qs.length
+      · subst a
+        rw [ym, Function.update_self]
+        exact hthreshold.symm
+      · have habove : memoryEnd L m t N qs.length ≤ a := by omega
+        rw [ym, Function.update_of_ne (by omega), ArrayCopy.copyPrefix_outside (by omega),
+          oframe _ (Or.inr (by unfold QueriedProduct.scratchBase; omega)),
+          vf _ (by omega) (by omega), gf _ (by omega), rf _ (Or.inr (by omega))]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Front.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Front.lean
new file mode 100644
index 0000000000..facfbe0611
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Front.lean
@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.FrontProgram
+import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.MatrixInput
+
+
+/-!
+# Correctness of original-input routing and shared band production
+
+The extra readonly parameter pass locates the original threshold. Actual routing and
+matrix adaptation then establish every computed wanted span, stable permutation and
+shared encoding from original words, while retaining the protected input snapshot.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+private theorem exec_thresholdLoad {W L m t N Q : ℕ} (x : Data 160)
+    (hrows : x.regs (QueriedProduct.bank BandPreparation.rows) = N)
+    (hcols : x.regs (QueriedProduct.bank BandPreparation.columns) = D m)
+    (hQ : x.mem 4 = Q) (ht : x.mem (QueriedProduct.inputEnd m N Q) = t)
+    (hfit : Fits W (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin W thresholdLoad x y 9 ∧ y.regs Reg.threshold = t ∧ y.mem = x.mem := by
+  have hI : Fits W (QueriedProduct.inputEnd m N Q) :=
+    hfit.of_le (by unfold wordBudget QueriedProduct.wordBudget; omega)
+  have h4 : Fits W 4 := hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have h5 : Fits W 5 := hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have hprod : Fits W (N * D m) := hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have hdouble : Fits W (N * D m + N * D m) :=
+    hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have hq : Fits W (Q + Q) := hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have hsum : Fits W ((N * D m + N * D m) + (Q + Q)) :=
+    hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  have hsum5 : Fits W ((N * D m + N * D m) + (Q + Q) + 5) :=
+    hI.of_le (by unfold QueriedProduct.inputEnd; omega)
+  let z0 := (x.set QueriedProduct.Reg.address 4).set QueriedProduct.Reg.queryCount Q
+  let z1 := (z0.set QueriedProduct.Reg.address (N * D m)).set QueriedProduct.Reg.address
+    (N * D m + N * D m)
+  let z2 := (z1.set QueriedProduct.Reg.value (Q + Q)).set QueriedProduct.Reg.address
+    ((N * D m + N * D m) + (Q + Q))
+  let z3 := (z2.set QueriedProduct.Reg.value 5).set QueriedProduct.Reg.address
+    (QueriedProduct.inputEnd m N Q)
+  let y := z3.set Reg.threshold t
+  have haddr : (N * D m + N * D m) + (Q + Q) + 5 =
+      QueriedProduct.inputEnd m N Q := by unfold QueriedProduct.inputEnd; omega
+  change x.regs (34 : Fin 160) = N at hrows
+  change x.regs (35 : Fin 160) = D m at hcols
+  have er : QueriedProduct.bank BandPreparation.rows = (34 : Fin 160) := rfl
+  have ec : QueriedProduct.bank BandPreparation.columns = (35 : Fin 160) := rfl
+  have he : ExecWithin W thresholdLoad x y 9 := by
+    simp only [thresholdLoad, er, ec]
+    ram_eval [y, z3, z2, z1, z0, hrows, hcols, hQ, ht, hI,
+      h4, h5, hprod, hdouble, hq, hsum, hsum5, haddr,
+      QueriedProduct.Reg.queryCount, QueriedProduct.Reg.address, QueriedProduct.Reg.value,
+      Reg.threshold, Fin.mk.injEq]
+  exact ⟨y, he, by simp [y], rfl⟩
+
+/-- The actual readonly pass locates and retains the original threshold without changing memory. -/
+theorem exec_loadThreshold {W L m t N Q : ℕ} (hm : m ≤ L) (x : Data 160)
+    (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N)
+    (hQ : x.mem 4 = Q) (ht : x.mem (QueriedProduct.inputEnd m N Q) = t)
+    (hfit : Fits W (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin W loadThreshold x y (thresholdTime L) ∧
+      y.regs Reg.threshold = t ∧ y.mem = x.mem := by
+  obtain ⟨u, hu, up, um, _⟩ := QueriedProduct.exec_parameters hm x hL hmemory hN
+    (old_fits hfit)
+  obtain ⟨y, hy, yt, ym⟩ := exec_thresholdLoad u up.fixed.rows up.columns
+    (by rw [um]; exact hQ) (by rw [um]; exact ht) hfit
+  exact ⟨y, hu.seq hy, yt, ym.trans um⟩
+
+/-- Actual routing and shared encoding production from ordinary original matrix words.
+The returned router memory is an executed proof witness, not an input certificate. -/
+theorem exec_front {w L m t N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (x : Data 160)
+    (hinput : ∀ a, 0 < a → a < QueriedProduct.inputEnd m N qs.length → x.mem a =
+      (State.init (QueriedProduct.input bits L X Y qs) : State 160).data.mem a)
+    (hthreshold : x.mem (QueriedProduct.inputEnd m N qs.length) = t)
+    (hX : ∀ i k, |X i k| ≤ (A : ℤ)) (hY : ∀ k j, |Y k j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j))
+    (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    ∃ (y : Data 160) (old : ℕ → ℕ),
+      ExecWithin (w + 2) (front bits) x y (frontTime L m N qs.length) ∧
+      QueriedProduct.Parameters L m N qs.length y ∧ y.regs Reg.threshold = t ∧
+      QueriedProduct.SavedGroups L m N qs.length old y.mem ∧
+      QueriedProduct.EncodedBands hm X Y y.mem ∧
+      (∀ i : Fin qs.length,
+        old (Wanted.codeAddress L m N qs.length +
+            CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+          (PrunedQuery.queryIndex
+            (outStrOfPos (MaskTable.layout hm) (qs.get i).1 (qs.get i).2)).val ∧
+        old (Wanted.originalAddress L m N qs.length +
+            CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs)
+              qs.length i) = i.val) ∧
+      (∀ j ≤ numBands L m N ^ 2,
+        old (Wanted.offsetAddress L m N qs.length + j) =
+          Nat.count (fun k => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < j) qs.length) ∧
+      (∀ j < QueriedProduct.inputEnd m N qs.length,
+        y.mem (QueriedProduct.snapshotBase L m N qs.length + j) = x.mem j) ∧
+      (∀ p, p < 4 ∨ QueriedProduct.groupedBase L m N qs.length ≤ p → y.mem p = x.mem p) := by
+  have hL : x.mem 1 = L := by
+    rw [hinput 1 (by decide) (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  have hm' : x.mem 2 = m := by
+    rw [hinput 2 (by decide) (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  have hN : x.mem 3 = N := by
+    rw [hinput 3 (by decide) (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  have hQ : x.mem 4 = qs.length := by
+    rw [hinput 4 (by decide) (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  have hqueries (i : ℕ) (hi : i < qs.length) :
+      x.mem (QueriedProduct.queryInputBase m N + 2 * i) = (Wanted.inputPairs qs i).1 ∧
+      x.mem (QueriedProduct.queryInputBase m N + 2 * i + 1) = (Wanted.inputPairs qs i).2 := by
+    have hr := QueriedProduct.input_query_word bits L X Y qs ⟨i, hi⟩ 0
+    have hc := QueriedProduct.input_query_word bits L X Y qs ⟨i, hi⟩ 1
+    rw [hinput _ (by unfold QueriedProduct.queryInputBase; omega) (by
+        simpa only [Nat.add_zero] using QueriedProduct.query_address_lt hi (by decide : 0 < 2)),
+      hinput _ (by unfold QueriedProduct.queryInputBase; omega)
+        (QueriedProduct.query_address_lt hi (by decide : 1 < 2))]
+    rw [Wanted.inputPairs_get qs ⟨i, hi⟩]
+    simpa only [Fin.val_zero, Fin.val_one, Nat.add_zero, ↓reduceIte, Fin.reduceEq] using
+      And.intro hr hc
+  obtain ⟨u, hu, ut, um⟩ := exec_loadThreshold hm x hL hm' hN hQ hthreshold hfit
+  obtain ⟨r, old, hr, rp, rg, rv, ro, rs, rf⟩ :=
+    QueriedProduct.exec_prepareRouting hm qs u (by rw [um]; exact hL)
+      (by rw [um]; exact hm') (by rw [um]; exact hN) (by rw [um]; exact hQ)
+      (by intro i hi; rw [um]; exact hqueries i hi) (old_fits hfit)
+  have rt : r.regs Reg.threshold = t := (hr.regs_eq (by decide)).trans ut
+  have hs := QueriedProduct.producers_le_snapshot L m N qs.length
+  have hsnapshot : QueriedProduct.snapshotBase L m N qs.length +
+      QueriedProduct.inputEnd m N qs.length ≤ QueriedProduct.groupedBase L m N qs.length := by
+    unfold QueriedProduct.groupedBase QueriedProduct.originalBase QueriedProduct.codeBase
+      QueriedProduct.offsetBase
+    omega
+  have rsource (j : ℕ) (hj : j < 2 * (N * D m)) :
+      r.mem (QueriedProduct.snapshotBase L m N qs.length + 5 + j) =
+        (State.init (QueriedProduct.input bits L X Y qs) : State 160).data.mem (5 + j) := by
+    rw [show QueriedProduct.snapshotBase L m N qs.length + 5 + j =
+      QueriedProduct.snapshotBase L m N qs.length + (5 + j) by omega,
+      rs _ (by unfold QueriedProduct.inputEnd; omega), um]
+    exact hinput _ (by omega) (by unfold QueriedProduct.inputEnd; omega)
+  obtain ⟨c, hc, cp, cm, cf⟩ := QueriedProduct.exec_prepareInputMatrices hw bits X Y qs r rp
+    rsource hX hY hbits (old_magnitude hmag) (old_fits hfit)
+  have ct : c.regs Reg.threshold = t := (hc.regs_eq (by cases bits <;> decide)).trans rt
+  have cs (j : ℕ) (hj : j < QueriedProduct.inputEnd m N qs.length) :
+      c.mem (QueriedProduct.snapshotBase L m N qs.length + j) = x.mem j := by
+    rw [cf _ (Or.inr (by unfold QueriedProduct.inputEnd at hs; omega)), rs j hj, um]
+  have cg : QueriedProduct.SavedGroups L m N qs.length old c.mem :=
+    rg.reframe (fun a ha _ => cf a (Or.inr (by
+      unfold QueriedProduct.offsetBase at ha
+      unfold QueriedProduct.inputEnd at hs
+      omega)))
+  obtain ⟨y, hy, yp, yl, yr, yf⟩ := QueriedProduct.exec_bands hw hm X Y c cp
+    (by rw [cf 1 (Or.inl (by decide)), rf 1 (Or.inl (by decide)), um]; exact hL)
+    (by rw [cf 2 (Or.inl (by decide)), rf 2 (Or.inl (by decide)), um]; exact hm')
+    (by rw [cf 3 (Or.inl (by decide)), rf 3 (Or.inl (by decide)), um]; exact hN)
+    cm hX hY (old_magnitude hmag) (old_fits hfit)
+  have yt : y.regs Reg.threshold = t := (hy.regs_eq (by decide)).trans ct
+  have yg : QueriedProduct.SavedGroups L m N qs.length old y.mem :=
+    cg.reframe (fun a ha _ => yf a (Or.inr (by unfold QueriedProduct.offsetBase at ha; omega)))
+  refine ⟨y, old, ?_, yp, yt, yg, ⟨yl, yr⟩, rv, ro, ?_, ?_⟩
+  · exact (hu.seq (hr.seq (hc.seq hy))).mono (by unfold frontTime; omega)
+  · intro j hj
+    rw [yf _ (Or.inr (by omega))]
+    exact cs j hj
+  · intro p hp
+    calc
+      y.mem p = c.mem p := by
+        apply yf
+        rcases hp with hp | hp
+        · exact Or.inl (by unfold BandPreparation.inputEnd; omega)
+        · exact Or.inr (by omega)
+      _ = r.mem p := by
+        apply cf
+        rcases hp with hp | hp
+        · exact Or.inl hp
+        · exact Or.inr (by unfold QueriedProduct.inputEnd at hs; omega)
+      _ = u.mem p := rf p (by rcases hp with hp | hp <;> omega)
+      _ = x.mem p := congrFun um p
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/FrontProgram.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/FrontProgram.lean
new file mode 100644
index 0000000000..4ccbe970fd
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/FrontProgram.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Program
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Input
+
+/-!
+# Original-input routing and shared band production for box products
+
+A preliminary readonly parameter pass locates the appended threshold before the existing
+router reuses low memory. The unchanged routing and band programs compute real tile spans,
+wanted codes, a stable original-index permutation and shared canonical leaf encodings.
+The extra parameter pass and threshold load are charged explicitly.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Locate the final original threshold word using computed matrix dimensions. -/
+@[expose] def thresholdLoad : Code .standard 160 :=
+  let rows := QueriedProduct.bank BandPreparation.rows
+  let columns := QueriedProduct.bank BandPreparation.columns
+  ram[
+    QueriedProduct.Reg.address ← #4;
+    QueriedProduct.Reg.queryCount ← *QueriedProduct.Reg.address;
+    QueriedProduct.Reg.address ← rows * columns;
+    QueriedProduct.Reg.address ← QueriedProduct.Reg.address + QueriedProduct.Reg.address;
+    QueriedProduct.Reg.value ← QueriedProduct.Reg.queryCount + QueriedProduct.Reg.queryCount;
+    QueriedProduct.Reg.address ← QueriedProduct.Reg.address + QueriedProduct.Reg.value;
+    QueriedProduct.Reg.value ← #5;
+    QueriedProduct.Reg.address ← QueriedProduct.Reg.address + QueriedProduct.Reg.value;
+    Reg.threshold ← *QueriedProduct.Reg.address ]
+
+/-- Read the ordinary threshold before either producer mutates the original payload. -/
+@[expose] def loadThreshold : Code .standard 160 :=
+  .seq QueriedProduct.parameters thresholdLoad
+
+/-- Actual original-coordinate routing and actual shared band encodings. -/
+@[expose] def front (bits : Bool) : Code .standard 160 :=
+  .seq loadThreshold (.seq QueriedProduct.prepareRouting
+    (.seq (QueriedProduct.prepareMatrices bits)
+      (BandPreparation.program.rename QueriedProduct.bank)))
+
+/-- Restore the appended original threshold after the unchanged original-prefix restoration. -/
+@[expose] def restoreThreshold : Code .standard 160 := ram[
+  QueriedProduct.Reg.address ← QueriedProduct.Reg.inputSize;
+  *QueriedProduct.Reg.address ← Reg.threshold ]
+
+/-- Both original-prefix restoration and the additional original threshold store are charged. -/
+@[expose] def restoreInput : Code .standard 160 :=
+  .seq QueriedProduct.restoreInput restoreThreshold
+
+/-- Complete fixed native product: real routing/encodings, one geometry construction,
+all retained-table query batches, original-order reconstruction and input restoration. -/
+@[expose] def program (bits : Bool) : Code .standard 160 :=
+  .seq (front bits) (.seq prepareGeometry (.seq evaluateTiles
+    (.seq QueriedProduct.reconstruct restoreInput)))
+
+/-- Readonly preliminary parameter pass and the nine actual threshold-adapter instructions. -/
+@[expose] def thresholdTime (L : ℕ) : ℕ :=
+  ((16 * L + 49) + ((6 * L + 16) * 2 ^ L + 16)) + 9
+
+/-- The charged original routing, actual matrix adaptation and shared encoding preparation. -/
+@[expose] def frontTime (L m N Q : ℕ) : ℕ :=
+  thresholdTime L + QueriedProduct.routingTimeBound L m N Q +
+    (8 * (2 * (N * D m)) + 10) + BandPreparation.timeBound L m N
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Geometry.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Geometry.lean
new file mode 100644
index 0000000000..e3225cf3d4
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Geometry.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.State
+
+
+/-!
+# One actual shared box-geometry construction for all tiles
+
+The constructor consumes original depth, inner count, threshold and an actual directory
+pointer. Its computed records, retained-value base and compact count are saved in the high
+bank. No assumed table or geometry execution is supplied to this stage.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+set_option maxRecDepth 4096 in
+-- Fixed 160-register frame checks unfold the existing 32-member caller register set.
+/-- Construct shared geometry exactly once, save its actual addresses/count and initialize
+the reusable sparse-result allocation and tile index. -/
+theorem exec_prepareGeometry {w L m t N Q : ℕ} (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N Q x) (ht : x.regs Reg.threshold = t)
+    (hfit : Fits w (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin w prepareGeometry x y (BoxTable.geometryTime L m t + 17) ∧
+      QueriedProduct.Parameters L m N Q y ∧ Parameters L m t N Q y ∧
+      y.regs QueriedProduct.Reg.index = 0 ∧ Geometry L m t N Q y.mem ∧
+      (∀ p, ¬(directoryBase L m N Q ≤ p ∧ p < valueBase L m t N Q) →
+        y.mem p = x.mem p) := by
+  let D := directoryBase L m N Q
+  let R := recordBase L m t N Q
+  let V := valueBase L m t N Q
+  let K := (boxes L m t).card
+  let u := ((((x.set Reg.directory D).set (boxBank BoxTable.Reg.levels) L).set
+    (boxBank BoxTable.Reg.inner) m).set (boxBank BoxTable.Reg.threshold) t).set
+      (boxBank BoxTable.Reg.directory) D
+  have hu : ExecWithin w geometryHead x u 5 := by
+    ram_eval [geometryHead, u, D, directoryBase, hp.memoryLimit, hp.depth, hp.inner, ht,
+      boxBank, Reg.directory, Reg.threshold, BoxTable.Reg.levels, BoxTable.Reg.inner,
+      BoxTable.Reg.threshold, BoxTable.Reg.directory, Fin.mk.injEq, Fin.val_ofNat, Fin.val_natCast]
+  have hT : 10 ^ L ≤ (L + 1) * 10 ^ L := Nat.le_mul_of_pos_left _ (by omega)
+  have up : QueriedProduct.Parameters L m N Q u := hp.of_frame (by
+    intro i hi
+    exact hu.regs_eq (by decide +revert))
+  obtain ⟨z, hz, zp, zK, zV, zcat⟩ := BoxTable.exec_geometry (L := L) (m := m) (t := t) (D := D)
+      (u.comap boxBank)
+    (by simp [u, boxBank, BoxTable.Reg.levels, BoxTable.Reg.inner,
+      BoxTable.Reg.threshold, BoxTable.Reg.directory, Reg.directory])
+    (by simp [u, boxBank, BoxTable.Reg.inner, BoxTable.Reg.threshold,
+      BoxTable.Reg.directory, Reg.directory])
+    (by simp [u, boxBank, BoxTable.Reg.threshold, BoxTable.Reg.directory])
+    (by simp [u, boxBank])
+    (hfit.of_le (by unfold wordBudget; dsimp only [D]; omega))
+  let v := z.extend boxBank u
+  have hv := hz.rename boxBank_injective
+  have vp : QueriedProduct.Parameters L m N Q v := up.reframe
+    (fun i hi => boxBank_extend_high z u i (by omega))
+  have vR : v.regs ⟨15, by decide⟩ = R := by
+    exact (boxBank_injective.extend_apply _ _ _).trans zp.records
+  have vV : v.regs ⟨16, by decide⟩ = V := by
+    exact (boxBank_injective.extend_apply _ _ _).trans zV
+  have vK : v.regs ⟨21, by decide⟩ = K := by
+    exact (boxBank_injective.extend_apply _ _ _).trans zK
+  have vt : v.regs Reg.threshold = t :=
+    (boxBank_extend_high z u _ (by decide)).trans ((hu.regs_eq (by decide)).trans ht)
+  have vD : v.regs Reg.directory = D := by
+    rw [boxBank_extend_high z u _ (by decide)]
+    simp [u, Reg.directory, boxBank, BoxTable.Reg.levels, BoxTable.Reg.inner,
+      BoxTable.Reg.threshold, BoxTable.Reg.directory]
+  have f10 : Fits w 10 := hfit.of_le (by unfold wordBudget; omega)
+  have f5 : Fits w 5 := hfit.of_le (by unfold wordBudget; omega)
+  have fL : Fits w (L + 1) := hfit.of_le (by unfold wordBudget; omega)
+  have fT : Fits w ((L + 1) * 10 ^ L) := hfit.of_le (by unfold wordBudget; omega)
+  have fC : Fits w ((L + 1) * 10 ^ L + 10) := hfit.of_le (by unfold wordBudget; omega)
+  have fS : Fits w (((L + 1) * 10 ^ L + 10) * 5) := hfit.of_le (by
+    unfold wordBudget; omega)
+  have fV : Fits w (((L + 1) * 10 ^ L + 10) * 5 + V) := hfit.of_le (by
+    unfold wordBudget; dsimp only [V]; omega)
+  have fK : Fits w (((L + 1) * 10 ^ L + 10) * 5 + V + K) := by
+    apply allocated_fits hfit
+    unfold memoryEnd resultBase stackBase BoxQuery.stackCapacity
+    dsimp only [V, K]
+    omega
+  let y₀ := ((v.set Reg.records R).set Reg.values V).set Reg.count K
+  let y₁ := (y₀.set Reg.results (L + 1)).set Reg.results ((L + 1) * 10 ^ L)
+  let y₂ := (y₁.set QueriedProduct.Reg.temporary 10).set Reg.results
+    ((L + 1) * 10 ^ L + 10)
+  let y₃ := (y₂.set QueriedProduct.Reg.temporary 5).set Reg.results
+    (((L + 1) * 10 ^ L + 10) * 5)
+  let y := ((y₃.set Reg.results (((L + 1) * 10 ^ L + 10) * 5 + V)).set
+    Reg.results (((L + 1) * 10 ^ L + 10) * 5 + V + K)).set QueriedProduct.Reg.index 0
+  have eR : boxBank BoxTable.Reg.records = (15 : Fin 160) := rfl
+  have eV : boxBank BoxTable.Reg.values = (16 : Fin 160) := rfl
+  have eK : boxBank BoxTable.Reg.count = (21 : Fin 160) := rfl
+  change v.regs (15 : Fin 160) = R at vR
+  change v.regs (16 : Fin 160) = V at vV
+  change v.regs (21 : Fin 160) = K at vK
+  have hy : ExecWithin w geometryFinish v y 12 := by
+    simp only [geometryFinish, eR, eV, eK]
+    ram_eval [y, y₀, y₁, y₂, y₃, vR, vV, vK, vp.depth, vp.one, vp.leaves,
+      f10, f5, fL, fT, fC, fS, fV, fK, Reg.records, Reg.values,
+      Reg.count, Reg.results, QueriedProduct.Reg.depth, QueriedProduct.Reg.one,
+      QueriedProduct.Reg.leaves, QueriedProduct.Reg.temporary, QueriedProduct.Reg.index,
+      Fin.mk.injEq]
+  have yp : QueriedProduct.Parameters L m N Q y := vp.of_frame (by
+    intro i hi
+    exact hy.regs_eq (by decide +revert))
+  refine ⟨y, (hu.seq (hv.seq hy)).mono (by unfold BoxTable.geometryTime; omega), yp,
+    ?_, by simp [y], ?_, ?_⟩
+  · constructor
+    · exact (hy.regs_eq (by decide)).trans vt
+    · exact (hy.regs_eq (by decide)).trans vD
+    · simp [y, y₀, y₁, y₂, y₃, Reg.records, Reg.values, Reg.count, Reg.results,
+        QueriedProduct.Reg.temporary, QueriedProduct.Reg.index, R]
+    · simp [y, y₀, y₁, y₂, y₃, Reg.records, Reg.values, Reg.count, Reg.results,
+        QueriedProduct.Reg.temporary,
+        QueriedProduct.Reg.index, V]
+    · simp [y, y₀, y₁, y₂, y₃, Reg.records, Reg.values, Reg.count, Reg.results,
+        QueriedProduct.Reg.temporary,
+        QueriedProduct.Reg.index, K]
+    · simp [y, y₀, y₁, y₂, y₃, Reg.results, Reg.records, Reg.values, Reg.count,
+        QueriedProduct.Reg.index, QueriedProduct.Reg.temporary, resultBase, stackBase,
+        BoxQuery.stackCapacity, V, K, Nat.add_assoc, Nat.add_comm,
+        Nat.mul_comm]
+  · exact ⟨zcat.directory, zcat.code, zcat.stars, zcat.stride⟩
+  · intro p hp
+    apply zcat.frame p
+    · simp only [D] at *
+      unfold valueBase recordBase at hp
+      omega
+    · rw [BoxTable.count_eligible_eq_card_boxes]
+      simp only [D]
+      unfold valueBase recordBase at hp
+      omega
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Input.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Input.lean
new file mode 100644
index 0000000000..c42222e86b
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Input.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Admission
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Input
+import Mathlib.Data.List.GetD
+
+/-!
+# Original matrix, coordinate and threshold input for a box product
+
+The existing four headers, both original matrices and coordinate occurrences retain
+their input addresses. One final word contains the ordinary box threshold. The actual
+program reads that word before either producer reuses the original low-memory payload.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Original matrix/coordinate words, followed by one ordinary threshold word. -/
+@[expose] def input {m N : ℕ} (bits : Bool) (L t : ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) : List ℕ := QueriedProduct.input bits L X Y qs ++ [t]
+
+/-- Every original word, including the threshold and native length header, has this extent. -/
+theorem input_length {m N : ℕ} (bits : Bool) (L t : ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) :
+    (input bits L t X Y qs).length = QueriedProduct.inputEnd m N qs.length := by
+  simpa only [input, List.length_append, List.length_singleton] using
+    QueriedProduct.input_length bits L X Y qs
+
+/-- Appending the threshold preserves every original positive-address matrix/coordinate word.
+Address zero instead records the new literal input length. -/
+theorem input_prefix {L m t N : ℕ} (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (p : ℕ) (hp : 0 < p)
+    (hbound : p < QueriedProduct.inputEnd m N qs.length) :
+    (State.init (input bits L t X Y qs) : State 160).data.mem p =
+      (State.init (QueriedProduct.input bits L X Y qs) : State 160).data.mem p := by
+  obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : p ≠ 0)
+  change (Data.init (input bits L t X Y qs) : Data 160).mem (k + 1) = _
+  rw [Data.init_mem_succ]
+  change (QueriedProduct.input bits L X Y qs ++ [t]).getD k 0 =
+    (Data.init (QueriedProduct.input bits L X Y qs) : Data 160).mem (k + 1)
+  rw [Data.init_mem_succ]
+  exact List.getD_append _ _ _ _ (by
+    have := QueriedProduct.input_length bits L X Y qs
+    omega)
+
+/-- The final original word contains precisely the supplied threshold. -/
+theorem input_threshold {L m t N : ℕ} (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) :
+    (State.init (input bits L t X Y qs) : State 160).data.mem
+      (QueriedProduct.inputEnd m N qs.length) = t := by
+  rw [← QueriedProduct.input_length bits L X Y qs]
+  change (Data.init (input bits L t X Y qs) : Data 160).mem
+    ((QueriedProduct.input bits L X Y qs).length + 1) = t
+  rw [Data.init_mem_succ]
+  simp [input]
+
+/-- All original words fit from original dimensions, threshold and entry magnitudes. -/
+theorem input_fits {w L m t N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hX : ∀ i k, |X i k| ≤ (A : ℤ))
+    (hY : ∀ k j, |Y k j| ≤ (A : ℤ)) (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    InputFits (w + 2) (input bits L t X Y qs) := by
+  have hold := QueriedProduct.input_fits hw hm bits X Y qs hX hY
+    (old_magnitude hmag) (old_fits hfit)
+  constructor
+  · rw [input_length]
+    exact hfit.of_le (by unfold wordBudget QueriedProduct.wordBudget; omega)
+  · intro v hv
+    rcases List.mem_append.mp hv with hv | hv
+    · exact hold.2 v hv
+    · have hv' : v = t := by simpa only [List.mem_singleton] using hv
+      subst v
+      exact hfit.of_le (by unfold wordBudget; omega)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Layout.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Layout.lean
new file mode 100644
index 0000000000..21c8d147d2
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Layout.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxBatch
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Catalogue
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Routing
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Reconstruct
+
+/-!
+# Allocation and original-input bounds for routed box products
+
+Existing native routing, shared band encodings and original-order answer buffers are
+reused unchanged. One box directory and compact catalogue follow that caller's allocation.
+The retained values and sparse work stack are reused by all tiles; a temporary answer
+array follows the stack. Actual native copies deliver each tile's answers to the protected
+grouped buffer before the next tile overwrites the retained values.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- First shared box-directory word, above every existing producer/caller buffer. -/
+@[expose] def directoryBase (L m N Q : ℕ) : ℕ := QueriedProduct.memoryEnd L m N Q
+
+/-- Compact geometry follows all shared directory slots. -/
+@[expose] def recordBase (L m t N Q : ℕ) : ℕ :=
+  directoryBase L m N Q + (m - t + 1) * 10 ^ L
+
+/-- Each tile's retained signed values follow the compact three-word geometry. -/
+@[expose] def valueBase (L m t N Q : ℕ) : ℕ :=
+  recordBase L m t N Q + 3 * (boxes L m t).card
+
+/-- Reusable sparse-query stack, beyond all retained values. -/
+@[expose] def stackBase (L m t N Q : ℕ) : ℕ :=
+  valueBase L m t N Q + (boxes L m t).card
+
+/-- Reusable temporary answers, copied into the actual grouped span after each tile. -/
+@[expose] def resultBase (L m t N Q : ℕ) : ℕ :=
+  stackBase L m t N Q + 5 * BoxQuery.stackCapacity L
+
+/-- One past every possible write, including the largest temporary answer span. -/
+@[expose] def memoryEnd (L m t N Q : ℕ) : ℕ := resultBase L m t N Q + Q
+
+/-- Original matrix entries bound all shared encoding operands. -/
+@[expose] def encodedBound (L A : ℕ) : ℕ := 7 ^ L * A
+
+/-- One original-entry magnitude envelope covers both the existing producer and sparse boxes. -/
+@[expose] def magnitudeBound (L A : ℕ) : ℕ :=
+  QueriedProduct.magnitudeBound L A +
+    BoxQuery.magnitudeBound L (encodedBound L A) (encodedBound L A)
+
+/-- Original scalar/allocation envelope; no intermediate-state fit certificate is an input. -/
+@[expose] def wordBudget (L m t N Q : ℕ) : ℕ :=
+  10000 * (QueriedProduct.wordBudget L m N Q + memoryEnd L m t N Q +
+    directoryBase L m N Q + recordBase L m t N Q + valueBase L m t N Q +
+    (m - t + 1) * 10 ^ L + (L + 1) * 10 ^ L + L + m + t + N + Q + 64)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Program.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Program.lean
new file mode 100644
index 0000000000..3b919cd536
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Program.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Layout
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Arguments
+
+/-!
+# One-geometry native box-product controller
+
+The existing producer and router keep their 160-register caller protocol. Six unused
+high registers retain the ordinary threshold and actual box geometry between tile calls.
+Every tile reloads the low box bank, constructs its retained values, executes all wanted
+queries, and copies temporary answers into the protected grouped buffer.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM
+
+/-- Reuse the unchanged fixed box kernels in the caller's low register bank. -/
+@[expose] def boxBank (i : Fin 64) : Fin 160 := ⟨i.val, by omega⟩
+
+theorem boxBank_injective : Function.Injective boxBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun i : Fin 160 => i.val) h)
+
+namespace Reg
+
+/-- Ordinary original threshold, retained before low-memory producer reuse. -/
+abbrev threshold : Fin 160 := 147
+/-- Actual shared box-directory base. -/
+abbrev directory : Fin 160 := 148
+/-- Actual compact descriptor base. -/
+abbrev records : Fin 160 := 149
+/-- Actual reusable signed value-table base. -/
+abbrev values : Fin 160 := 150
+/-- Actual computed compact box count. -/
+abbrev count : Fin 160 := 151
+/-- Actual reusable temporary-answer base, above the work stack. -/
+abbrev results : Fin 160 := 152
+
+end Reg
+
+/-- Supply original scalars to the actual geometry constructor. -/
+@[expose] def geometryHead : Code .standard 160 :=
+  let L := boxBank BoxTable.Reg.levels
+  let m := boxBank BoxTable.Reg.inner
+  let t := boxBank BoxTable.Reg.threshold
+  let D := boxBank BoxTable.Reg.directory
+  ram[ Reg.directory ← QueriedProduct.Reg.memoryLimit;
+    L ← QueriedProduct.Reg.depth; m ← QueriedProduct.Reg.inner;
+    t ← Reg.threshold; D ← Reg.directory ]
+
+/-- Retain the computed geometry and initialize the actual tile index and temporary answers. -/
+@[expose] def geometryFinish : Code .standard 160 :=
+  let R := boxBank BoxTable.Reg.records
+  let V := boxBank BoxTable.Reg.values
+  let K := boxBank BoxTable.Reg.count
+  ram[ Reg.records ← R; Reg.values ← V; Reg.count ← K;
+    Reg.results ← QueriedProduct.Reg.depth + QueriedProduct.Reg.one;
+    Reg.results ← Reg.results * QueriedProduct.Reg.leaves;
+    QueriedProduct.Reg.temporary ← #10;
+    Reg.results ← Reg.results + QueriedProduct.Reg.temporary;
+    QueriedProduct.Reg.temporary ← #5;
+    Reg.results ← Reg.results * QueriedProduct.Reg.temporary;
+    Reg.results ← Reg.results + Reg.values; Reg.results ← Reg.results + Reg.count;
+    QueriedProduct.Reg.index ← #0 ]
+
+/-- Construct the real geometry once, before the entire tile loop. -/
+@[expose] def prepareGeometry : Code .standard 160 :=
+  .seq geometryHead (.seq (BoxTable.geometry.rename boxBank) geometryFinish)
+
+/-- Restore every low scalar read by the retained-value constructor after ordinary span setup. -/
+@[expose] def restoreBoxArguments : Code .standard 160 :=
+  let L := boxBank BoxTable.Reg.levels
+  let m := boxBank BoxTable.Reg.inner
+  let t := boxBank BoxTable.Reg.threshold
+  let H := boxBank BoxTable.Reg.height
+  let T := boxBank BoxTable.Reg.span
+  let D := boxBank BoxTable.Reg.directory
+  let R := boxBank BoxTable.Reg.records
+  let V := boxBank BoxTable.Reg.values
+  let K := boxBank BoxTable.Reg.count
+  let A := boxBank BoxTable.Reg.arrayA
+  let B := boxBank BoxTable.Reg.arrayB
+  let S := boxBank BoxTable.Reg.slots
+  let oldA := QueriedProduct.bank PrunedQuery.arrayA
+  let oldB := QueriedProduct.bank PrunedQuery.arrayB
+  ram[ ⟪BoxTable.constants.rename boxBank⟫; A ← oldA; B ← oldB;
+    L ← QueriedProduct.Reg.depth; m ← QueriedProduct.Reg.inner; t ← Reg.threshold;
+    H ← m - t; T ← QueriedProduct.Reg.leaves; D ← Reg.directory;
+    R ← Reg.records; V ← Reg.values; K ← Reg.count;
+    S ← H + QueriedProduct.Reg.one; S ← S * T ]
+
+/-- Save the computed low ABI before its registers are reused by the box constructor. -/
+@[expose] def batchArguments : Code .standard 160 :=
+  let next := boxBank BoxBatch.Reg.next
+  let stop := boxBank BoxBatch.Reg.stop
+  let output := boxBank BoxBatch.Reg.output
+  let queries := QueriedProduct.bank PrunedQuery.queries
+  let count := QueriedProduct.bank PrunedQuery.queryCount
+  let answers := QueriedProduct.bank PrunedQuery.output
+  ram[ next ← queries; stop ← queries + count; output ← Reg.results;
+    QueriedProduct.Reg.destination ← answers; QueriedProduct.Reg.length ← count ]
+
+/-- Reuse actual span/pointer arithmetic, retain the real cursors and fully restore the box ABI. -/
+@[expose] def tileArguments : Code .standard 160 :=
+  .seq QueriedProduct.tileArguments (.seq batchArguments restoreBoxArguments)
+
+/-- Actual temporary-result copy, retaining the original protected grouped-answer layout. -/
+@[expose] def copyResults : Code .standard 160 :=
+  .seq (ram[ QueriedProduct.Reg.source ← Reg.results ]) QueriedProduct.copyCall
+
+/-- One native retained table, all sparse queries in its real span, and actual answer delivery. -/
+@[expose] def tileStep : Code .standard 160 :=
+  .seq tileArguments (.seq (BoxTable.tile.rename boxBank)
+    (.seq (BoxBatch.queryProgram.rename boxBank)
+      (.seq copyResults (ram[
+        QueriedProduct.Reg.index ← QueriedProduct.Reg.index + QueriedProduct.Reg.one ]))))
+
+/-- All tiles use the same compact geometry and reusable value/query/result allocation. -/
+@[expose] def evaluateTiles : Code .standard 160 :=
+  .loop (.lt QueriedProduct.Reg.index QueriedProduct.Reg.tiles) tileStep
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Resources.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Resources.lean
new file mode 100644
index 0000000000..bdbced3699
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Resources.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Charges
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffExponent
+import Mathlib.Tactic.Linarith
+
+/-!
+# Complete finite work bound for the actual routed box-product ledger
+
+The actual charge is polynomial in depth times original matrix/input work, shared
+encodings, all retained boxes and every sparse query occurrence. At block parameters
+`L=189k`, `m=9k`, `t=k`, finite estimates give the improved geometric saving. The bound
+includes the final halt; conversion to an end-to-end 3SUM exponent remains separate.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Original finite work of input/routing, shared encodings, all retained tiles and queries. -/
+@[expose] def workShape (L m t N Q : ℕ) : ℕ :=
+  1 + N * D m + Q + 2 ^ L + (numBands L m N + 1) * 10 ^ L +
+    numBands L m N ^ 2 * ((boxes L m t).card + 1) +
+    Q * (∑ d ∈ Finset.range (t + 1), alpha m d)
+
+private theorem frontTime_le (L m N Q : ℕ) :
+    frontTime L m N Q + (9 * Q + 3) + (7 * QueriedProduct.inputEnd m N Q + 12) + 1 ≤
+      16384 * (L + 1) *
+        (1 + N * D m + Q + 2 ^ L + (numBands L m N + 1) * 10 ^ L + numBands L m N ^ 2) := by
+  unfold frontTime thresholdTime QueriedProduct.routingTimeBound Wanted.timeBound
+    BandPreparation.timeBound QueriedProduct.inputEnd
+  nlinarith only [Nat.zero_le L, Nat.zero_le (2 ^ L), Nat.zero_le (10 ^ L),
+    Nat.zero_le (L * 10 ^ L), Nat.zero_le (N * D m), Nat.zero_le (L * (N * D m)),
+    Nat.zero_le Q, Nat.zero_le (L * Q), Nat.zero_le (L * 2 ^ L),
+    Nat.zero_le (numBands L m N * 10 ^ L), Nat.zero_le (L * (numBands L m N * 10 ^ L)),
+    Nat.zero_le (numBands L m N ^ 2), Nat.zero_le (L * numBands L m N ^ 2)]
+
+/-- The complete native ledger, including halt, has one shared preparation term and
+occurrence-sensitive sparse work. No source running-time law is assumed. -/
+theorem timeBound_le {L m N : ℕ} (hm : m ≤ L) (t : ℕ) (qs : List (Fin N × Fin N)) :
+    timeBound L m t qs + 1 ≤ 32768 * (L + 1) ^ 2 * workShape L m t N qs.length := by
+  let S := workShape L m t N qs.length
+  let G := (L + 1) ^ 2
+  have hG : 1 ≤ G := by dsimp only [G]; nlinarith only [Nat.zero_le L]
+  have hLG : L + 1 ≤ G := by dsimp only [G]; nlinarith only [Nat.zero_le L]
+  have hS : 1 ≤ S := by
+    apply Nat.succ_le_of_lt
+    dsimp only [S, workShape]
+    positivity
+  have hF : 1 + N * D m + qs.length + 2 ^ L + (numBands L m N + 1) * 10 ^ L +
+      numBands L m N ^ 2 ≤ S := by
+    have hmul : numBands L m N ^ 2 ≤
+        numBands L m N ^ 2 * ((boxes L m t).card + 1) := by
+      simpa only [Nat.mul_one] using Nat.mul_le_mul_left (numBands L m N ^ 2)
+        (show 1 ≤ (boxes L m t).card + 1 by omega)
+    exact (Nat.add_le_add_left hmul _).trans (Nat.le_add_right _ _)
+  have hT : 10 ^ L ≤ S := by
+    have hmul : 10 ^ L ≤ (numBands L m N + 1) * 10 ^ L :=
+      Nat.le_mul_of_pos_left _ (by omega)
+    exact hmul.trans ((Nat.le_add_left _ _).trans
+      ((Nat.le_add_right _ _).trans (Nat.le_add_right _ _)))
+  have hB : numBands L m N ^ 2 * ((boxes L m t).card + 1) ≤ S :=
+    (Nat.le_add_left _ _).trans (Nat.le_add_right _ _)
+  have hQ : qs.length ≤ S :=
+    (Nat.le_add_left _ _).trans ((Nat.le_add_right _ _).trans
+      ((Nat.le_add_right _ _).trans ((Nat.le_add_right _ _).trans (Nat.le_add_right _ _))))
+  have hA : qs.length * (∑ d ∈ Finset.range (t + 1), alpha m d) ≤ S :=
+    Nat.le_add_left _ _
+  have hf := (frontTime_le L m N qs.length).trans
+    (Nat.mul_le_mul (Nat.mul_le_mul_left _ hLG) hF)
+  have hg := (BoxTable.geometryTime_le L m t hm).trans
+    (Nat.mul_le_mul_left (64 * G) hT)
+  have ht : numBands L m N ^ 2 * (328 * (boxes L m t).card + 65) ≤ 328 * G * S := by
+    calc _ ≤ 328 * (numBands L m N ^ 2 * ((boxes L m t).card + 1)) := by
+              nlinarith only [Nat.zero_le (numBands L m N ^ 2)]
+         _ ≤ 328 * S := Nat.mul_le_mul_left _ hB
+         _ ≤ 328 * G * S := by nlinarith only [Nat.mul_le_mul_right (328 * S) hG]
+  have hqa : qs.length * (batchUnit L m t + 7) ≤ 299 * G * S := by
+    have hA' := Nat.mul_le_mul (Nat.mul_le_mul_left 258 hLG) hA
+    have hQ' := Nat.mul_le_mul_left 41 hQ
+    have hQS := Nat.mul_le_mul_right (41 * S) hG
+    unfold batchUnit
+    nlinarith only [hA', hQ', hQS]
+  have hunit : 1 ≤ G * S := by
+    simpa only [Nat.one_mul] using Nat.mul_le_mul hG hS
+  unfold timeBound
+  rw [sum_tileCharge hm t qs]
+  change _ ≤ 32768 * G * S
+  simp only [Nat.mul_assoc] at hf hg ht hqa ⊢
+  omega
+
+/-- Complete native work, including halt, at the algebraic block parameters. The saving
+charges every original occurrence and includes all routing, encodings and shared preparation. -/
+theorem thin_timeBound (k N : ℕ) (qs : List (Fin N × Fin N))
+    (hN : D (9 * k) ^ 18 ≤ N) (hQ : qs.length * 2 ^ (9 * k) ≤ N ^ 2) :
+    ((timeBound (189 * k) (9 * k) k qs + 1 : ℕ) : ℝ) ≤
+      2621440 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+        (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+  have hc : ((timeBound (189 * k) (9 * k) k qs + 1 : ℕ) : ℝ) ≤
+      32768 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 *
+        (workShape (189 * k) (9 * k) k N qs.length : ℝ) := by
+    exact_mod_cast timeBound_le (L := 189 * k) (m := 9 * k) (by omega) k qs
+  have hs : (workShape (189 * k) (9 * k) k N qs.length : ℝ) ≤
+      80 * ((9 * k + 1 : ℕ) : ℝ) * (9 / 20 : ℝ) ^ k * (N : ℝ) ^ 2 := by
+    simpa only [workShape, Nat.cast_add, Nat.cast_one] using
+      BoxTradeoff.nativeShape_ninth_blocks k N qs.length hN hQ
+  have h := hc.trans (mul_le_mul_of_nonneg_left hs (by positivity))
+  convert h using 1; ring
+
+/-- The same actual native ledger has finite thin-dimension exponent `8/125 = 0.064`,
+with polynomial depth factors explicit. This is not an end-to-end 3SUM time bound. -/
+theorem thin_timeBound_rpow (k N : ℕ) (qs : List (Fin N × Fin N))
+    (hN : D (9 * k) ^ 18 ≤ N) (hQ : qs.length * 2 ^ (9 * k) ≤ N ^ 2) :
+    ((timeBound (189 * k) (9 * k) k qs + 1 : ℕ) : ℝ) ≤
+      2621440 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+        (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (N : ℝ) ^ 2 := by
+  have hd := mul_le_mul_of_nonneg_left (BoxTradeoff.decay_le_rpow k)
+    (show (0 : ℝ) ≤ 2621440 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 *
+      ((9 * k + 1 : ℕ) : ℝ) by positivity)
+  exact (thin_timeBound k N qs hN hQ).trans (mul_le_mul_of_nonneg_right hd (by positivity))
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Restore.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Restore.lean
new file mode 100644
index 0000000000..10fd4496ea
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Restore.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Front
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Transfer
+
+/-!
+# Actual restoration of the original matrix, coordinate and threshold words
+
+The unchanged native copy restores every original matrix/coordinate word and the native
+length header from its protected snapshot. Two final instructions restore the additional
+threshold word, which was retained in a high register before producer reuse.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM
+
+/-- Actual restoration copy and threshold store, with their complete memory readback. -/
+theorem exec_restoreInput {W L m t N Q : ℕ} (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N Q x) (ht : x.regs Reg.threshold = t)
+    (hfit : Fits W (wordBudget L m t N Q)) :
+    ∃ y, ExecWithin W restoreInput x y (7 * QueriedProduct.inputEnd m N Q + 12) ∧
+      QueriedProduct.Parameters L m N Q y ∧
+      y.mem = Function.update
+        (ArrayCopy.copyPrefix x.mem (QueriedProduct.snapshotBase L m N Q) 0
+          (QueriedProduct.inputEnd m N Q)) (QueriedProduct.inputEnd m N Q) t := by
+  obtain ⟨u, hu, up, um⟩ := QueriedProduct.exec_restoreInput x hp (old_fits hfit)
+  have ut : u.regs Reg.threshold = t := (hu.regs_eq (by decide)).trans ht
+  let y := (u.set QueriedProduct.Reg.address (QueriedProduct.inputEnd m N Q)).write
+    (QueriedProduct.inputEnd m N Q) t
+  have hy : ExecWithin W restoreThreshold u y 2 := by
+    ram_eval [restoreThreshold, y, up.inputSize, ut, QueriedProduct.Reg.address,
+      QueriedProduct.Reg.inputSize, Reg.threshold, Fin.mk.injEq]
+  refine ⟨y, (hu.seq hy).mono (by omega), up.of_frame ?_, ?_⟩
+  · intro i hi
+    have hnot : QueriedProduct.Reg.address ∉ QueriedProduct.parameterRegisters := by decide
+    have hne : i ≠ QueriedProduct.Reg.address := by
+      intro heq
+      exact hnot (heq ▸ hi)
+    simp only [y, Data.write_regs, Data.set_regs, Function.update_of_ne hne]
+  · change Function.update u.mem _ t = _
+    rw [um]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/State.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/State.lean
new file mode 100644
index 0000000000..3dd462af84
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/State.lean
@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Program
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Admission
+
+/-!
+# Persistent routed box-product geometry
+
+The high scalar protocol contains only original parameters and actual computed addresses.
+The geometry predicate records the four readonly families of directory/descriptor words.
+It is independent of the changing per-tile values, query stack and temporary results.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Actual high-register contents retained between all tile calls. -/
+structure Parameters (L m t N Q : ℕ) (x : Data 160) : Prop where
+  /-- Original threshold. -/
+  threshold : x.regs Reg.threshold = t
+  /-- Shared directory. -/
+  directory : x.regs Reg.directory = directoryBase L m N Q
+  /-- Computed compact descriptors. -/
+  records : x.regs Reg.records = recordBase L m t N Q
+  /-- Reusable compact signed values. -/
+  values : x.regs Reg.values = valueBase L m t N Q
+  /-- Actual compact count. -/
+  count : x.regs Reg.count = (boxes L m t).card
+  /-- Reusable actual temporary results. -/
+  results : x.regs Reg.results = resultBase L m t N Q
+
+/-- Pure directory/descriptor readback, with no execution, frame or cost certificate. -/
+structure Geometry (L m t N Q : ℕ) (μ : ℕ → ℕ) : Prop where
+  /-- Actual directory ranks, including invalid zero words. -/
+  directory : ∀ s < (m - t + 1) * 10 ^ L,
+    μ (directoryBase L m N Q + s) = BoxTable.directoryWord L (m - t) s
+  /-- Actual completed leaf codes. -/
+  code : ∀ s < (m - t + 1) * 10 ^ L, BoxTable.Eligible L (m - t) s →
+    μ (recordBase L m t N Q + 3 * Nat.count (BoxTable.Eligible L (m - t)) s) =
+      BoxTable.recordCode L s
+  /-- Actual star counts. -/
+  stars : ∀ s < (m - t + 1) * 10 ^ L, BoxTable.Eligible L (m - t) s →
+    μ (recordBase L m t N Q + 3 * Nat.count (BoxTable.Eligible L (m - t)) s + 1) =
+      BoxTable.recordStars L s
+  /-- Actual highest-star place values. -/
+  stride : ∀ s < (m - t + 1) * 10 ^ L, BoxTable.Eligible L (m - t) s →
+    μ (recordBase L m t N Q + 3 * Nat.count (BoxTable.Eligible L (m - t)) s + 2) =
+      BoxTable.recordStride L s
+
+/-- The current geometry supplies the constructor's readonly catalogue without tying its
+outside frame to a previous tile's values. -/
+theorem Geometry.catalogue {L m t N Q : ℕ} {μ : ℕ → ℕ} (h : Geometry L m t N Q μ) :
+    BoxTable.CataloguePrefix L (m - t) (directoryBase L m N Q) (recordBase L m t N Q)
+      ((m - t + 1) * 10 ^ L) μ μ :=
+  ⟨h.directory, h.code, h.stars, h.stride, fun _ _ _ => rfl⟩
+
+/-- Writes outside the directory and compact descriptors preserve the actual shared geometry. -/
+theorem Geometry.reframe {L m t N Q : ℕ} {μ ν : ℕ → ℕ} (h : Geometry L m t N Q μ)
+    (hf : ∀ p, directoryBase L m N Q ≤ p → p < valueBase L m t N Q → ν p = μ p) :
+    Geometry L m t N Q ν := by
+  have hK (s : ℕ) (hs : s < (m - t + 1) * 10 ^ L)
+      (hv : BoxTable.Eligible L (m - t) s) :
+      Nat.count (BoxTable.Eligible L (m - t)) s < (boxes L m t).card := by
+    have h := Nat.count_strict_mono hv hs
+    rwa [BoxTable.count_eligible_eq_card_boxes] at h
+  constructor
+  · intro s hs
+    rw [hf _ (by omega) (by unfold valueBase recordBase; omega)]
+    exact h.directory s hs
+  · intro s hs hv
+    have hk := hK s hs hv
+    rw [hf _ (by unfold recordBase; omega) (by unfold valueBase; omega)]
+    exact h.code s hs hv
+  · intro s hs hv
+    have hk := hK s hs hv
+    rw [hf _ (by unfold recordBase; omega) (by unfold valueBase; omega)]
+    exact h.stars s hs hv
+  · intro s hs hv
+    have hk := hK s hs hv
+    rw [hf _ (by unfold recordBase; omega) (by unfold valueBase; omega)]
+    exact h.stride s hs hv
+
+/-- Extending a low-bank execution leaves every higher caller register untouched. -/
+theorem boxBank_extend_high (z : Data 64) (x : Data 160) (i : Fin 160) (hi : 64 ≤ i.val) :
+    (z.extend boxBank x).regs i = x.regs i := by
+  have hnot : ¬∃ j, boxBank j = i := by
+    rintro ⟨j, hj⟩
+    have hv := congrArg (fun r : Fin 160 => r.val) hj
+    change j.val = i.val at hv
+    omega
+  exact Function.extend_apply' _ _ _ hnot
+
+/-- The scalar protocol survives any low-bank native execution. -/
+theorem Parameters.extend {L m t N Q : ℕ} {x : Data 160}
+    (h : Parameters L m t N Q x) (z : Data 64) :
+    Parameters L m t N Q (z.extend boxBank x) :=
+  ⟨(boxBank_extend_high z x _ (by decide)).trans h.threshold,
+    (boxBank_extend_high z x _ (by decide)).trans h.directory,
+    (boxBank_extend_high z x _ (by decide)).trans h.records,
+    (boxBank_extend_high z x _ (by decide)).trans h.values,
+    (boxBank_extend_high z x _ (by decide)).trans h.count,
+    (boxBank_extend_high z x _ (by decide)).trans h.results⟩
+
+/-- The full allocation and one-past-end cursor values fit the original envelope. -/
+theorem allocated_fits {w L m t N Q n : ℕ} (hfit : Fits w (wordBudget L m t N Q))
+    (hn : n ≤ memoryEnd L m t N Q) : Fits w n :=
+  hfit.of_le (by unfold wordBudget; omega)
+
+/-- Every old producer/group buffer precedes the shared box geometry, followed in order
+by compact records, retained values, query stack and temporary answers. -/
+theorem allocation_order (L m t N Q : ℕ) :
+    BandPreparation.memoryEnd L m N ≤ directoryBase L m N Q ∧
+    QueriedProduct.groupedBase L m N Q + Q ≤ directoryBase L m N Q ∧
+    QueriedProduct.codeBase L m N Q + Q ≤ directoryBase L m N Q ∧
+    directoryBase L m N Q ≤ recordBase L m t N Q ∧
+    recordBase L m t N Q ≤ valueBase L m t N Q ∧
+    valueBase L m t N Q + (boxes L m t).card ≤ resultBase L m t N Q := by
+  have hs := (QueriedProduct.producers_le_snapshot L m N Q).1
+  have hT := Nat.zero_le (10 ^ L)
+  simp only [directoryBase, recordBase, valueBase, resultBase, stackBase,
+    QueriedProduct.memoryEnd, QueriedProduct.stampBase, QueriedProduct.scratchBase,
+    QueriedProduct.outputBase, QueriedProduct.groupedBase, QueriedProduct.originalBase,
+    QueriedProduct.codeBase, QueriedProduct.offsetBase]
+  omega
+
+/-- Original admission covers one retained-value constructor on any actual producer pointers. -/
+theorem tile_fits {W L m t N Q AA BB : ℕ} (hfit : Fits W (wordBudget L m t N Q))
+    (hA : AA ≤ directoryBase L m N Q) (hB : BB ≤ directoryBase L m N Q) :
+    Fits W (directoryBase L m N Q + recordBase L m t N Q + valueBase L m t N Q + AA + BB +
+      20 * ((m - t + 1) * 10 ^ L) + 20 * 10 ^ L + 30) := by
+  have hT : 10 ^ L ≤ (L + 1) * 10 ^ L := Nat.le_mul_of_pos_left _ (by omega)
+  apply hfit.of_le
+  unfold wordBudget
+  omega
+
+/-- Original admission covers the sparse batch and every one-past-end cursor. -/
+theorem batch_fits {W L m t N Q AA BB C n : ℕ} (hfit : Fits W (wordBudget L m t N Q))
+    (hA : AA ≤ directoryBase L m N Q) (hB : BB ≤ directoryBase L m N Q)
+    (hC : C ≤ directoryBase L m N Q) (hn : n ≤ Q) :
+    Fits W (BoxBatch.addressBound L t AA BB (directoryBase L m N Q)
+      (valueBase L m t N Q) (boxes L m t).card C (resultBase L m t N Q) n) := by
+  have hK : (boxes L m t).card ≤ valueBase L m t N Q := by unfold valueBase; omega
+  have hO : resultBase L m t N Q ≤ memoryEnd L m t N Q := by unfold memoryEnd; omega
+  apply hfit.of_le
+  unfold wordBudget BoxBatch.addressBound BoxQuery.queryAddressBound
+  omega
+
+/-- The shared encodings precede every protected group and answer word. -/
+theorem band_before_grouped (L m N Q : ℕ) :
+    BandPreparation.memoryEnd L m N ≤ QueriedProduct.groupedBase L m N Q := by
+  have h := (QueriedProduct.producers_le_snapshot L m N Q).1
+  simp only [QueriedProduct.groupedBase, QueriedProduct.originalBase, QueriedProduct.codeBase,
+    QueriedProduct.offsetBase]
+  omega
+
+/-- Every increment of the actual bounded tile index fits the original input envelope. -/
+theorem index_fits {W L m t N Q j : ℕ} (hfit : Fits W (wordBudget L m t N Q))
+    (hj : j < numBands L m N ^ 2) : Fits W (j + 1) := by
+  have ho := allocation_order L m t N Q
+  have hc : numBands L m N ^ 2 ≤ QueriedProduct.codeBase L m N Q := by
+    unfold QueriedProduct.codeBase
+    omega
+  have hcd : QueriedProduct.codeBase L m N Q ≤ directoryBase L m N Q :=
+    (Nat.le_add_right _ Q).trans ho.2.2.1
+  have hde : directoryBase L m N Q ≤ memoryEnd L m t N Q := by
+    have h := ho.2.2.2
+    unfold memoryEnd
+    omega
+  exact allocated_fits hfit ((Nat.succ_le_of_lt hj).trans (hc.trans (hcd.trans hde)))
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Thin.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Thin.lean
new file mode 100644
index 0000000000..fc56d3f30b
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Thin.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Width
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Resources
+
+/-!
+# Actual native thin-product execution with the improved finite saving
+
+The same initialized prefix, charged halt and exact original-order matrix products
+satisfy the finite `D^(-8/125)` instruction bound. Original dimensions, occurrence
+sparsity, entry magnitudes and sufficient width are explicit; no backend is supplied.
+Polynomial depth factors remain visible, so this is not the final 3SUM exponent.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- One actual initialized native product with finite `0.064` thin-dimension saving,
+including the charged halt, raw conversion when selected, and complete input restoration. -/
+theorem runs_thin {W k N A : ℕ} (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D (9 * k))) ℤ)
+    (Y : Matrix (Fin (D (9 * k))) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hX : ∀ i j, |X i j| ≤ (A : ℤ))
+    (hY : ∀ i j, |Y i j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i j, 0 ≤ X i j) ∧ (∀ i j, 0 ≤ Y i j))
+    (hN : D (9 * k) ^ 18 ≤ N) (hQ : qs.length * 2 ^ (9 * k) ≤ N ^ 2)
+    (hW : admissionWidth (189 * k) (9 * k) k N qs.length A ≤ W) :
+    InputFits W (input bits (189 * k) k X Y qs) ∧
+    ∃ y n, ((n + 1 : ℕ) : ℝ) ≤
+        2621440 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+          (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (N : ℝ) ^ 2 ∧
+      Runs W ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits (189 * k) k X Y qs)) ⟨(program bits).size, y⟩ n ∧
+      Executes W ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits (189 * k) k X Y qs))
+        (QueriedProduct.outputBase (189 * k) (9 * k) N qs.length) (n + 1) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length,
+        y.mem (QueriedProduct.outputBase (189 * k) (9 * k) N qs.length + i.val) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ p, ¬(QueriedProduct.inputEnd (9 * k) N qs.length + 1 ≤ p ∧
+        p < memoryEnd (189 * k) (9 * k) k N qs.length) →
+        y.mem p = (State.init (input bits (189 * k) k X Y qs) : State 160).data.mem p) := by
+  obtain ⟨hi, y, n, hn, hp, he, hy, hv, hf⟩ :=
+    runs_wide (L := 189 * k) (m := 9 * k) (t := k)
+      (by omega) (by omega) bits X Y qs hX hY hbits hW
+  have hn' : ((n + 1 : ℕ) : ℝ) ≤ (timeBound (189 * k) (9 * k) k qs + 1 : ℕ) := by
+    exact_mod_cast hn
+  exact ⟨hi, y, n, hn'.trans (thin_timeBound_rpow k N qs hN hQ), hp, he, hy, hv, hf⟩
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tile.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tile.lean
new file mode 100644
index 0000000000..45cf2fd93e
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tile.lean
@@ -0,0 +1,343 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Arguments
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Charges
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Magnitude
+
+/-!
+# One actual routed tile against shared box geometry
+
+The real saved offsets determine the query span. Its typed codes, inner-coordinate count,
+source encodings and original matrix coordinates are recovered from the existing native
+producer contracts. One retained table, sparse batch and actual answer copy are charged.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+set_option maxRecDepth 4096 in
+-- The fixed caller frame check unfolds the existing 32-member 160-register protocol.
+/-- One actual tile builds retained values, answers its real grouped span and delivers all
+signed matrix-product answers, retaining the one shared geometry and producer arrays. -/
+theorem exec_tileStep {w L m t N A j : ℕ} (hw : 0 < w) (hm : m ≤ L) (ht : t ≤ m)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N qs.length x) (hb : Parameters L m t N qs.length x)
+    (hx : x.regs QueriedProduct.Reg.index = j) (hj : j < numBands L m N ^ 2)
+    (hg : QueriedProduct.SavedGroups L m N qs.length old x.mem)
+    (he : QueriedProduct.EncodedBands hm X Y x.mem) (hgeom : Geometry L m t N qs.length x.mem)
+    (hvalues : ∀ i : Fin qs.length,
+      old (Wanted.codeAddress L m N qs.length +
+          CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+        (PrunedQuery.queryIndex
+          (outStrOfPos (MaskTable.layout hm) (qs.get i).1 (qs.get i).2)).val)
+    (hoffsets : ∀ s ≤ numBands L m N ^ 2,
+      old (Wanted.offsetAddress L m N qs.length + s) =
+        Nat.count (fun k => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < s) qs.length)
+    (hX : ∀ i k, |X i k| ≤ (A : ℤ)) (hY : ∀ k i, |Y k i| ≤ (A : ℤ))
+    (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    let a := x.mem (QueriedProduct.offsetBase L m N qs.length + j)
+    let b := x.mem (QueriedProduct.offsetBase L m N qs.length + j + 1)
+    ∃ y, ExecWithin (w + 2) tileStep x y
+        (328 * (boxes L m t).card + (b - a) * (batchUnit L m t + 7) + 63) ∧
+      QueriedProduct.Parameters L m N qs.length y ∧ Parameters L m t N qs.length y ∧
+      y.regs QueriedProduct.Reg.index = j + 1 ∧
+      QueriedProduct.SavedGroups L m N qs.length old y.mem ∧
+      QueriedProduct.EncodedBands hm X Y y.mem ∧ Geometry L m t N qs.length y.mem ∧
+      (∀ i : Fin qs.length, (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) i.val = j →
+        y.mem (QueriedProduct.groupedBase L m N qs.length +
+          CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+            Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ p, ¬(QueriedProduct.groupedBase L m N qs.length + a ≤ p ∧
+          p < QueriedProduct.groupedBase L m N qs.length + b) →
+        ¬(directoryBase L m N qs.length ≤ p ∧ p < memoryEnd L m t N qs.length) →
+          y.mem p = x.mem p) := by
+  dsimp only
+  let B := numBands L m N
+  let a := x.mem (QueriedProduct.offsetBase L m N qs.length + j)
+  let b := x.mem (QueriedProduct.offsetBase L m N qs.length + j + 1)
+  let β := j / B
+  let γ := j % B
+  let pa := BandPreparation.catalogueBase L m N + β * 10 ^ L
+  let pb := BandPreparation.catalogueBase L m N + (B + γ) * 10 ^ L
+  let encA := encodingL (bandArrayL (MaskTable.layout hm) X β)
+  let encB := encodingR (bandArrayR (MaskTable.layout hm) Y γ)
+  let D0 := directoryBase L m N qs.length
+  let R0 := recordBase L m t N qs.length
+  let V := valueBase L m t N qs.length
+  let K := (boxes L m t).card
+  let O := resultBase L m t N qs.length
+  have habQ := hg.span_bounds (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) hoffsets hj
+  have hB : 0 < B := by dsimp only [B] at *; nlinarith only [hj, Nat.zero_le j]
+  have hβ : β < B := (Nat.div_lt_iff_lt_mul hB).mpr (by simpa [B, pow_two] using hj)
+  have hγ : γ < B := Nat.mod_lt j hB
+  have hT : (β, γ) ∈ tiles L m N :=
+    Finset.mem_product.mpr ⟨Finset.mem_range.mpr hβ, Finset.mem_range.mpr hγ⟩
+  have hnum : β * numBands L m N + γ = j := by
+    simpa only [β, γ, B, Nat.mul_comm] using Nat.div_add_mod j B
+  have hcode (k : ℕ) (hk : k < qs.length) :
+      x.mem (QueriedProduct.codeBase L m N qs.length + k) < 10 ^ L := by
+    rw [hg.codes k hk]
+    exact QueriedProduct.router_code_lt hm qs old hvalues k hk
+  let queries : Fin (b - a) → OutStr L := fun i => PrunedQuery.queryAt
+    ⟨x.mem (QueriedProduct.codeBase L m N qs.length + (a + i.val)),
+      hcode _ (by have := i.isLt; omega)⟩
+  let wanted := List.ofFn queries
+  have hinput (i : Fin (b - a)) :
+      x.mem (QueriedProduct.codeBase L m N qs.length + (a + i.val)) =
+        (PrunedQuery.queryIndex (queries i)).val := by
+    simp only [queries, PrunedQuery.queryIndex_queryAt]
+  have hset : Finset.univ.image queries =
+      wantedStrings (MaskTable.layout hm) qs.toFinset β γ :=
+    hg.span_queries hm qs hvalues hoffsets (β, γ) hT a b (by rw [hnum])
+      (by rw [hnum]; rfl) queries hinput
+  have hinner : ∀ η ∈ wanted, (innerSetO η).card = m := by
+    intro η hη
+    obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hη
+    apply card_innerSetO_of_mem_wantedStrings (MaskTable.layout hm) qs.toFinset β γ
+    rw [← hset]
+    exact Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩
+  obtain ⟨arg, har, arp, arb, arm, ari, arc, arinner, arth, arV, arK,
+      arA, arB, arq, ars, aro, ard, arlen⟩ :=
+    exec_tileArguments x hp hb hx hj rfl rfl habQ.1 habQ.2 hfit
+  change (arg.comap boxBank).regs BoxTable.Reg.arrayA = pa at arA
+  change (arg.comap boxBank).regs BoxTable.Reg.arrayB = pb at arB
+  change (arg.comap boxBank).regs BoxTable.Reg.values = V at arV
+  change (arg.comap boxBank).regs BoxTable.Reg.count = K at arK
+  have hpab : pa + 10 ^ L ≤ BandPreparation.memoryEnd L m N ∧
+      pb + 10 ^ L ≤ BandPreparation.memoryEnd L m N := by
+    have hl := BandPreparation.catalogue_block_le false hβ
+    have hr := BandPreparation.catalogue_block_le true hγ
+    simpa only [BandPreparation.catalogueAddress, Bool.false_eq_true, ↓reduceIte,
+      Nat.zero_add, Nat.add_zero, pa, pb, B] using And.intro hl hr
+  have horder := allocation_order L m t N qs.length
+  have hbefore : BandPreparation.memoryEnd L m N ≤ D0 := horder.1
+  have hgroup : QueriedProduct.groupedBase L m N qs.length + qs.length ≤ D0 := horder.2.1
+  have hqueries : QueriedProduct.codeBase L m N qs.length + qs.length ≤ D0 := horder.2.2.1
+  have hVorder : D0 ≤ R0 ∧ R0 ≤ V ∧ V + K ≤ O := horder.2.2.2
+  have hpaD : pa ≤ D0 := (Nat.le_add_right pa (10 ^ L)).trans (hpab.1.trans hbefore)
+  have hpbD : pb ≤ D0 := (Nat.le_add_right pb (10 ^ L)).trans (hpab.2.trans hbefore)
+  have hpaV : pa + 10 ^ L ≤ V :=
+    hpab.1.trans (hbefore.trans (hVorder.1.trans hVorder.2.1))
+  have hpbV : pb + 10 ^ L ≤ V :=
+    hpab.2.trans (hbefore.trans (hVorder.1.trans hVorder.2.1))
+  have hqD : QueriedProduct.codeBase L m N qs.length + a ≤ D0 :=
+    (Nat.add_le_add_left (habQ.1.trans habQ.2) _).trans hqueries
+  have hleft (c : Fin (10 ^ L)) :
+      arg.mem (pa + c.val) = Signed.encode (encA (BoxTable.leafAt c)) := by
+    rw [arm]
+    simpa only [pa, encA, BandPreparation.catalogueAddress, Bool.false_eq_true, ↓reduceIte,
+      Nat.zero_add, Nat.add_assoc, BoxTable.leafIndex_leafAt] using
+        he.left β hβ (BoxTable.leafAt c)
+  have hright (c : Fin (10 ^ L)) :
+      arg.mem (pb + c.val) = Signed.encode (encB (BoxTable.leafAt c)) := by
+    rw [arm]
+    simpa only [pb, encB, B, BandPreparation.catalogueAddress, ↓reduceIte,
+      Nat.add_assoc, BoxTable.leafIndex_leafAt] using he.right γ hγ (BoxTable.leafAt c)
+  have haB (τ : Leaf L) : (encA τ).natAbs ≤ encodedBound L A := by
+    have h := abs_encodingL_le (abs_bandArrayL_le (MaskTable.layout hm) (by positivity) hX β) τ
+    rw [← Int.natCast_natAbs] at h
+    exact_mod_cast h
+  have hbB (τ : Leaf L) : (encB τ).natAbs ≤ encodedBound L A := by
+    have h := abs_encodingR_le (abs_bandArrayR_le (MaskTable.layout hm) (by positivity) hY γ) τ
+    rw [← Int.natCast_natAbs] at h
+    exact_mod_cast h
+  have htablemag : GenericRAM.Signed.Fits w
+      (encodedBound L A + encodedBound L A + 10 ^ L * (encodedBound L A * encodedBound L A) : ℕ) :=
+    (box_magnitude hw hmag).of_natAbs_le (by
+      simpa only [Int.natAbs_natCast] using BoxQuery.table_magnitudeBound_le L
+        (encodedBound L A) (encodedBound L A))
+  have hspan : 10 ^ L ≤ (L + 1) * 10 ^ L := Nat.le_mul_of_pos_left _ (by omega)
+  obtain ⟨z, hz, zv, zf, zregs⟩ := BoxTable.exec_tile (arg.comap boxBank) encA encB haB hbB arc
+    arV arA arB (by rw [arK, BoxTable.count_eligible_eq_card_boxes])
+    (by simpa only [Data.comap_mem, arm] using hgeom.catalogue)
+    (by rfl) (by rw [BoxTable.count_eligible_eq_card_boxes]; rfl)
+    hpaV hpbV hleft hright (tile_fits hfit hpaD hpbD) htablemag
+  rw [BoxTable.count_eligible_eq_card_boxes] at hz zf
+  let u := z.extend boxBank arg
+  have hu := hz.rename boxBank_injective
+  have ur (i : Fin 160) (hi : 64 ≤ i.val) : u.regs i = arg.regs i := boxBank_extend_high z arg i hi
+  have up : QueriedProduct.Parameters L m N qs.length u := arp.reframe (fun i hi => ur i (by omega))
+  have ub : Parameters L m t N qs.length u := arb.extend z
+  have ulow (i : Fin 64) (hi : ¬BoxTable.TileLocal i) :
+      (u.comap boxBank).regs i = (arg.comap boxBank).regs i := by
+    simpa only [u, Data.comap_extend boxBank_injective] using zregs i hi
+  have uread : BoxQuery.Readback m t D0 V pa pb encA encB u.mem := by
+    change BoxQuery.Readback m t D0 V pa pb encA encB z.mem
+    constructor
+    · intro c
+      rw [zf _ (by have := c.isLt; omega)]
+      exact hleft c
+    · intro c
+      rw [zf _ (by have := c.isLt; omega)]
+      exact hright c
+    · intro s hs
+      rw [zf _ (by dsimp only [D0, V]; unfold valueBase recordBase; omega), Data.comap_mem, arm]
+      exact hgeom.directory s hs
+    · exact zv
+  have ux : BoxBatch.Arguments L t pa pb D0 V K (u.comap boxBank) :=
+    ⟨(ulow _ (by decide)).trans arc.levels, (ulow _ (by decide)).trans arth,
+      (ulow _ (by decide)).trans arc.span, (ulow _ (by decide)).trans arA,
+      (ulow _ (by decide)).trans arB, (ulow _ (by decide)).trans arc.directory,
+      (ulow _ (by decide)).trans arV, (ulow _ (by decide)).trans arK⟩
+  have uwanted (i : Fin wanted.length) : u.mem
+      (QueriedProduct.codeBase L m N qs.length + a + i.val) =
+        (PrunedQuery.queryIndex (wanted.get i)).val := by
+    change z.mem _ = _
+    rw [zf _ (by have := i.isLt; simp only [wanted, List.length_ofFn] at this; omega),
+      Data.comap_mem, arm]
+    simpa only [wanted, List.get_eq_getElem, List.getElem_ofFn, Nat.add_assoc] using
+      hinput ⟨i.val, by simpa only [wanted, List.length_ofFn] using i.isLt⟩
+  obtain ⟨q, hq, _, _, _, _, qv, _, qf⟩ := BoxBatch.exec_queryProgram wanted (u.comap boxBank)
+    ux ((ulow _ (by decide)).trans arq)
+    (by
+      calc
+        (u.comap boxBank).regs BoxBatch.Reg.stop = QueriedProduct.codeBase L m N qs.length + b := by
+          simpa only [b, Nat.add_assoc] using (ulow _ (by decide)).trans ars
+        _ = (QueriedProduct.codeBase L m N qs.length + a) + wanted.length := by
+          simp only [wanted, List.length_ofFn]
+          omega) ((ulow _ (by decide)).trans aro)
+    encA encB haB hbB hinner uwanted rfl (by omega) (by omega)
+    (by dsimp only [D0, V]; unfold valueBase recordBase; omega)
+    (by simp only [wanted, List.length_ofFn]; omega) (by rfl) uread
+    (batch_fits hfit hpaD hpbD hqD (by
+      simp only [wanted, List.length_ofFn]; omega)) (box_magnitude hw hmag)
+  have hqtime : BoxBatch.queryTime m t wanted = (b - a) * batchUnit L m t + 2 := by
+    simpa only [wanted, List.length_ofFn, batchUnit] using
+      BoxBatch.queryTime_eq_alpha wanted hinner
+  rw [hqtime] at hq
+  let v := q.extend boxBank u
+  have hv := hq.rename boxBank_injective
+  have vr (i : Fin 160) (hi : 64 ≤ i.val) : v.regs i = u.regs i := boxBank_extend_high q u i hi
+  have vp : QueriedProduct.Parameters L m N qs.length v := up.reframe (fun i hi => vr i (by omega))
+  have vb : Parameters L m t N qs.length v := ub.extend q
+  have vd : v.regs QueriedProduct.Reg.destination =
+      QueriedProduct.groupedBase L m N qs.length + a :=
+    (vr _ (by decide)).trans ((ur _ (by decide)).trans ard)
+  have vl : v.regs QueriedProduct.Reg.length = b - a :=
+    (vr _ (by decide)).trans ((ur _ (by decide)).trans arlen)
+  let c := v.set QueriedProduct.Reg.source O
+  have hc : ExecWithin (B := .standard) (w + 2)
+      (ram[QueriedProduct.Reg.source ← Reg.results]) v c 1 := by
+    ram_eval [c, vb.results, O]
+  have cp : QueriedProduct.Parameters L m N qs.length c :=
+    vp.set_work _ (by decide) _
+  have cs : c.regs QueriedProduct.Reg.source = O := by simp [c]
+  have cd : c.regs QueriedProduct.Reg.destination =
+      QueriedProduct.groupedBase L m N qs.length + a :=
+    (hc.regs_eq (by decide)).trans vd
+  have cl : c.regs QueriedProduct.Reg.length = b - a := (hc.regs_eq (by decide)).trans vl
+  obtain ⟨d, hd, dm, dr⟩ := QueriedProduct.exec_copyCall c
+    (hfit.of_le (by unfold wordBudget; omega))
+    (by rw [cs, cl]; apply allocated_fits hfit; dsimp only [O]; unfold memoryEnd; omega)
+    (by rw [cd, cl]; apply allocated_fits hfit; unfold memoryEnd; dsimp only [O] at *; omega)
+    (by rw [cs, cd, cl]; exact Or.inr (Or.inl (by omega)))
+  have dp : QueriedProduct.Parameters L m N qs.length d := cp.reframe (fun i hi => dr i (by omega))
+  have di : d.regs QueriedProduct.Reg.index = j :=
+    (dr _ (by decide)).trans ((hc.regs_eq (by decide)).trans
+      ((vr _ (by decide)).trans ((ur _ (by decide)).trans ari)))
+  have fnext : Fits (w + 2) (j + 1) := index_fits hfit hj
+  let y := d.set QueriedProduct.Reg.index (j + 1)
+  have hy : ExecWithin (B := .standard) (w + 2)
+      (ram[QueriedProduct.Reg.index ← QueriedProduct.Reg.index + QueriedProduct.Reg.one])
+      d y 1 := by
+    ram_eval [y, di, dp.one, fnext]
+  have yp : QueriedProduct.Parameters L m N qs.length y := dp.set_work _ (by decide) _
+  have native : ExecWithin (w + 2) tileStep x y
+      (328 * K + (b - a) * (batchUnit L m t + 7) + 63) := by
+    apply (har.seq (hu.seq (hv.seq ((hc.seq hd).seq hy)))).mono
+    rw [cl]
+    simp only [Nat.mul_add]
+    omega
+  have vframe (p : ℕ) (hf : ¬(V ≤ p ∧ p < memoryEnd L m t N qs.length)) :
+      v.mem p = x.mem p := by
+    change q.mem p = x.mem p
+    have hO : V + K + 5 * BoxQuery.stackCapacity L = O := rfl
+    have hEnd : memoryEnd L m t N qs.length = O + qs.length := rfl
+    rw [qf p (by
+      simp only [wanted, List.length_ofFn]
+      change ¬((V + K ≤ p ∧ p < V + K + 5 * BoxQuery.stackCapacity L) ∨
+        (O ≤ p ∧ p < O + (b - a)))
+      rw [hO]
+      rw [hEnd] at hf
+      omega)]
+    change z.mem p = x.mem p
+    rw [zf p (by rw [hEnd] at hf; omega), Data.comap_mem, arm]
+  have ym : y.mem = ArrayCopy.copyPrefix v.mem O
+      (QueriedProduct.groupedBase L m N qs.length + a) (b - a) := by
+    simpa only [y, Data.set_mem, cs, cd, cl, c] using dm
+  have strongframe (p : ℕ)
+      (ho : ¬(QueriedProduct.groupedBase L m N qs.length + a ≤ p ∧
+        p < QueriedProduct.groupedBase L m N qs.length + b))
+      (hf : ¬(V ≤ p ∧ p < memoryEnd L m t N qs.length)) : y.mem p = x.mem p := by
+    rw [ym, ArrayCopy.copyPrefix_outside (by omega), vframe p hf]
+  have frame (p : ℕ)
+      (ho : ¬(QueriedProduct.groupedBase L m N qs.length + a ≤ p ∧
+        p < QueriedProduct.groupedBase L m N qs.length + b))
+      (hf : ¬(D0 ≤ p ∧ p < memoryEnd L m t N qs.length)) : y.mem p = x.mem p :=
+    strongframe p ho (by omega)
+  refine ⟨y, native, yp, ?_, by simp [y], ?_, ?_, ?_, ?_, frame⟩
+  · exact ⟨(native.regs_eq (by decide)).trans hb.threshold,
+      (native.regs_eq (by decide)).trans hb.directory,
+      (native.regs_eq (by decide)).trans hb.records,
+      (native.regs_eq (by decide)).trans hb.values,
+      (native.regs_eq (by decide)).trans hb.count,
+      (native.regs_eq (by decide)).trans hb.results⟩
+  · exact hg.reframe (fun p hp hbefore => frame p (by omega) (by omega))
+  · exact he.reframe (fun p hp => frame p
+      (by have h := band_before_grouped L m N qs.length; omega) (by omega))
+  · exact hgeom.reframe (fun p hD hV => strongframe p (by omega) (by omega))
+  · intro i hkey
+    let p := CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i
+    have hp : p < qs.length := CountingSort.position_lt _ i.isLt
+    have hspan : a ≤ p ∧ p < b := by
+      have hs := (CountingSort.position_mem_iff
+        (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) i.isLt j).mpr hkey
+      have ha := (hg.offsets j hj.le).trans (hoffsets j hj.le)
+      have hb := (hg.offsets (j + 1) (by omega)).trans (hoffsets (j + 1) (by omega))
+      change a = _ at ha
+      change b = _ at hb
+      simpa only [← ha, ← hb] using hs
+    let k : Fin (b - a) := ⟨p - a, by omega⟩
+    have hak : a + k.val = p := by dsimp only [k]; omega
+    have hquery : queries k = outStrOfPos (MaskTable.layout hm) (qs.get i).1 (qs.get i).2 := by
+      have hr := hinput k
+      rw [hak, hg.codes p hp, hvalues i] at hr
+      simpa only [PrunedQuery.queryAt_queryIndex] using
+        congrArg PrunedQuery.queryAt (Fin.ext hr.symm)
+    have htile : Wanted.tileKey L m N ((qs.get i).1.val, (qs.get i).2.val) =
+        β * numBands L m N + γ := by
+      simpa only [Function.comp_apply, Wanted.inputPairs_get, hnum] using hkey
+    have hbands := (Wanted.tileKey_eq_iff hm (qs.get i).1 (qs.get i).2 (β, γ) hT).mp htile
+    change bandOf L m (qs.get i).1.val = β ∧ bandOf L m (qs.get i).2.val = γ at hbands
+    have hr := qv ⟨k.val, by simp only [wanted, List.length_ofFn]; exact k.isLt⟩
+    simp only [wanted, List.get_eq_getElem, List.getElem_ofFn] at hr
+    rw [hquery, BoxQuery.queryValue_encoding ht _
+      (card_innerSetO_of_mem_wantedStrings (MaskTable.layout hm) qs.toFinset β γ _ (by
+        rw [← hset]; exact Finset.mem_image.mpr ⟨k, Finset.mem_univ _, hquery⟩))] at hr
+    change q.mem (O + k.val) = _ at hr
+    rw [ym]
+    have hcopy := ArrayCopy.copyPrefix_read (mem := v.mem) (src := O)
+      (dst := QueriedProduct.groupedBase L m N qs.length + a) (k := b - a) k.isLt
+    have haddr : QueriedProduct.groupedBase L m N qs.length + a + k.val =
+        QueriedProduct.groupedBase L m N qs.length + p := by omega
+    rw [haddr] at hcopy
+    rw [hcopy]
+    change v.mem (O + k.val) = _ at hr
+    rw [hr]
+    congr 1
+    rw [← hbands.1, ← hbands.2]
+    exact bilinearProduct_bandArray_eq_mul (MaskTable.layout hm) X Y _ _
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tiles.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tiles.lean
new file mode 100644
index 0000000000..e400bc1249
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Tiles.lean
@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Tile
+import Mathlib.Algebra.BigOperators.Intervals
+
+/-!
+# All routed tiles with one shared box geometry
+
+Every actual group span is evaluated against the shared band encodings. The geometry
+is never rebuilt by this loop; values, stack and temporary answers are reused. The
+charged sum counts each original request occurrence only in its own tile.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+open scoped BigOperators
+
+private structure Progress {L m t N : ℕ} (hm : m ≤ L)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (old initial : ℕ → ℕ) (z : Data 160) : Prop where
+  fixed : QueriedProduct.Parameters L m N qs.length z
+  boxes : Parameters L m t N qs.length z
+  index_le : z.regs QueriedProduct.Reg.index ≤ numBands L m N ^ 2
+  groups : QueriedProduct.SavedGroups L m N qs.length old z.mem
+  catalogue : QueriedProduct.EncodedBands hm X Y z.mem
+  geometry : Geometry L m t N qs.length z.mem
+  answers : ∀ i : Fin qs.length,
+    (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) i.val < z.regs QueriedProduct.Reg.index →
+      z.mem (QueriedProduct.groupedBase L m N qs.length +
+          CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+        Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)
+  frame : ∀ p,
+    ¬(QueriedProduct.groupedBase L m N qs.length ≤ p ∧
+      p < QueriedProduct.outputBase L m N qs.length) →
+    ¬(directoryBase L m N qs.length ≤ p ∧ p < memoryEnd L m t N qs.length) →
+      z.mem p = initial p
+
+/-- The fixed native loop evaluates every original wanted occurrence and preserves both
+actual routing and shared encoding/geometry readback, with no tile/time oracle. -/
+theorem exec_evaluateTiles {w L m t N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (ht : t ≤ m)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (x : Data 160)
+    (hp : QueriedProduct.Parameters L m N qs.length x) (hb : Parameters L m t N qs.length x)
+    (hi : x.regs QueriedProduct.Reg.index = 0)
+    (hg : QueriedProduct.SavedGroups L m N qs.length old x.mem)
+    (he : QueriedProduct.EncodedBands hm X Y x.mem) (hgeom : Geometry L m t N qs.length x.mem)
+    (hvalues : ∀ i : Fin qs.length,
+      old (Wanted.codeAddress L m N qs.length +
+          CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+        (PrunedQuery.queryIndex
+          (outStrOfPos (MaskTable.layout hm) (qs.get i).1 (qs.get i).2)).val)
+    (hoffsets : ∀ s ≤ numBands L m N ^ 2,
+      old (Wanted.offsetAddress L m N qs.length + s) =
+        Nat.count (fun k => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < s) qs.length)
+    (hX : ∀ i k, |X i k| ≤ (A : ℤ)) (hY : ∀ k i, |Y k i| ≤ (A : ℤ))
+    (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    ∃ y, ExecWithin (w + 2) evaluateTiles x y
+        ((∑ j ∈ Finset.range (numBands L m N ^ 2), tileCharge L m t qs j) + 2) ∧
+      QueriedProduct.Parameters L m N qs.length y ∧ Parameters L m t N qs.length y ∧
+      QueriedProduct.SavedGroups L m N qs.length old y.mem ∧
+      QueriedProduct.EncodedBands hm X Y y.mem ∧ Geometry L m t N qs.length y.mem ∧
+      (∀ i : Fin qs.length,
+        y.mem (QueriedProduct.groupedBase L m N qs.length +
+          CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length i) =
+            Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ p, ¬(QueriedProduct.groupedBase L m N qs.length ≤ p ∧
+        p < QueriedProduct.outputBase L m N qs.length) →
+        ¬(directoryBase L m N qs.length ≤ p ∧ p < memoryEnd L m t N qs.length) →
+          y.mem p = x.mem p) := by
+  let key := Wanted.tileKey L m N ∘ Wanted.inputPairs qs
+  let T := numBands L m N ^ 2
+  let I := Progress (t := t) hm X Y qs old x.mem
+  let Φ (z : Data 160) :=
+    ∑ j ∈ Finset.Ico (z.regs QueriedProduct.Reg.index) T, tileCharge L m t qs j
+  have hout : QueriedProduct.groupedBase L m N qs.length + qs.length =
+      QueriedProduct.outputBase L m N qs.length := rfl
+  have hgroupBefore := (allocation_order L m t N qs.length).2.1
+  have hstart : I x := ⟨hp, hb, by rw [hi]; omega, hg, he, hgeom,
+    by intro i hk; rw [hi] at hk; omega, by intro p _ _; rfl⟩
+  have hbody (z : Data 160) (hz : I z)
+      (hc : (Cond.lt QueriedProduct.Reg.index QueriedProduct.Reg.tiles).Holds z) :
+      ∃ y C, ExecWithin (w + 2) tileStep z y C ∧ I y ∧ C + 2 + Φ y ≤ Φ z := by
+    have hj : z.regs QueriedProduct.Reg.index < T := by
+      simpa only [Cond.holds_lt, hz.fixed.tiles, T] using hc
+    obtain ⟨y, hr, yp, yb, yi, yg, ye, ygeom, yvalues, yf⟩ :=
+      exec_tileStep hw hm ht X Y qs old z hz.fixed hz.boxes rfl hj
+        hz.groups hz.catalogue hz.geometry hvalues hoffsets hX hY hmag hfit
+    have ha := (hz.groups.offsets _ hj.le).trans (hoffsets _ hj.le)
+    have hb := (hz.groups.offsets _ (Nat.succ_le_of_lt hj)).trans
+      (hoffsets _ (Nat.succ_le_of_lt hj))
+    have hdiff :
+        z.mem (QueriedProduct.offsetBase L m N qs.length + z.regs QueriedProduct.Reg.index + 1) -
+          z.mem (QueriedProduct.offsetBase L m N qs.length + z.regs QueriedProduct.Reg.index) =
+        Nat.count (fun k => key k = z.regs QueriedProduct.Reg.index) qs.length := by
+      rw [show QueriedProduct.offsetBase L m N qs.length + z.regs QueriedProduct.Reg.index + 1 =
+          QueriedProduct.offsetBase L m N qs.length +
+            (z.regs QueriedProduct.Reg.index + 1) by omega,
+        hb, ha, CountingSort.count_lt_succ]
+      dsimp only [key]
+      omega
+    rw [hdiff] at hr
+    refine ⟨y, _, hr, ?_, ?_⟩
+    · refine ⟨yp, yb, by rw [yi]; omega, yg, ye, ygeom, ?_, ?_⟩
+      · intro i hik
+        change key i.val < y.regs QueriedProduct.Reg.index at hik
+        by_cases hki : key i.val = z.regs QueriedProduct.Reg.index
+        · exact yvalues i hki
+        · have hold : key i.val < z.regs QueriedProduct.Reg.index := by rw [yi] at hik; omega
+          have hs := (CountingSort.position_mem key i.isLt).2
+          have hmcount : Nat.count (fun k => key k < key i.val + 1) qs.length ≤
+              Nat.count (fun k => key k < z.regs QueriedProduct.Reg.index) qs.length :=
+            Nat.count_mono_left (fun k _ hk => by omega)
+          have hpos := CountingSort.position_lt key i.isLt
+          dsimp only [key] at hs hmcount hpos
+          rw [yf _ (by omega) (by omega)]
+          exact hz.answers i hold
+      · intro p ho hf
+        have hbQ := (hz.groups.span_bounds key hoffsets hj).2
+        rw [yf p (by omega) hf]
+        exact hz.frame p ho hf
+    · have hsplit := Finset.sum_eq_sum_Ico_succ_bot hj (tileCharge L m t qs)
+      dsimp only [Φ]
+      rw [yi, hsplit]
+      dsimp only [tileCharge, key]
+      omega
+  obtain ⟨y, hr, hy, hc⟩ := ExecWithin.loop_potential I Φ hbody hstart
+  have hlast : y.regs QueriedProduct.Reg.index = T := by
+    have h := hy.index_le
+    simp only [Cond.holds_lt, hy.fixed.tiles] at hc
+    dsimp only [T] at *
+    omega
+  refine ⟨y, ?_, hy.fixed, hy.boxes, hy.groups, hy.catalogue, hy.geometry, ?_, hy.frame⟩
+  · simpa only [Φ, hi, Nat.Ico_zero_eq_range, T, evaluateTiles] using hr
+  · intro i
+    apply hy.answers i
+    rw [hlast]
+    exact Wanted.tileKey_lt hm (Wanted.inputPairs qs i.val)
+      (Wanted.inputPairs_lt qs i i.isLt).1 (Wanted.inputPairs_lt qs i i.isLt).2
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Width.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Width.lean
new file mode 100644
index 0000000000..862658c163
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxProduct/Width.lean
@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Exec
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct.Bounds
+public import Complexity.Computability.WordRAM.Width
+import Mathlib.Data.List.GetD
+
+/-!
+# Initialized routed box products and every wider execution prefix
+
+The original matrices, raw coordinates and threshold initialize the actual program.
+Exact original-order product values, restored input, pre-halt execution and charged halt
+share one final memory. The minimum-admission run bounds every wider prefix independently
+of its physical width, including all words and memory support.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Actual initialized execution of both original input modes, with one charged halt
+and the same final state containing every matrix-product answer in request order. -/
+theorem runs {w L m t N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (ht : t ≤ m) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hX : ∀ i k, |X i k| ≤ (A : ℤ))
+    (hY : ∀ k j, |Y k j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j))
+    (hmag : magnitudeBound L A < 2 ^ (w - 1))
+    (hfit : Fits (w + 2) (wordBudget L m t N qs.length)) :
+    InputFits (w + 2) (input bits L t X Y qs) ∧
+    ∃ y n, n + 1 ≤ timeBound L m t qs + 1 ∧
+      Runs (w + 2) ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits L t X Y qs)) ⟨(program bits).size, y⟩ n ∧
+      Executes (w + 2) ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits L t X Y qs)) (QueriedProduct.outputBase L m N qs.length) (n + 1) ∧
+      y.Bounded (w + 2) ∧
+      (∀ i : Fin qs.length, y.mem (QueriedProduct.outputBase L m N qs.length + i.val) =
+        Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ p, ¬(QueriedProduct.inputEnd m N qs.length + 1 ≤ p ∧
+        p < memoryEnd L m t N qs.length) →
+        y.mem p = (State.init (input bits L t X Y qs) : State 160).data.mem p) := by
+  have hi := input_fits hw hm bits X Y qs hX hY hmag hfit
+  obtain ⟨y, he, hp, _, hv, hf⟩ := exec hw hm ht bits X Y qs
+    (State.init (input bits L t X Y qs)).data
+    (fun p hp hb => input_prefix bits X Y qs p hp hb)
+    (input_threshold bits X Y qs) hX hY hbits hmag hfit
+  have hy := he.bounded (Data.Bounded.init hi)
+  obtain ⟨n, hn, he⟩ := he
+  refine ⟨hi, y, n, by omega, ?_, ?_, hy, hv, hf⟩
+  · simpa only [Nat.zero_add, State.init] using he.runs (pc := 0)
+      (p := (program bits).program QueriedProduct.Reg.output) (Program.Contains.self _).append_left
+  · simpa only [hp.output, State.init] using he.executes QueriedProduct.Reg.output
+
+/-- Both native input modes run at every sufficiently wide original-input admission.
+The scalar return is the first address of the complete original-order answer array. -/
+theorem runs_wide {W L m t N A : ℕ} (hm : m ≤ L) (ht : t ≤ m) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hX : ∀ i k, |X i k| ≤ (A : ℤ))
+    (hY : ∀ k j, |Y k j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j))
+    (hW : admissionWidth L m t N qs.length A ≤ W) :
+    InputFits W (input bits L t X Y qs) ∧
+    ∃ y n, n + 1 ≤ timeBound L m t qs + 1 ∧
+      Runs W ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits L t X Y qs)) ⟨(program bits).size, y⟩ n ∧
+      Executes W ((program bits).program QueriedProduct.Reg.output)
+        (State.init (input bits L t X Y qs)) (QueriedProduct.outputBase L m N qs.length) (n + 1) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length, y.mem (QueriedProduct.outputBase L m N qs.length + i.val) =
+        Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ p, ¬(QueriedProduct.inputEnd m N qs.length + 1 ≤ p ∧
+        p < memoryEnd L m t N qs.length) →
+        y.mem p = (State.init (input bits L t X Y qs) : State 160).data.mem p) := by
+  obtain ⟨hw, hmag, hfit⟩ := admission_bounds hW
+  have htwo : W - 2 + 2 = W := by unfold admissionWidth at hW; omega
+  simpa only [htwo] using
+    runs hw hm ht bits X Y qs hX hY hbits hmag (by simpa only [htwo] using hfit)
+
+/-- Original-input bounds on every successful prefix, independent of any larger admitted width. -/
+theorem prefix_bounded {W L m t N A : ℕ} (hm : m ≤ L) (ht : t ≤ m) (bits : Bool)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hX : ∀ i k, |X i k| ≤ (A : ℤ))
+    (hY : ∀ k j, |Y k j| ≤ (A : ℤ))
+    (hbits : bits = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j))
+    (hW : admissionWidth L m t N qs.length A ≤ W) (s : State 160) (steps : ℕ)
+    (hr : Runs W ((program bits).program QueriedProduct.Reg.output)
+      (State.init (input bits L t X Y qs)) s steps) :
+    (∀ i, s.data.regs i < wordBound L m t N qs.length A) ∧
+      (∀ p, s.data.mem p < wordBound L m t N qs.length A) ∧
+      ∀ p, wordBound L m t N qs.length A ≤ p → s.data.mem p = 0 := by
+  obtain ⟨hi, _, _, _, _, halt, _⟩ := runs_wide hm ht bits X Y qs hX hY hbits le_rfl
+  have low := Runs.prefix_at_smaller_width
+    (Code.not_readsWidth_program (not_readsWidth bits) QueriedProduct.Reg.output) hW hr halt
+  have hb := low.bounded_init hi
+  have hw := pow_admissionWidth_lt_wordBound L m t N qs.length A
+  refine ⟨fun i => (hb.1 i).trans hw, fun p => (hb.2 p).trans hw, ?_⟩
+  intro p hp
+  have above : 2 ^ admissionWidth L m t N qs.length A ≤ p := hw.le.trans hp
+  rw [low.mem_above (.init hi) above]
+  cases p with
+  | zero => have := Nat.two_pow_pos (admissionWidth L m t N qs.length A); omega
+  | succ p =>
+    change (input bits L t X Y qs).getD p 0 = 0
+    apply List.getD_eq_default
+    have hlen := hi.1
+    dsimp only [Fits] at hlen
+    omega
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
diff --git a/ComplexityTests/SchonhageBoxTradeoff.lean b/ComplexityTests/SchonhageBoxTradeoff.lean
new file mode 100644
index 0000000000..b891f1fa31
--- /dev/null
+++ b/ComplexityTests/SchonhageBoxTradeoff.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoffExponent
+import Mathlib.Tactic.Linarith
+
+/-!
+Concrete threshold, sparse count, empty-depth and nonzero block-parameter clients of
+the finite shared-box tradeoff. These tests assert no native execution or final exponent.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.SchonhageBoxTradeoff
+
+open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.MatrixMultiplication.Schonhage.BoxTradeoff
+
+-- The natural switch rounds upward at the first and next block boundaries.
+#guard ninthThreshold 0 = 0
+#guard ninthThreshold 1 = 1
+#guard ninthThreshold 8 = 1
+#guard ninthThreshold 9 = 1
+#guard ninthThreshold 10 = 2
+#guard ninthThreshold 18 = 2
+
+-- A genuine nonzero sparse query count, rather than a vacuous upper bound.
+example : (∑ d ∈ range 2, alpha 9 d) = 82 := by decide +kernel
+
+-- The smallest finite model has a real tile and retained value, even with no coordinates.
+example : (tiles 0 0 1).card = 1 ∧ (boxes 0 0 0).card = 1 ∧ alpha 0 0 = 1 := by
+  decide +kernel
+
+-- An order threshold beyond the inner depth gives an empty retained-count tail.
+example : (∑ d ∈ Icc 2 1, (beta 21 1 d : ℝ)) = 0 := by simp
+
+-- All admission premises are discharged at positive block depth. The same rational gain
+-- bounds both shared encodings and one nonzero query occurrence.
+example :
+    (numBands 189 9 (D 9 ^ 18) : ℝ) * (10 : ℝ) ^ 189 +
+      ∑ d ∈ range 2, (alpha 9 d : ℝ) ≤
+        5 * (9 / 20 : ℝ) * (D 9 ^ 18 : ℕ) ^ 2 := by
+  have he := encodings_ninth_blocks 1 (D 9 ^ 18) le_rfl
+  have hq := queries_ninth_blocks 1 (D 9 ^ 18) 1 (by decide +kernel)
+  norm_num only [Nat.mul_one, pow_one, one_mul] at he hq
+  nlinarith only [he, hq]
+
+-- The rational exponent conversion is checked at a positive block depth.
+example : (9 / 20 : ℝ) ≤ (D 9 : ℝ) ^ (-(8 / 125 : ℝ)) := by
+  simpa only [pow_one, Nat.mul_one] using decay_le_rpow 1
+
+-- The complete natural-cost shape at zero depth has a real tile, table and query.
+example :
+    ((1 + 1 * D 0 + 1 + 2 ^ 0 +
+      (numBands 0 0 1 + 1) * 10 ^ 0 +
+      numBands 0 0 1 ^ 2 * ((boxes 0 0 0).card + 1) +
+      1 * (∑ d ∈ range 1, alpha 0 d) : ℕ) : ℝ) ≤
+        80 * ((0 : ℕ) + 1 : ℝ) * (9 / 20 : ℝ) ^ 0 * (1 : ℝ) ^ 2 := by
+  simpa only [Nat.mul_zero, Nat.zero_add, Nat.cast_one] using
+    nativeShape_ninth_blocks 0 1 1 (by decide +kernel) (by decide +kernel)
+
+end ComplexityTests.SchonhageBoxTradeoff
diff --git a/ComplexityTests/WordRAMSchonhageBoxProduct.lean b/ComplexityTests/WordRAMSchonhageBoxProduct.lean
new file mode 100644
index 0000000000..509e135dc4
--- /dev/null
+++ b/ComplexityTests/WordRAMSchonhageBoxProduct.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+/-!
+Complete native routed box-product regressions. Original matrices and coordinates are
+routed and encoded by the real producers, one shared geometry is built, and every tile
+runs the retained-value/sparse-query kernels. Input restoration includes the ordinary
+appended threshold and native length header.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.WordRAMSchonhageBoxProduct
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxProduct
+
+private def X : Matrix (Fin 2) (Fin (D 0)) ℤ := fun i _ => ![-3, 4] i
+private def Y : Matrix (Fin (D 0)) (Fin 2) ℤ := fun _ j => ![2, -5] j
+private def queries : List (Fin 2 × Fin 2) := [(1, 0), (0, 1), (1, 0), (0, 0)]
+
+private def dirtyInput : Data 160 :=
+  let x := (State.init (input false 0 0 X Y queries) : State 160).data
+  { x with mem := fun p =>
+      if QueriedProduct.inputEnd 0 2 queries.length < p then 777 else x.mem p }
+
+-- Four different tiles reuse one real geometry; request order and repetitions survive.
+-- Every original word is restored, and a far dirty sentinel lies outside the allocation.
+#guard match (program false).eval 64 10000 dirtyInput with
+  | some (y, _) =>
+      y.mem (QueriedProduct.outputBase 0 0 2 4) == encode 8 &&
+      y.mem (QueriedProduct.outputBase 0 0 2 4 + 1) == encode 15 &&
+      y.mem (QueriedProduct.outputBase 0 0 2 4 + 2) == encode 8 &&
+      y.mem (QueriedProduct.outputBase 0 0 2 4 + 3) == encode (-6) &&
+      y.mem 100000 == 777 &&
+      (List.range (QueriedProduct.inputEnd 0 2 4 + 1)).all
+        (fun p => y.mem p == dirtyInput.mem p)
+  | none => false
+
+private def emptyX : Matrix (Fin 0) (Fin (D 0)) ℤ := fun i _ => Fin.elim0 i
+private def emptyY : Matrix (Fin (D 0)) (Fin 0) ℤ := fun _ j => Fin.elim0 j
+
+-- With no bands or wanted coordinates, the tile loop exits before any division by zero.
+#guard match (program false).eval 64 10000
+    (State.init (input false 0 0 emptyX emptyY [])).data with
+  | some (y, _) => y.regs QueriedProduct.Reg.index == 0 &&
+      y.mem (QueriedProduct.inputEnd 0 0 0) == 0
+  | none => false
+
+private def innerX : Matrix (Fin 1) (Fin (D 1)) ℤ := fun _ k => ![1, -2, 3, 0] k
+private def innerY : Matrix (Fin (D 1)) (Fin 1) ℤ := fun k _ => ![4, 5, -1, 2] k
+
+-- Positive depth and signed cancellation, using retained starred values at threshold zero.
+#guard match (program false).eval 64 10000
+    (State.init (input false 1 0 innerX innerY [(0, 0), (0, 0)])).data with
+  | some (y, _) => y.mem (QueriedProduct.outputBase 1 1 1 2) == encode (-9) &&
+      y.mem (QueriedProduct.outputBase 1 1 1 2 + 1) == encode (-9) &&
+      y.mem (QueriedProduct.inputEnd 1 1 2) == 0
+  | none => false
+
+-- The same source product through low-order multiplication and singleton box lookups.
+#guard match (program false).eval 64 10000
+    (State.init (input false 1 1 innerX innerY [(0, 0)])).data with
+  | some (y, _) => y.mem (QueriedProduct.outputBase 1 1 1 1) == encode (-9) &&
+      y.mem (QueriedProduct.inputEnd 1 1 1) == 1
+  | none => false
+
+private def rawX : Matrix (Fin 2) (Fin (D 0)) ℤ := fun i _ => ![1, 0] i
+private def rawY : Matrix (Fin (D 0)) (Fin 2) ℤ := fun _ j => ![0, 1] j
+
+-- Actual raw-word conversion is part of the native program, as needed by the ET frontend.
+#guard match (program true).eval 64 10000
+    (State.init (input true 0 0 rawX rawY [(0, 1), (1, 0), (0, 1)])).data with
+  | some (y, _) => y.mem (QueriedProduct.outputBase 0 0 2 3) == encode 1 &&
+      y.mem (QueriedProduct.outputBase 0 0 2 3 + 1) == encode 0 &&
+      y.mem (QueriedProduct.outputBase 0 0 2 3 + 2) == encode 1
+  | none => false
+
+-- Original signed matrices, four raw coordinate occurrences and every admission premise
+-- instantiate the finite thin-product endpoint. Prefix, halt, charge and answers share y.
+example : ∃ (y : Data 160) (n : ℕ),
+    n + 1 ≤ 10485760 ∧
+    Runs 64 ((program false).program QueriedProduct.Reg.output)
+      (State.init (input false 0 0 X Y queries)) ⟨(program false).size, y⟩ n ∧
+    Executes 64 ((program false).program QueriedProduct.Reg.output)
+      (State.init (input false 0 0 X Y queries)) (QueriedProduct.outputBase 0 0 2 4) (n + 1) ∧
+    y.mem (QueriedProduct.outputBase 0 0 2 4) = encode 8 ∧
+    y.mem (QueriedProduct.outputBase 0 0 2 4 + 3) = encode (-6) ∧
+    y.mem 0 = (input false 0 0 X Y queries).length := by
+  obtain ⟨_, y, n, hn, hp, he, _, hv, hf⟩ :=
+    runs_thin (W := 64) (k := 0) (N := 2) (A := 5) false X Y queries
+      (by decide +kernel) (by decide +kernel) (by simp) (by decide +kernel)
+      (by decide +kernel) (by decide +kernel)
+  have hn' : n + 1 ≤ 10485760 := by
+    norm_num [D] at hn
+    exact_mod_cast hn
+  have h0 := hv ⟨0, by decide⟩
+  have h3 := hv ⟨3, by decide⟩
+  have v0 : (X * Y) (queries.get ⟨0, by decide⟩).1 (queries.get ⟨0, by decide⟩).2 = 8 := by
+    decide +kernel
+  have v3 : (X * Y) (queries.get ⟨3, by decide⟩).1 (queries.get ⟨3, by decide⟩).2 = -6 := by
+    decide +kernel
+  refine ⟨y, n, hn', hp, he, ?_, ?_, ?_⟩
+  · simpa only [v0, Fin.val_zero, Nat.add_zero, Nat.mul_zero,
+      show queries.length = 4 from rfl] using h0
+  · simpa only [v3, Nat.mul_zero, show queries.length = 4 from rfl] using h3
+  · rw [hf 0 (by unfold QueriedProduct.inputEnd; omega)]
+    rfl
+
+-- Empty matrices and requests also instantiate the complete minimum-width initialized run.
+example : ∃ (y : Data 160) (n : ℕ),
+    Runs (admissionWidth 0 0 0 0 0 0) ((program false).program QueriedProduct.Reg.output)
+      (State.init (input false 0 0 emptyX emptyY [])) ⟨(program false).size, y⟩ n ∧
+    Executes (admissionWidth 0 0 0 0 0 0)
+      ((program false).program QueriedProduct.Reg.output)
+      (State.init (input false 0 0 emptyX emptyY [])) (QueriedProduct.outputBase 0 0 0 0) (n + 1) ∧
+    y.mem (QueriedProduct.inputEnd 0 0 0) = 0 := by
+  obtain ⟨_, y, n, _, hp, he, _, _, hf⟩ :=
+    runs_wide (W := admissionWidth 0 0 0 0 0 0) (L := 0) (m := 0) (t := 0) (A := 0)
+      (by decide) (by decide) false emptyX emptyY []
+      (by intro i; exact Fin.elim0 i) (by intro _ j; exact Fin.elim0 j) (by simp) le_rfl
+  refine ⟨y, n, hp, he, ?_⟩
+  rw [hf _ (by simp only [List.length_nil]; omega)]
+  exact input_threshold false emptyX emptyY []
+
+end ComplexityTests.WordRAMSchonhageBoxProduct
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 415fcfe63a..adafc97518 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -441,9 +441,23 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   least significant and the inner `P0` digit is nine. Actual initialized preparation,
   same-witness prefix/halt and outside frame are proved; a logarithm of original magnitudes
   and addresses admits all wider machines, with an independent-width polynomial envelope
-  for every prefix. Shared table setup and retained storage remain explicit. Global all-tile
-  reuse, wanted-query construction, Corollary 26/ET integration and the tuned 1.9992 endpoint
-  remain #1394; this milestone changes no curated abstract or rendering.
+  for every prefix. Shared table setup and retained storage remain explicit. The following
+  routed-product component supplies all-tile reuse and actual routing; remaining endpoint
+  composition stays #1394. This query milestone changes no curated abstract or rendering.
+* **Routed native box product.** [#2314](https://github.com/cslib-community/complexitylib/issues/2314)
+  reuses the existing actual raw-coordinate router, shared band producer and original-order
+  reconstruction. One native geometry construction serves all tiles; each actual retained-value
+  table and sparse query batch is charged, including temporary-result copies and every repeated
+  request occurrence. An appended ordinary threshold is read before low-memory reuse and restored
+  with all original input words. No computed layout, routing, encoding, table, run or time oracle
+  is supplied. The original native controller preserves the existing source terms and numbering.
+  The finite `BoxTradeoff` modules adapt the Section 4 geometric-tail and weighted-binomial
+  estimates at the same formal-math pin, with an original algebraic block specialization
+  `L=189k`, `m=9k`, `t=k`. Under `D^18≤N` and `Q*2^m≤N²`, the complete actual ledger has
+  finite `D^(-8/125)` saving with polynomial depth factors explicit. Here `Q` counts occurrences,
+  strengthening distinct-set sparsity when inputs repeat. Exact integer comparisons replace
+  analytic numerical approximations. Polynomial-factor absorption, ET replacement, parameter
+  retuning and tuned ordinary-3SUM 1.9992 remain #1394. No curated abstract or rendering changes.
 * **Native pruned-query evaluator.** The explicit-stack pruned-query evaluator ([#1526](https://github.com/cslib-community/complexitylib/issues/1526))
   is original native code, reusing the finite `Pruned.result`, `childSet` and trace/leaf
   quantities from `Sec2/Lemma10.lean`. `PrunedQuery.queryIndex` directly applies the existing