diff --git a/Complexity.lean b/Complexity.lean
index 6435eed4ee..15798f54f4 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -52,7 +52,12 @@ public import Complexity.Algorithms.Lean.Submodular.Greedy
 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.BoxValues
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Boxes
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BoxesFromLeaves
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Cubes
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Full
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Identity
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Layout
@@ -3480,6 +3485,7 @@ public import Complexity.Foundations.Data.Finset.Expect
 public import Complexity.Foundations.Data.Finset.Finpartition
 public import Complexity.Foundations.Data.Finset.KthLargest
 public import Complexity.Foundations.Data.Finset.KthLargest.Truncation
+public import Complexity.Foundations.Data.Finset.Lowest
 public import Complexity.Foundations.Data.Finset.Markov
 public import Complexity.Foundations.Data.Finset.OrderGlue
 public import Complexity.Foundations.Data.Finset.OrderedFilter
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxPartition.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxPartition.lean
new file mode 100644
index 0000000000..99ed3f2866
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxPartition.lean
@@ -0,0 +1,484 @@
+/-
+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
+
+/-!
+# Disjoint box decomposition of the contributing leaves
+
+For an output with `m` inner levels and `t ≤ m`, pad each high-order leaf's P0 levels
+from below. Its resulting box is unique. Different indexing sets give disjoint box
+families, and their leaf sets partition exactly the high-order contributing leaves.
+The remaining low-order leaves are explicit in `boxQuery`; `bilinearProduct_eq_boxQuery`
+holds for arbitrary signed input arrays, including cancellation.
+
+The level assignment is finite algebra from [AlmanWilliams2026, Lemmas 27–28], adapted
+from [Lemma27_28.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Lemma27_28.lean) at
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+It uses the existing alphabets, encodings, contribution relation, signed leaf order
+and alpha counts. There is no assumed native lookup, enumeration, layout or cost contract.
+-/
+
+public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Pad a restricted P0 set with the lowest remaining levels to the threshold size. -/
+@[expose] def paddedLevels {L : ℕ} (m t : ℕ) (Q Z : Finset (Fin L)) : Finset (Fin L) :=
+  Z ∪ lowest (m - t - Z.card) (Q \ Z)
+
+/-- Levels preceding every omitted level; if none are omitted this is all of `Q`. -/
+@[expose] def initialLevels {L : ℕ} (Q V : Finset (Fin L)) : Finset (Fin L) :=
+  Q.filter fun ℓ => ∀ ℓ' ∈ Q \ V, ℓ < ℓ'
+
+/-- Cubes for an output and an indexing set, with stars, fixed P0, nine-way and private regions. -/
+@[expose] def boxesAt {L : ℕ} (η : OutStr L) (V : Finset (Fin L)) : Finset (Cube L) :=
+  univ.filter fun π => ∀ ℓ,
+    (ℓ ∈ initialLevels (innerSetO η) V → π ℓ = .star) ∧
+    (ℓ ∈ V \ initialLevels (innerSetO η) V → π ℓ = .term .P0) ∧
+    (ℓ ∈ innerSetO η \ V → ∃ i j, π ℓ = .term (.P i j)) ∧
+    (ℓ ∉ innerSetO η → π ℓ = .term (privateLeaf η ℓ))
+
+/-- Eligible indexing sets have the required cardinality within the output's inner levels. -/
+@[expose] def boxLevelSets {L : ℕ} (m t : ℕ) (η : OutStr L) : Finset (Finset (Fin L)) :=
+  (innerSetO η).powersetCard (m - t)
+
+/-- The contributing leaves below the order threshold, retained explicitly in every query. -/
+@[expose] def lowLeaves {L : ℕ} (m t : ℕ) (η : OutStr L) : Finset (Leaf L) :=
+  univ.filter fun τ => Leaf.Contributes τ η ∧ order m τ < (t : ℤ)
+
+/-- Complete finite query expression: low-order products plus the values of the output's boxes. -/
+@[expose] def boxQuery {L : ℕ} (m t : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ)
+    (η : OutStr L) : ℤ :=
+  ∑ τ ∈ lowLeaves m t η, encodeLeft τ a * encodeRight τ b +
+    ∑ V ∈ boxLevelSets m t η, ∑ π ∈ boxesAt η V, Cube.val a b π
+
+variable {L : ℕ}
+
+/-- The P0 coordinates of a leaf lying in the selected levels. -/
+@[expose] def P0LevelsWithin (Q : Finset (Fin L)) (τ : Leaf L) : Finset (Fin L) :=
+  Q.filter fun ℓ => τ ℓ = Term.P0
+
+private lemma contributes_iff_eq_privateLeaf (η : OutStr L) (τ : Leaf L) :
+    Leaf.Contributes τ η ↔ ∀ ℓ, ℓ ∉ innerSetO η → τ ℓ = privateLeaf η ℓ := by
+  refine forall_congr' fun ℓ => ?_
+  rw [Term.contributes_iff, mem_innerSetO]
+  exact or_iff_not_imp_left
+
+private lemma privateLeaf_ne_P0 {η : OutStr L} {ℓ : Fin L} (hℓ : ℓ ∉ innerSetO η) :
+    privateLeaf η ℓ ≠ Term.P0 :=
+  fun h => hℓ (mem_innerSetO.2 ((OutVar.privateTerm_eq_P0_iff _).1 h))
+
+private lemma P0LevelsWithin_subset (Q : Finset (Fin L)) (τ : Leaf L) : P0LevelsWithin Q τ ⊆ Q :=
+  filter_subset _ _
+
+private lemma P0Levels_eq_P0LevelsWithin (η : OutStr L) (τ : Leaf L) (hτ : Leaf.Contributes τ η) :
+    P0Levels τ = P0LevelsWithin (innerSetO η) τ := by
+  ext ℓ
+  rw [P0LevelsWithin, mem_filter, mem_P0Levels]
+  exact ⟨fun h => ⟨P0Levels_subset hτ (mem_P0Levels.2 h), h⟩, fun h => h.2⟩
+
+/-- Restricted P0 coordinates determine the order of a contributing leaf. -/
+theorem order_eq_sub_card_P0LevelsWithin (m : ℕ) (η : OutStr L) (τ : Leaf L)
+    (hτ : Leaf.Contributes τ η) :
+    order m τ = (m : ℤ) - ((P0LevelsWithin (innerSetO η) τ).card : ℤ) := by
+  rw [order, P0Levels_eq_P0LevelsWithin η τ hτ]
+
+private lemma card_P0LevelsWithin_le {m t : ℕ} {η : OutStr L} {τ : Leaf L} (hτ : Leaf.Contributes
+  τ η)
+    (hord : (t : ℤ) ≤ order m τ) : (P0LevelsWithin (innerSetO η) τ).card ≤ m - t := by
+  have := order_eq_sub_card_P0LevelsWithin m η τ hτ
+  omega
+
+/-- Padding stays within its ambient set. -/
+theorem paddedLevels_subset (m t : ℕ) {Q Z : Finset (Fin L)} (hZ : Z ⊆ Q) : paddedLevels m t Q Z ⊆
+  Q :=
+  union_subset hZ ((lowest_subset _ _).trans sdiff_subset)
+
+/-- Padding has the prescribed size under the explicit cardinality premises. -/
+theorem card_paddedLevels {m t : ℕ} (ht : t ≤ m) {Q Z : Finset (Fin L)} (hQ : Q.card = m) (hZ : Z
+  ⊆ Q)
+    (hZc : Z.card ≤ m - t) : (paddedLevels m t Q Z).card = m - t := by
+  have hdisj : Disjoint Z (lowest (m - t - Z.card) (Q \ Z)) :=
+    disjoint_of_subset_right (lowest_subset _ _) disjoint_sdiff
+  rw [paddedLevels, card_union_of_disjoint hdisj, card_lowest, card_sdiff_of_subset hZ, hQ]
+  omega
+
+private lemma paddedLevels_sdiff_lt (m t : ℕ) (Q Z : Finset (Fin L)) :
+    ∀ ℓ ∈ paddedLevels m t Q Z \ Z, ∀ ℓ' ∈ Q \ paddedLevels m t Q Z, ℓ < ℓ' := by
+  intro ℓ hℓ ℓ' hℓ'
+  obtain ⟨hV, hZ⟩ := mem_sdiff.1 hℓ
+  obtain ⟨hQ', hV'⟩ := mem_sdiff.1 hℓ'
+  obtain ⟨hZ', hlow'⟩ := not_or.1 (mt mem_union.2 hV')
+  exact lowest_lt ((mem_union.1 hV).resolve_left hZ)
+    (mem_sdiff.2 ⟨mem_sdiff.2 ⟨hQ', hZ'⟩, hlow'⟩)
+
+/-- The initial levels are all levels at the boundary, or those below the first omission. -/
+theorem initialLevels_eq (Q V : Finset (Fin L)) :
+    initialLevels Q Q = Q ∧ ∀ h : (Q \ V).Nonempty, initialLevels Q V = Q.filter fun ℓ => ℓ < (Q \
+      V).min' h := by
+  refine ⟨by simp [initialLevels], fun h => filter_congr fun ℓ _ => ?_⟩
+  rw [lt_min'_iff]
+
+/-- The initial levels lie inside the selected set. -/
+theorem initialLevels_subset (Q V : Finset (Fin L)) : initialLevels Q V ⊆ V := by
+  intro ℓ hℓ
+  by_contra hV
+  exact lt_irrefl ℓ ((mem_filter.1 hℓ).2 ℓ (mem_sdiff.2 ⟨(mem_filter.1 hℓ).1, hV⟩))
+
+private lemma mem_initialLevels_of_le {Q V : Finset (Fin L)} {ℓ ℓ' : Fin L} (hℓ : ℓ ∈
+  initialLevels Q V)
+    (hℓ' : ℓ' ∈ Q) (hle : ℓ' ≤ ℓ) : ℓ' ∈ initialLevels Q V :=
+  mem_filter.2 ⟨hℓ', fun x hx => hle.trans_lt ((mem_filter.1 hℓ).2 x hx)⟩
+
+private lemma sdiff_initialLevels_subset_iff {Q V Z : Finset (Fin L)} (hV : V ⊆ Q) :
+    V \ initialLevels Q V ⊆ Z ↔ ∀ ℓ ∈ V \ Z, ∀ ℓ' ∈ Q \ V, ℓ < ℓ' := by
+  constructor
+  · intro h ℓ hℓ ℓ' hℓ'
+    obtain ⟨hℓV, hℓZ⟩ := mem_sdiff.1 hℓ
+    have hℓF : ℓ ∈ initialLevels Q V := by
+      by_contra hF
+      exact hℓZ (h (mem_sdiff.2 ⟨hℓV, hF⟩))
+    exact (mem_filter.1 hℓF).2 ℓ' hℓ'
+  · intro h ℓ hℓ
+    obtain ⟨hℓV, hℓF⟩ := mem_sdiff.1 hℓ
+    by_contra hZ
+    exact hℓF (mem_filter.2 ⟨hV hℓV, h ℓ (mem_sdiff.2 ⟨hℓV, hZ⟩)⟩)
+
+section boxesAt
+
+variable {η : OutStr L} {V : Finset (Fin L)} {π : Cube L} {ℓ : Fin L}
+
+private lemma boxesAt_star (hπ : π ∈ boxesAt η V) (hℓ : ℓ ∈ initialLevels (innerSetO η) V) : π ℓ =
+  CubeSymbol.star :=
+  ((mem_filter.1 hπ).2 ℓ).1 hℓ
+
+private lemma boxesAt_P0 (hπ : π ∈ boxesAt η V) (hℓ : ℓ ∈ V \ initialLevels (innerSetO η) V) :
+    π ℓ = CubeSymbol.term Term.P0 :=
+  ((mem_filter.1 hπ).2 ℓ).2.1 hℓ
+
+private lemma boxesAt_nine (hπ : π ∈ boxesAt η V) (hℓ : ℓ ∈ innerSetO η \ V) :
+    ∃ i j, π ℓ = CubeSymbol.term (Term.P i j) :=
+  ((mem_filter.1 hπ).2 ℓ).2.2.1 hℓ
+
+private lemma boxesAt_outside (hπ : π ∈ boxesAt η V) (hℓ : ℓ ∉ innerSetO η) :
+    π ℓ = CubeSymbol.term (privateLeaf η ℓ) :=
+  ((mem_filter.1 hπ).2 ℓ).2.2.2 hℓ
+
+private lemma level_cases (Q V : Finset (Fin L)) (ℓ : Fin L) :
+    ℓ ∈ initialLevels Q V ∨ ℓ ∈ V \ initialLevels Q V ∨ ℓ ∈ Q \ V ∨ ℓ ∉ Q := by
+  simp only [mem_sdiff]
+  tauto
+
+/-- The stars of a family member are exactly its initial levels. -/
+theorem boxesAt_starLevels (hπ : π ∈ boxesAt η V) : Cube.starLevels π = initialLevels (innerSetO
+  η) V := by
+  ext ℓ
+  rw [Cube.mem_starLevels]
+  refine ⟨fun h => ?_, boxesAt_star hπ⟩
+  rcases level_cases (innerSetO η) V ℓ with hℓ | hℓ | hℓ | hℓ
+  · exact hℓ
+  · simp [boxesAt_P0 hπ hℓ] at h
+  · obtain ⟨i, j, hij⟩ := boxesAt_nine hπ hℓ
+    simp [hij] at h
+  · simp [boxesAt_outside hπ hℓ] at h
+
+/-- Fixed P0 coordinates occupy the rest of the selected levels. -/
+theorem boxesAt_P0Levels (hπ : π ∈ boxesAt η V) : Cube.P0Levels π = V \ initialLevels (innerSetO
+  η) V := by
+  ext ℓ
+  rw [Cube.mem_P0Levels]
+  refine ⟨fun h => ?_, boxesAt_P0 hπ⟩
+  rcases level_cases (innerSetO η) V ℓ with hℓ | hℓ | hℓ | hℓ
+  · simp [boxesAt_star hπ hℓ] at h
+  · exact hℓ
+  · obtain ⟨i, j, hij⟩ := boxesAt_nine hπ hℓ
+    simp [hij] at h
+  · rw [boxesAt_outside hπ hℓ] at h
+    exact absurd (CubeSymbol.term.inj h) (privateLeaf_ne_P0 hℓ)
+
+/-- A family member recovers its indexing set from its stars and P0 symbols. -/
+theorem boxesAt_starLevels_union_P0Levels (hπ : π ∈ boxesAt η V) :
+    Cube.starLevels π ∪ Cube.P0Levels π = V := by
+  rw [boxesAt_starLevels hπ, boxesAt_P0Levels hπ, union_sdiff_of_subset (initialLevels_subset _ _)]
+
+private lemma boxesAt_ext {π' : Cube L} (hπ : π ∈ boxesAt η V) (hπ' : π' ∈ boxesAt η V)
+    (h : ∀ ℓ ∈ innerSetO η \ V, π ℓ = π' ℓ) : π = π' := by
+  funext ℓ
+  rcases level_cases (innerSetO η) V ℓ with hℓ | hℓ | hℓ | hℓ
+  · rw [boxesAt_star hπ hℓ, boxesAt_star hπ' hℓ]
+  · rw [boxesAt_P0 hπ hℓ, boxesAt_P0 hπ' hℓ]
+  · exact h ℓ hℓ
+  · rw [boxesAt_outside hπ hℓ, boxesAt_outside hπ' hℓ]
+
+private lemma boxesAt_eq_term_of_leaf (hπ : π ∈ boxesAt η V) {τ : Leaf L} (hτ : τ ∈ Cube.leaves π)
+    (hℓ : ℓ ∈ innerSetO η \ V) : π ℓ = CubeSymbol.term (τ ℓ) := by
+  obtain ⟨i, j, hij⟩ := boxesAt_nine hπ hℓ
+  rw [hij, Cube.eq_of_mem_leaves hτ hij]
+
+end boxesAt
+
+private def allowed (η : OutStr L) (V : Finset (Fin L)) (ℓ : Fin L) : Finset CubeSymbol :=
+  univ.filter fun s =>
+    (ℓ ∈ initialLevels (innerSetO η) V → s = CubeSymbol.star) ∧
+    (ℓ ∈ V \ initialLevels (innerSetO η) V → s = CubeSymbol.term Term.P0) ∧
+    (ℓ ∈ innerSetO η \ V → ∃ i j, s = CubeSymbol.term (Term.P i j)) ∧
+    (ℓ ∉ innerSetO η → s = CubeSymbol.term (privateLeaf η ℓ))
+
+private lemma boxesAt_eq_piFinset (η : OutStr L) (V : Finset (Fin L)) :
+    boxesAt η V = Fintype.piFinset (allowed η V) := by
+  ext π
+  simp [boxesAt, allowed, Fintype.mem_piFinset]
+
+private lemma card_allowed (η : OutStr L) (V : Finset (Fin L)) (hV : V ⊆ innerSetO η)
+    (ℓ : Fin L) : (allowed η V ℓ).card = if ℓ ∈ innerSetO η \ V then 9 else 1 := by
+  have hnine :
+      (univ.filter fun s : CubeSymbol => ∃ i j, s = CubeSymbol.term (Term.P i j)).card = 9 := by
+    decide
+  have hinitialLevels := @initialLevels_subset L (innerSetO η) V ℓ
+  have hVQ := @hV ℓ
+  unfold allowed
+  by_cases hF : ℓ ∈ initialLevels (innerSetO η) V
+  · simp [hF, hinitialLevels hF, hVQ (hinitialLevels hF), filter_eq']
+  by_cases hℓV : ℓ ∈ V
+  · simp [hF, hℓV, hVQ hℓV, filter_eq']
+  by_cases hℓQ : ℓ ∈ innerSetO η
+  · simp [hF, hℓV, hℓQ, hnine]
+  · simp [hF, hℓV, hℓQ, filter_eq']
+
+/-- There are nine choices at each free inner coordinate and one at every other coordinate. -/
+theorem card_boxesAt (m t : ℕ) (ht : t ≤ m) (η : OutStr L) (hη : (innerSetO η).card = m)
+    (V : Finset (Fin L)) (hV : V ∈ boxLevelSets m t η) : (boxesAt η V).card = 9 ^ t := by
+  obtain ⟨hVQ, hVc⟩ := mem_powersetCard.1 hV
+  rw [boxesAt_eq_piFinset η V, Fintype.card_piFinset]
+  simp only [card_allowed η V hVQ]
+  rw [prod_ite_mem_const, one_pow, mul_one, card_sdiff_of_subset hVQ, hη, hVc,
+    Nat.sub_sub_self ht]
+
+/-- Every member of an eligible output family satisfies the global box conditions. -/
+theorem boxesAt_isBox {m t : ℕ} {η : OutStr L} {V : Finset (Fin L)} (hV : V ∈ boxLevelSets m t η)
+  {π : Cube L}
+    (hπ : π ∈ boxesAt η V) : IsBox m t π := by
+  obtain ⟨hVQ, hVc⟩ := mem_powersetCard.1 hV
+  rw [IsBox, boxesAt_starLevels hπ, boxesAt_P0Levels hπ, add_comm,
+    card_sdiff_add_card_eq_card (initialLevels_subset _ _)]
+  refine ⟨hVc.le, fun ℓ hℓ ℓ' hℓ' => ?_⟩
+  obtain ⟨hℓ'V, hℓ'F⟩ := mem_sdiff.1 hℓ'
+  by_contra hlt
+  exact hℓ'F (mem_initialLevels_of_le hℓ (hVQ hℓ'V) (not_lt.1 hlt))
+
+/-- Different indexing sets give disjoint families of cubes. -/
+theorem boxesAt_pairwiseDisjoint (η : OutStr L) (s : Set (Finset (Fin L))) :
+    s.PairwiseDisjoint (boxesAt η) :=
+  fun _ _ _ _ hne => disjoint_left.2 fun _ hπ hπ' =>
+    hne ((boxesAt_starLevels_union_P0Levels hπ).symm.trans (boxesAt_starLevels_union_P0Levels hπ'))
+
+private lemma starAt_mem_boxesAt {η : OutStr L} {V : Finset (Fin L)} {τ : Leaf L}
+    (hτ : Leaf.Contributes τ η) (hVZ : V \ initialLevels (innerSetO η) V ⊆ P0LevelsWithin
+      (innerSetO η) τ)
+    (hZV : P0LevelsWithin (innerSetO η) τ ⊆ V) : Cube.starAt (initialLevels (innerSetO η) V) τ ∈
+      boxesAt η V := by
+  refine mem_filter.2
+    ⟨mem_univ _, fun ℓ => ⟨fun hF => ite_eq_left hF, fun hVF => ?_, fun hQV => ?_, fun hQ => ?_⟩⟩
+  · -- at a level of `V ∖ F_V`, which is a level of `Z`, the leaf chooses `P₀`
+    rw [Cube.starAt, ite_eq_right (mem_sdiff.1 hVF).2, (mem_filter.1 (hVZ hVF)).2]
+  · -- at a level of `Q ∖ V`, which is not a level of `Z`, the leaf chooses another term
+    obtain ⟨hQ, hV⟩ := mem_sdiff.1 hQV
+    rw [Cube.starAt, ite_eq_right fun hF => hV (initialLevels_subset _ _ hF)]
+    cases hterm : τ ℓ with
+    | P i j => exact ⟨i, j, rfl⟩
+    | P0 => exact absurd (hZV (mem_filter.2 ⟨hQ, hterm⟩)) hV
+  · -- outside `Q` the leaf agrees with the private leaf
+    rw [Cube.starAt, ite_eq_right fun hF : ℓ ∈ initialLevels (innerSetO η) V => hQ (mem_filter.1
+      hF).1,
+      (contributes_iff_eq_privateLeaf η τ).1 hτ ℓ hQ]
+
+/-- Assign a cube by starring the initial levels of the padded P0 set. -/
+@[expose] def boxOfLeaf (m t : ℕ) (η : OutStr L) (τ : Leaf L) : Cube L :=
+  Cube.starAt (initialLevels (innerSetO η) (paddedLevels m t (innerSetO η) (P0LevelsWithin
+    (innerSetO η) τ))) τ
+
+/-- The assignment retains its original leaf. -/
+theorem mem_leaves_boxOfLeaf (m t : ℕ) (η : OutStr L) (τ : Leaf L) :
+    τ ∈ Cube.leaves (boxOfLeaf m t η τ) :=
+  Cube.mem_leaves_starAt _ τ
+
+/-- The assigned cube belongs to the family indexed by the padded P0 set. -/
+theorem boxOfLeaf_mem_boxesAt (m t : ℕ) {η : OutStr L} {τ : Leaf L} (hτ : Leaf.Contributes τ η) :
+    boxOfLeaf m t η τ ∈ boxesAt η (paddedLevels m t (innerSetO η) (P0LevelsWithin (innerSetO η)
+      τ)) :=
+  starAt_mem_boxesAt hτ
+    ((sdiff_initialLevels_subset_iff (paddedLevels_subset m t (P0LevelsWithin_subset _ τ))).2
+      (paddedLevels_sdiff_lt m t _ _))
+    subset_union_left
+
+/-- Leaf incidence in a family is equivalent to the two P0-set inclusions. -/
+theorem exists_mem_boxesAt_leaf_iff {η : OutStr L} {V : Finset (Fin L)} (hV : V ⊆ innerSetO η)
+    {τ : Leaf L} (hτ : Leaf.Contributes τ η) :
+    (∃ π ∈ boxesAt η V, τ ∈ Cube.leaves π) ↔
+      V \ initialLevels (innerSetO η) V ⊆ P0LevelsWithin (innerSetO η) τ ∧ P0LevelsWithin
+        (innerSetO η) τ ⊆ V := by
+  constructor
+  · rintro ⟨π, hπ, hτπ⟩
+    refine ⟨fun ℓ hℓ => mem_filter.2 ⟨hV (mem_sdiff.1 hℓ).1, ?_⟩, fun ℓ hℓ => ?_⟩
+    · exact Cube.eq_of_mem_leaves hτπ (boxesAt_P0 hπ hℓ)
+    · by_contra hℓV
+      obtain ⟨hℓQ, hterm⟩ := mem_filter.1 hℓ
+      obtain ⟨i, j, hij⟩ := boxesAt_nine hπ (mem_sdiff.2 ⟨hℓQ, hℓV⟩)
+      simp [Cube.eq_of_mem_leaves hτπ hij] at hterm
+  · exact fun ⟨hVZ, hZV⟩ => ⟨_, starAt_mem_boxesAt hτ hVZ hZV, Cube.mem_leaves_starAt _ τ⟩
+
+/-- Within a single family, a leaf determines its cube. -/
+theorem boxesAt_leaf_unique {η : OutStr L} {V : Finset (Fin L)} {τ : Leaf L} {π π' : Cube L}
+    (hπ : π ∈ boxesAt η V) (hτπ : τ ∈ Cube.leaves π) (hπ' : π' ∈ boxesAt η V) (hτπ' : τ ∈
+      Cube.leaves π') :
+    π = π' :=
+  boxesAt_ext hπ hπ' fun _ hℓ =>
+    (boxesAt_eq_term_of_leaf hπ hτπ hℓ).trans (boxesAt_eq_term_of_leaf hπ' hτπ' hℓ).symm
+
+/-- The prescribed padding is the unique set satisfying both incidence inclusions. -/
+theorem paddedLevels_unique {L : ℕ} (m t : ℕ) (ht : t ≤ m) (Q Z : Finset (Fin L)) (hQ : Q.card = m)
+    (hZ : Z ⊆ Q) (hZc : Z.card ≤ m - t) (V : Finset (Fin L)) :
+    (V ⊆ Q ∧ V.card = m - t ∧ V \ initialLevels Q V ⊆ Z ∧ Z ⊆ V) ↔ V = paddedLevels m t Q Z := by
+  constructor
+  · rintro ⟨hVQ, hVc, hVZ, hZV⟩
+    have hrest : (Q \ Z) \ (V \ Z) = Q \ V := sdiff_sdiff_sdiff_cancel_right hZV
+    have hlow := eq_lowest_of_lt (sdiff_subset_sdiff hVQ (le_refl Z))
+      (hrest ▸ (sdiff_initialLevels_subset_iff hVQ).1 hVZ)
+    rw [card_sdiff_of_subset hZV, hVc] at hlow
+    rw [paddedLevels, ← hlow, union_sdiff_of_subset hZV]
+  · rintro rfl
+    have hVQ := paddedLevels_subset m t hZ
+    exact ⟨hVQ, card_paddedLevels ht hQ hZ hZc, (sdiff_initialLevels_subset_iff hVQ).2
+      (paddedLevels_sdiff_lt m t Q Z),
+      subset_union_left⟩
+
+/-- The families cover exactly the contributing leaves above the threshold. -/
+theorem contributes_high_iff_mem_box_leaves {L : ℕ} (m t : ℕ) (ht : t ≤ m) (η : OutStr L) (hη :
+  (innerSetO η).card = m)
+    (τ : Leaf L) :
+    (Leaf.Contributes τ η ∧ (t : ℤ) ≤ order m τ) ↔
+      ∃ π ∈ (boxLevelSets m t η).biUnion (boxesAt η), τ ∈ Cube.leaves π := by
+  constructor
+  · -- "Conversely, a leaf τ contributing to w, of order at least t," is a leaf of its box.
+    rintro ⟨hτ, hord⟩
+    refine ⟨boxOfLeaf m t η τ, mem_biUnion.2 ⟨_, mem_powersetCard.2 ?_, boxOfLeaf_mem_boxesAt m t
+      hτ⟩,
+      mem_leaves_boxOfLeaf m t η τ⟩
+    exact ⟨paddedLevels_subset m t (P0LevelsWithin_subset _ τ),
+      card_paddedLevels ht hη (P0LevelsWithin_subset _ τ) (card_P0LevelsWithin_le hτ hord)⟩
+  · -- "Every leaf of a box of 𝓑_V agrees with the private leaf of w outside Q, so it contributes
+    rintro ⟨π, hπ, hτπ⟩
+    obtain ⟨V, hV, hπV⟩ := mem_biUnion.1 hπ
+    exact ⟨(contributes_iff_eq_privateLeaf η τ).2 fun ℓ hℓ =>
+        Cube.eq_of_mem_leaves hτπ (boxesAt_outside hπV hℓ),
+      le_order_of_mem_leaves ht (boxesAt_isBox hV hπV) hτπ⟩
+
+private lemma eq_paddedLevels_of_mem_leaves {m t : ℕ} (ht : t ≤ m) {η : OutStr L}
+    (hη : (innerSetO η).card = m) {τ : Leaf L} (hτ : Leaf.Contributes τ η)
+    (hord : (t : ℤ) ≤ order m τ) {V : Finset (Fin L)} (hV : V ∈ boxLevelSets m t η) {π : Cube L}
+    (hπ : π ∈ boxesAt η V) (hτπ : τ ∈ Cube.leaves π) :
+    V = paddedLevels m t (innerSetO η) (P0LevelsWithin (innerSetO η) τ) := by
+  obtain ⟨hVQ, hVc⟩ := mem_powersetCard.1 hV
+  obtain ⟨hVZ, hZV⟩ := (exists_mem_boxesAt_leaf_iff hVQ hτ).1 ⟨π, hπ, hτπ⟩
+  exact (paddedLevels_unique m t ht _ _ hη (P0LevelsWithin_subset _ τ) (card_P0LevelsWithin_le hτ
+    hord) V).1 ⟨hVQ, hVc, hVZ, hZV⟩
+
+/-- Each high-order contributing leaf lies in exactly one output box. -/
+theorem existsUnique_box_containing_leaf {L : ℕ} (m t : ℕ) (ht : t ≤ m) (η : OutStr L) (hη :
+  (innerSetO η).card = m)
+    (τ : Leaf L) (hτ : Leaf.Contributes τ η) (hord : (t : ℤ) ≤ order m τ) :
+    ∃! π : Cube L, π ∈ (boxLevelSets m t η).biUnion (boxesAt η) ∧ τ ∈ Cube.leaves π := by
+  obtain ⟨π, hπ, hτπ⟩ := (contributes_high_iff_mem_box_leaves m t ht η hη τ).1 ⟨hτ, hord⟩
+  refine ⟨π, ⟨hπ, hτπ⟩, ?_⟩
+  rintro π' ⟨hπ', hτπ'⟩
+  obtain ⟨V, hV, hπV⟩ := mem_biUnion.1 hπ
+  obtain ⟨V', hV', hπV'⟩ := mem_biUnion.1 hπ'
+  obtain rfl : V' = V := (eq_paddedLevels_of_mem_leaves ht hη hτ hord hV' hπV' hτπ').trans
+    (eq_paddedLevels_of_mem_leaves ht hη hτ hord hV hπV hτπ).symm
+  exact boxesAt_leaf_unique hπV' hτπ' hπV hτπ
+
+/-- A sum splits into low-order leaves and the disjoint output boxes. -/
+theorem sum_contributing_eq_low_add_boxes {G : Type*} [AddCommMonoid G] (m t : ℕ) (ht : t ≤ m)
+    (η : OutStr L) (hη : (innerSetO η).card = m) (g : Leaf L → G) :
+    ∑ τ : Leaf L with Leaf.Contributes τ η, g τ =
+      ∑ τ ∈ lowLeaves m t η, g τ + ∑ V ∈ boxLevelSets m t η, ∑ π ∈ boxesAt η V, ∑ τ ∈ Cube.leaves
+        π, g τ := by
+  have hdisjoint :
+      (((boxLevelSets m t η).biUnion (boxesAt η) : Finset (Cube L)) : Set (Cube L)).PairwiseDisjoint
+        Cube.leaves := by
+    intro π hπ π' hπ' hne
+    rw [Function.onFun, disjoint_left]
+    intro τ hτ hτ'
+    obtain ⟨hc, hord⟩ := (contributes_high_iff_mem_box_leaves m t ht η hη τ).2 ⟨π, hπ, hτ⟩
+    exact hne ((existsUnique_box_containing_leaf m t ht η hη τ hc hord).unique ⟨hπ, hτ⟩ ⟨hπ', hτ'⟩)
+  have hhigh : ((boxLevelSets m t η).biUnion (boxesAt η)).biUnion Cube.leaves =
+      univ.filter fun τ : Leaf L => Leaf.Contributes τ η ∧ ¬ order m τ < (t : ℤ) := by
+    ext τ
+    rw [mem_biUnion, mem_filter, not_lt, ← contributes_high_iff_mem_box_leaves m t ht η hη τ]
+    simp
+  rw [← sum_biUnion (boxesAt_pairwiseDisjoint η _), ← sum_biUnion hdisjoint, hhigh, lowLeaves,
+    ← filter_filter, ← filter_filter, sum_filter_add_sum_filter_not]
+
+/-- The signed bilinear product equals the complete query expression. -/
+theorem bilinearProduct_eq_boxQuery (m t : ℕ) (ht : t ≤ m) (a : LeftStr L → ℤ) (b : RightStr L → ℤ)
+    (η : OutStr L) (hη : (innerSetO η).card = m) : bilinearProduct a b η = boxQuery m t a b η :=
+  sum_contributing_eq_low_add_boxes m t ht η hη fun τ => encodeLeft τ a * encodeRight τ b
+
+/-- Low-order leaves and box leaves account for each contributing leaf once. -/
+theorem card_low_add_box_leaves (m t : ℕ) (ht : t ≤ m) (η : OutStr L)
+    (hη : (innerSetO η).card = m) :
+    (lowLeaves m t η).card + ∑ π ∈ (boxLevelSets m t η).biUnion (boxesAt η), (Cube.leaves π).card
+      = 10 ^ m := by
+  have hsplit := sum_contributing_eq_low_add_boxes m t ht η hη fun _ => 1
+  rw [← card_eq_sum_ones, card_filter_contributes η hη] at hsplit
+  rw [hsplit, sum_biUnion (boxesAt_pairwiseDisjoint η _)]
+  simp
+
+private lemma lowLeaves_eq_biUnion (m t : ℕ) (η : OutStr L) (hη : (innerSetO η).card = m) :
+    lowLeaves m t η = (range t).biUnion fun d =>
+      univ.filter fun τ : Leaf L => Leaf.Contributes τ η ∧ order m τ = d := by
+  ext τ
+  simp only [lowLeaves, mem_filter, mem_univ, true_and, mem_biUnion, mem_range]
+  constructor
+  · rintro ⟨hτ, hlt⟩
+    have hnonneg := order_nonneg hη hτ
+    exact ⟨(order m τ).toNat, by omega, hτ, (Int.toNat_of_nonneg hnonneg).symm⟩
+  · rintro ⟨d, hd, hτ, heq⟩
+    exact ⟨hτ, by omega⟩
+
+/-- The exact query counts are given by the existing alpha function. -/
+theorem box_query_counts {L : ℕ} (m t : ℕ) (ht : t ≤ m) (η : OutStr L)
+    (hη : (innerSetO η).card = m) :
+    (lowLeaves m t η).card = ∑ d ∈ range t, alpha m d ∧
+      ∑ V ∈ boxLevelSets m t η, (boxesAt η V).card = alpha m t ∧
+      ((boxLevelSets m t η).biUnion (boxesAt η)).card = alpha m t := by
+  have hsum : ∑ V ∈ boxLevelSets m t η, (boxesAt η V).card = alpha m t := by
+    rw [sum_congr rfl fun V hV => card_boxesAt m t ht η hη V hV, sum_const, boxLevelSets,
+      card_powersetCard, hη, Nat.choose_symm ht, smul_eq_mul, alpha]
+  refine ⟨?_, hsum, ?_⟩
+  · -- "α_d leaves of order d contribute to w"
+    rw [lowLeaves_eq_biUnion m t η hη, card_biUnion]
+    · exact sum_congr rfl fun d _ => card_contributing_of_order η hη d
+    · intro d _ d' _ hne
+      rw [Function.onFun, disjoint_left]
+      intro τ hd hd'
+      exact hne (by exact_mod_cast (mem_filter.1 hd).2.2.symm.trans (mem_filter.1 hd').2.2)
+  · rw [card_biUnion (boxesAt_pairwiseDisjoint η _), hsum]
+
+/-- An output box belongs to the global box set at its actual star count. -/
+theorem mem_boxesWithStars_of_mem_boxesAt {L : ℕ} (m t : ℕ) (η : OutStr L) (V : Finset (Fin L))
+  (hV : V ∈ boxLevelSets m t η)
+    (π : Cube L) (hπ : π ∈ boxesAt η V) : π ∈ boxesWithStars L m t (initialLevels (innerSetO η)
+      V).card :=
+  mem_filter.2 ⟨mem_filter.2 ⟨mem_univ _, boxesAt_isBox hV hπ⟩, by rw [boxesAt_starLevels hπ]⟩
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxValues.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxValues.lean
new file mode 100644
index 0000000000..518c379141
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxValues.lean
@@ -0,0 +1,177 @@
+/-
+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.Boxes
+import Mathlib.Algebra.BigOperators.Intervals
+
+/-!
+# Finite box counts and value recurrence
+
+The canonical-box bijection counts boxes by a completed leaf and a number of stars.
+`card_boxes_le` bounds their total by `(m + 1)` times the sum of the existing `beta`
+counts. It needs only `m ≤ L` and `t ≤ m`; the source's stronger `10 * m ≤ L` is unnecessary.
+
+`boxValue` recursively replaces the highest star by each of the ten existing terms.
+`boxValue_eq_val` proves that it computes the signed cube value when the supplied star
+count is exact. This recurrence may recompute subproblems: it is neither a memoized table
+nor a native program and carries no preprocessing-time or space theorem.
+
+Adapted from [AlmanWilliams2026, Lemma 29] and
+[Lemma29.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Lemma29.lean) at
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+The encodings, terms, leaf order and `beta` counts are the existing local notions.
+-/
+
+public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- All cubes satisfying the box conditions at the selected parameters. -/
+@[expose] def boxes (L m t : ℕ) : Finset (Cube L) := univ.filter (IsBox m t)
+
+/-- Boxes whose star count is exactly `e`. -/
+@[expose] def boxesWithStars (L m t e : ℕ) : Finset (Cube L) :=
+  (boxes L m t).filter fun π => π.starLevels.card = e
+
+/-- Finite recursive value evaluation, indexed by the exact number of stars. -/
+@[expose] def boxValue {L : ℕ} (encA encB : Leaf L → ℤ) : ℕ → Cube L → ℤ
+  | 0, π => encA π.starsToP0 * encB π.starsToP0
+  | e + 1, π =>
+    if h : π.starLevels.Nonempty then
+      ∑ lam : Term, boxValue encA encB e (π.replace (π.starLevels.max' h) lam)
+    else 0
+
+/-- Membership is exactly the two box conditions. -/
+@[simp] theorem mem_boxes {L m t : ℕ} {π : Cube L} : π ∈ boxes L m t ↔ IsBox m t π := by
+  simp [boxes]
+
+/-- Membership combines the box conditions with an exact star count. -/
+@[simp] theorem mem_boxesWithStars {L m t e : ℕ} {π : Cube L} :
+    π ∈ boxesWithStars L m t e ↔ IsBox m t π ∧ (Cube.starLevels π).card = e := by
+  simp [boxesWithStars, boxes]
+
+
+
+private lemma card_leaves_P0 {L m f : ℕ} (hmL : m ≤ L) (hf : f ≤ m) :
+    (univ.filter fun τ : Leaf L => (P0Levels τ).card = f).card = beta L m (m - f) := by
+  rw [← card_filter_order_eq hmL (m - f) (Nat.sub_le _ _)]
+  congr 1
+  ext τ
+  rw [mem_filter, mem_filter, order]
+  simp only [mem_univ, true_and]
+  omega
+
+/-- Boxes with a fixed combined star/P0 count correspond to completed leaves and star counts. -/
+theorem card_boxes_with_P0_count (L m t f : ℕ) (hmL : m ≤ L) (hf : f ≤ m - t) :
+    ((boxes L m t).filter fun π => (Cube.starLevels π).card + (Cube.P0Levels π).card = f).card
+      = (f + 1) * beta L m (m - f) := by
+  have hpairs : ((univ.filter fun τ : Leaf L => (P0Levels τ).card = f) ×ˢ range (f + 1)).card
+      = (f + 1) * beta L m (m - f) := by
+    rw [card_product, card_leaves_P0 hmL (by omega), card_range, mul_comm]
+  have hpair : ∀ p ∈ (univ.filter fun τ : Leaf L => (P0Levels τ).card = f) ×ˢ range (f + 1),
+      (P0Levels p.1).card = f ∧ p.2 < f + 1 := fun p hp =>
+    ⟨(mem_filter.1 (mem_product.1 hp).1).2, mem_range.1 (mem_product.1 hp).2⟩
+  rw [← hpairs]
+  refine card_bij' (fun π _ => (Cube.starsToP0 π, (Cube.starLevels π).card))
+    (fun p _ => starLowest p.2 p.1) (fun π hπ => ?_) (fun p hp => ?_) (fun π hπ => ?_)
+    fun p hp => ?_
+  · -- the pair of such a box is such a pair
+    have hf := (mem_filter.1 hπ).2
+    simp only [mem_product, mem_filter, mem_univ, true_and, mem_range,
+      card_P0Levels_starsToP0]
+    omega
+  · -- the cube of such a pair is such a box: its leaf is the leaf of the pair
+    obtain ⟨hτ, -⟩ := hpair p hp
+    rw [mem_filter, mem_boxes, ← card_P0Levels_starsToP0, starsToP0_starLowest]
+    exact ⟨isBox_starLowest m t p.2 p.1 (by omega), hτ⟩
+  · -- from a box to its pair and back
+    exact (eq_starLowest_starsToP0 π (mem_boxes.1 (mem_filter.1 hπ).1).2).symm
+  · -- from a pair `(τ, e)` to its cube and back: the cube has `min e f = e` stars
+    obtain ⟨hτ, he⟩ := hpair p hp
+    rw [starsToP0_starLowest, starLevels_starLowest, card_lowest, hτ,
+      min_eq_left (by omega)]
+
+/-- The total count is bounded by completed-leaf counts and at most `m + 1` star counts. -/
+theorem card_boxes_le (L m t : ℕ) (hmL : m ≤ L) (ht : t ≤ m) :
+    (boxes L m t).card ≤ (m + 1) * ∑ d ∈ Finset.Icc t m, beta L m d := by
+  have hsort : (boxes L m t).card = ∑ f ∈ range (m - t + 1),
+      ((boxes L m t).filter
+        fun π => (Cube.starLevels π).card + (Cube.P0Levels π).card = f).card := by
+    refine card_eq_sum_card_fiberwise fun π hπ => ?_
+    have hi := (mem_boxes.1 (mem_coe.1 hπ)).1
+    simp only [coe_range, Set.mem_Iio]
+    omega
+  have hreflect : ∑ f ∈ range (m - t + 1), beta L m (m - f) = ∑ d ∈ Finset.Icc t m, beta L m d := by
+    rw [range_eq_Ico, sum_Ico_reflect _ _ (by omega)]
+    congr 1
+    ext d
+    simp only [mem_Ico, mem_Icc]
+    omega
+  rw [hsort, ← hreflect, mul_sum]
+  refine sum_le_sum fun f hf => ?_
+  have hfm : f < m - t + 1 := mem_range.1 hf
+  rw [card_boxes_with_P0_count L m t f (by omega) (by omega)]
+  exact Nat.mul_le_mul_right _ (by omega)
+
+
+
+/-- Boxes without stars are exactly the eligible fully fixed leaves. -/
+theorem boxesWithStars_zero_iff {L : ℕ} (m t : ℕ) (π : Cube L) :
+    π ∈ boxesWithStars L m t 0 ↔ ∃ τ : Leaf L, (P0Levels τ).card ≤ m - t ∧ π = Cube.ofLeaf τ := by
+  rw [mem_boxesWithStars]
+  constructor
+  · rintro ⟨hbox, hstar⟩
+    refine ⟨Cube.starsToP0 π, ?_,
+      Cube.eq_ofLeaf_of_starLevels_eq_empty π (card_eq_zero.1 hstar)⟩
+    rw [card_P0Levels_starsToP0]
+    exact hbox.1
+  · rintro ⟨τ, hτ, rfl⟩
+    rw [IsBox, Cube.starLevels_ofLeaf, Cube.P0Levels_ofLeaf]
+    simpa using hτ
+
+/-- Replacing the highest star gives a box with one fewer star. -/
+theorem replace_highest_mem_boxesWithStars {L m t e : ℕ} {π : Cube L}
+    (hπ : π ∈ boxesWithStars L m t (e + 1))
+    (hne : (Cube.starLevels π).Nonempty) (lam : Term) :
+    Cube.replace π ((Cube.starLevels π).max' hne) lam ∈ boxesWithStars L m t e := by
+  obtain ⟨⟨hcount, hbelow⟩, hcard⟩ := mem_boxesWithStars.1 hπ
+  have hstar :
+      (Cube.starLevels (Cube.replace π ((Cube.starLevels π).max' hne) lam)).card = e := by
+    rw [Cube.starLevels_replace, card_erase_of_mem (max'_mem _ hne), hcard,
+      Nat.add_sub_cancel]
+  have hP0 := Cube.P0Levels_replace_subset π ((Cube.starLevels π).max' hne) lam
+  refine mem_boxesWithStars.2 ⟨⟨?_, fun k hk k' hk' => ?_⟩, hstar⟩
+  · -- One star fewer (`hstar`, `hcard`) and at most one symbol `P₀` more (`hmore`), so (i) stays.
+    have hmore := (card_le_card hP0).trans (card_insert_le _ _)
+    omega
+  · -- The new symbol is above the remaining stars, and so are the old symbols `P₀`, by (ii).
+    rw [Cube.starLevels_replace, mem_erase] at hk
+    rcases mem_insert.1 (hP0 hk') with hnew | hold
+    · exact hnew ▸ lt_of_le_of_ne (le_max' _ k hk.2) hk.1
+    · exact hbelow k hk.2 k' hold
+
+/-- The finite recurrence agrees with the signed encoding-product sum of a box. -/
+theorem boxValue_eq_val (L m t e : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (π : Cube L)
+    (hπ : π ∈ boxesWithStars L m t e) :
+    boxValue (encodingL a) (encodingR b) e π = Cube.val a b π := by
+  induction e generalizing π with
+  | zero =>
+    obtain ⟨τ, -, rfl⟩ := (boxesWithStars_zero_iff m t π).1 hπ
+    rw [Cube.val_ofLeaf]
+    rfl
+  | succ e ih =>
+    have hne : (Cube.starLevels π).Nonempty :=
+      card_pos.1 ((mem_boxesWithStars.1 hπ).2 ▸ Nat.succ_pos e)
+    rw [boxValue, dite_eq_left hne,
+      Cube.val_eq_sum_replace a b π _ (Cube.mem_starLevels.1 (max'_mem _ hne))]
+    exact sum_congr rfl fun lam _ => ih _ (replace_highest_mem_boxesWithStars hπ hne lam)
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Boxes.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Boxes.lean
new file mode 100644
index 0000000000..108e581dbb
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Boxes.lean
@@ -0,0 +1,104 @@
+/-
+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.Cubes
+public import Complexity.Foundations.Data.Finset.Lowest
+
+/-!
+# Canonical boxes of tensor leaves
+
+A box has at most `m - t` stars or fixed P0 terms, with every star preceding every
+fixed P0 term. Thus its leaves all have order at least `t`. Every box is obtained
+uniquely from its P0 completion by turning an initial segment of its P0 coordinates
+into stars; `Finset.lowest` supplies that initial segment without a separate rank API.
+
+This adapts [AlmanWilliams2026, Section 4.2] and the primary formal source
+[Boxes.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Boxes.lean) at `anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+The definitions have the source's natural truncated subtraction: claims about order
+explicitly require `t ≤ m`. These are finite statements, with no stored table or time bound.
+-/
+
+public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+variable {L : ℕ}
+
+/-- A cube with a bounded number of stars/P0 symbols, stars preceding all fixed P0 symbols. -/
+@[expose] def IsBox (m t : ℕ) (π : Cube L) : Prop :=
+  π.starLevels.card + π.P0Levels.card ≤ m - t ∧
+    ∀ ℓ ∈ π.starLevels, ∀ ℓ' ∈ π.P0Levels, ℓ < ℓ'
+
+instance IsBox.instDecidable (m t : ℕ) (π : Cube L) : Decidable (IsBox m t π) :=
+  inferInstanceAs (Decidable (π.starLevels.card + π.P0Levels.card ≤ m - t ∧
+    ∀ ℓ ∈ π.starLevels, ∀ ℓ' ∈ π.P0Levels, ℓ < ℓ'))
+
+/-- A lower bound on order is an upper bound on the number of P0 terms. -/
+theorem le_order_iff {m t : ℕ} (ht : t ≤ m) (τ : Leaf L) :
+    (t : ℤ) ≤ order m τ ↔ (P0Levels τ).card ≤ m - t := by
+  unfold order
+  omega
+
+/-- A matching leaf can use P0 only at a star or a coordinate fixed to P0. -/
+theorem P0Levels_subset_of_mem_leaves {π : Cube L} {τ : Leaf L} (hτ : τ ∈ Cube.leaves π) :
+    P0Levels τ ⊆ Cube.P0Levels π ∪ Cube.starLevels π := by
+  intro ℓ hℓ
+  rw [mem_P0Levels] at hℓ
+  rw [mem_union, Cube.mem_P0Levels, Cube.mem_starLevels, ← hℓ]
+  exact (Cube.mem_leaves.1 hτ ℓ).symm
+
+/-- Every leaf of a box has the required minimum order. -/
+theorem le_order_of_mem_leaves {m t : ℕ} (ht : t ≤ m) {π : Cube L} (hπ : IsBox m t π)
+    {τ : Leaf L} (hτ : τ ∈ Cube.leaves π) : (t : ℤ) ≤ order m τ := by
+  rw [le_order_iff ht]
+  calc (P0Levels τ).card ≤ (Cube.P0Levels π ∪ Cube.starLevels π).card :=
+        card_le_card (P0Levels_subset_of_mem_leaves hτ)
+    _ ≤ (Cube.P0Levels π).card + (Cube.starLevels π).card := card_union_le _ _
+    _ ≤ m - t := (add_comm _ _).trans_le hπ.1
+
+/-- The canonical cube made by starring the lowest P0 coordinates. -/
+@[expose] def starLowest (e : ℕ) (τ : Leaf L) : Cube L := Cube.starAt (lowest e (P0Levels τ)) τ
+
+/-- The selected initial segment is exactly the star set. -/
+theorem starLevels_starLowest (e : ℕ) (τ : Leaf L) :
+    Cube.starLevels (starLowest e τ) = lowest e (P0Levels τ) :=
+  Cube.starLevels_starAt _ τ
+
+/-- Unselected P0 coordinates remain fixed. -/
+theorem P0Levels_starLowest (e : ℕ) (τ : Leaf L) :
+    Cube.P0Levels (starLowest e τ) = P0Levels τ \ lowest e (P0Levels τ) :=
+  Cube.P0Levels_starAt _ τ
+
+/-- Completion recovers the original leaf, including when selection saturates. -/
+theorem starsToP0_starLowest (e : ℕ) (τ : Leaf L) : Cube.starsToP0 (starLowest e τ) = τ :=
+  Cube.starsToP0_starAt (lowest_subset _ _)
+
+/-- The star-order condition characterizes the canonical form of a cube. -/
+theorem eq_starLowest_starsToP0 (π : Cube L)
+    (h : ∀ ℓ ∈ Cube.starLevels π, ∀ ℓ' ∈ Cube.P0Levels π, ℓ < ℓ') :
+    π = starLowest (Cube.starLevels π).card (Cube.starsToP0 π) := by
+  have hlow : Cube.starLevels π =
+      lowest (Cube.starLevels π).card (P0Levels (Cube.starsToP0 π)) := by
+    refine eq_lowest_of_lt ?_ fun ℓ hℓ ℓ' hℓ' => h ℓ hℓ ℓ' ?_
+    · rw [P0Levels_starsToP0]
+      exact subset_union_left
+    · rw [P0Levels_starsToP0, mem_sdiff, mem_union] at hℓ'
+      tauto
+  rw [starLowest, ← hlow, Cube.starAt_starLevels_starsToP0]
+
+/-- Starring any initial segment preserves the box count and order conditions. -/
+theorem isBox_starLowest (m t e : ℕ) (τ : Leaf L) (hτ : (P0Levels τ).card ≤ m - t) :
+    IsBox m t (starLowest e τ) := by
+  rw [IsBox, ← card_P0Levels_starsToP0, starsToP0_starLowest, starLevels_starLowest,
+    P0Levels_starLowest]
+  exact ⟨hτ, fun ℓ hℓ ℓ' hℓ' => lowest_lt hℓ hℓ'⟩
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxesFromLeaves.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxesFromLeaves.lean
new file mode 100644
index 0000000000..d54568d56e
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/BoxesFromLeaves.lean
@@ -0,0 +1,97 @@
+/-
+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.BoxPartition
+
+/-!
+# Output boxes indexed by leaves of exactly the threshold order
+
+Completing the stars of an output box gives its unique contributing leaf of order `t`.
+Conversely `starBelow` constructs this box from such a leaf. The high-order partition
+remains the one in `BoxPartition`; this is an additional finite indexing bijection.
+
+Adapted from [AlmanWilliams2026, Section 4.2] and the primary formal source
+[BoxesFromLeaves.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/BoxesFromLeaves.lean) at
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+No native enumeration or lookup-cost statement is supplied by this bijection.
+-/
+
+public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+variable {L m t : ℕ} {η : OutStr L} {τ : Leaf L}
+
+/-- An output box has exactly the prescribed combined star and P0 count. -/
+theorem card_starLevels_add_card_P0Levels {π : Cube L} (hπ : π ∈ (boxLevelSets m t η).biUnion
+  (boxesAt η)) :
+    (Cube.starLevels π).card + (Cube.P0Levels π).card = m - t := by
+  obtain ⟨V, hV, hπV⟩ := mem_biUnion.1 hπ
+  rw [← card_union_of_disjoint (Cube.disjoint_starLevels_P0Levels π),
+    boxesAt_starLevels_union_P0Levels hπV, (mem_powersetCard.1 hV).2]
+
+/-- Star the P0 coordinates preceding every non-P0 inner coordinate. -/
+@[expose] def starBelow (η : OutStr L) (τ : Leaf L) : Cube L :=
+  Cube.starAt (initialLevels (innerSetO η) (P0LevelsWithin (innerSetO η) τ)) τ
+
+private lemma card_P0LevelsWithin_eq (hτ : Leaf.Contributes τ η) (hord : order m τ = t) :
+    (P0LevelsWithin (innerSetO η) τ).card = m - t := by
+  have := order_eq_sub_card_P0LevelsWithin m η τ hτ
+  omega
+
+private lemma paddedLevels_eq_self (Q Z : Finset (Fin L)) (hZ : Z.card = m - t) : paddedLevels m t
+  Q Z = Z := by
+  simp [paddedLevels, lowest, hZ]
+
+/-- At exact threshold order, the padded construction is the initial-star construction. -/
+theorem boxOfLeaf_eq_starBelow (hτ : Leaf.Contributes τ η) (hord : order m τ = t) :
+    boxOfLeaf m t η τ = starBelow η τ := by
+  rw [boxOfLeaf, starBelow, paddedLevels_eq_self _ _ (card_P0LevelsWithin_eq hτ hord)]
+
+/-- Initial starring retains the original leaf. -/
+theorem mem_leaves_starBelow (η : OutStr L) (τ : Leaf L) : τ ∈ Cube.leaves (starBelow η τ) :=
+  Cube.mem_leaves_starAt _ τ
+
+/-- A contributing leaf of exact threshold order gives an eligible output box. -/
+theorem starBelow_mem (hτ : Leaf.Contributes τ η) (hord : order m τ = t) :
+    starBelow η τ ∈ (boxLevelSets m t η).biUnion (boxesAt η) := by
+  have hmem := boxOfLeaf_mem_boxesAt m t hτ
+  rw [boxOfLeaf_eq_starBelow hτ hord, paddedLevels_eq_self _ _ (card_P0LevelsWithin_eq hτ hord)]
+    at hmem
+  exact mem_biUnion.2 ⟨_, mem_powersetCard.2 ⟨filter_subset _ _, card_P0LevelsWithin_eq hτ hord⟩,
+    hmem⟩
+
+/-- Completing the initial stars recovers the original leaf. -/
+theorem starsToP0_starBelow (η : OutStr L) (τ : Leaf L) : Cube.starsToP0 (starBelow η τ) = τ :=
+  Cube.starsToP0_starAt fun _ hℓ => mem_P0Levels.2 (mem_filter.1 (initialLevels_subset _ _ hℓ)).2
+
+/-- Completing an output box gives a contributing leaf of exact threshold order. -/
+theorem starsToP0_of_mem (ht : t ≤ m) (hη : (innerSetO η).card = m) {π : Cube L}
+    (hπ : π ∈ (boxLevelSets m t η).biUnion (boxesAt η)) :
+    Leaf.Contributes (Cube.starsToP0 π) η ∧ order m (Cube.starsToP0 π) = t := by
+  refine ⟨((contributes_high_iff_mem_box_leaves m t ht η hη _).2 ⟨π, hπ, Cube.starsToP0_mem_leaves
+    π⟩).1, ?_⟩
+  rw [order, card_P0Levels_starsToP0, card_starLevels_add_card_P0Levels hπ]
+  omega
+
+/-- Each output box has exactly one exact-threshold leaf giving its initial-star form. -/
+theorem existsUnique_starBelow_eq (ht : t ≤ m) (hη : (innerSetO η).card = m) {π : Cube L}
+    (hπ : π ∈ (boxLevelSets m t η).biUnion (boxesAt η)) :
+    ∃! τ : Leaf L, (Leaf.Contributes τ η ∧ order m τ = t) ∧ starBelow η τ = π := by
+  obtain ⟨hτ, hord⟩ := starsToP0_of_mem ht hη hπ
+  refine ⟨Cube.starsToP0 π, ⟨⟨hτ, hord⟩, ?_⟩, ?_⟩
+  · -- both are boxes of `η` with this leaf, and by Lemma 28 there is only one
+    exact (existsUnique_box_containing_leaf m t ht η hη _ hτ hord.ge).unique
+      ⟨starBelow_mem hτ hord, mem_leaves_starBelow η _⟩ ⟨hπ, Cube.starsToP0_mem_leaves π⟩
+  · rintro τ ⟨-, rfl⟩
+    exact (starsToP0_starBelow η τ).symm
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Cubes.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Cubes.lean
new file mode 100644
index 0000000000..a7958e578e
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Cubes.lean
@@ -0,0 +1,273 @@
+/-
+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.Orders
+
+/-!
+# Cubes of tensor leaves for the improved thin-product decomposition
+
+A cube fixes a term at some levels and permits every term at its star levels. It denotes a
+finite set of the existing tensor leaves. Its integer value sums the actual products of the
+existing two encodings. This is finite algebra; no cube is a native lookup or time certificate.
+
+## Main definitions
+
+* `CubeSymbol`, `Cube`: term-or-star symbols and their level-indexed tuples.
+* `Cube.HasLeaf`, `Cube.leaves`, `Cube.starLevels`, `Cube.P0Levels`: finite incidence data.
+* `Cube.val`: signed sum of existing encoded products.
+* `Cube.ofLeaf`, `Cube.replace`, `Cube.starAt`, `Cube.starsToP0`: basic cube operations.
+
+## Main results
+
+* `Cube.card_leaves`: each star supplies ten independent term choices.
+* `Cube.leaves_ofLeaf`: a cube fixing every level has exactly its original leaf.
+* `Cube.mem_leaves_replace`: replacing a star selects the leaves using that term.
+* `Cube.starLevels_starAt`, `Cube.P0Levels_starAt`: explicit readback of inserted stars.
+
+## References
+
+Adapted from [AlmanWilliams2026, Section 4.2] and the primary formal source at
+[anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp):
+`PaperStatements.lean` lines 1844–1901 and 1952–1954, and [Boxes.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Boxes.lean).
+The local value expression uses `encodeLeft` and `encodeRight`, the existing versions of
+that source's two encoding forms. No source machine, native execution or cost law is imported.
+-/
+
+public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+-- Expose the derived finite enumeration for checked box counts and signed-value clients.
+@[expose] public section
+
+/-- A fixed multiplication label or an unrestricted level. -/
+inductive CubeSymbol : Type
+  | term (lam : Term)
+  | star
+  deriving DecidableEq, Fintype
+
+end
+
+/-- Level-indexed term-or-star symbols over the existing tensor alphabets. -/
+abbrev Cube (L : ℕ) : Type := Fin L → CubeSymbol
+
+/-- A leaf agrees with every fixed term; stars impose no condition. -/
+@[expose] def Cube.HasLeaf {L : ℕ} (π : Cube L) (τ : Leaf L) : Prop :=
+  ∀ ℓ, π ℓ = .star ∨ π ℓ = .term (τ ℓ)
+
+/-- Finite leaf membership is executable in the specification. -/
+instance Cube.instDecidableHasLeaf {L : ℕ} (π : Cube L) (τ : Leaf L) :
+    Decidable (π.HasLeaf τ) :=
+  inferInstanceAs (Decidable (∀ ℓ, π ℓ = .star ∨ π ℓ = .term (τ ℓ)))
+
+/-- All leaves matching the fixed terms of the cube. -/
+@[expose] def Cube.leaves {L : ℕ} (π : Cube L) : Finset (Leaf L) :=
+  univ.filter π.HasLeaf
+
+/-- Levels at which every term is allowed. -/
+@[expose] def Cube.starLevels {L : ℕ} (π : Cube L) : Finset (Fin L) :=
+  univ.filter fun ℓ => π ℓ = .star
+
+/-- Levels fixed to the distinguished multiplication term. -/
+@[expose] def Cube.P0Levels {L : ℕ} (π : Cube L) : Finset (Fin L) :=
+  univ.filter fun ℓ => π ℓ = .term .P0
+
+/-- Sum of the existing signed encoding products over the leaves of the cube. -/
+@[expose] def Cube.val {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (π : Cube L) : ℤ :=
+  ∑ τ ∈ π.leaves, encodeLeft τ a * encodeRight τ b
+
+/-- The cube fixing each level to the given leaf. -/
+@[expose] def Cube.ofLeaf {L : ℕ} (τ : Leaf L) : Cube L := fun ℓ => .term (τ ℓ)
+
+/-- Fix one level to a multiplication label. -/
+@[expose] def Cube.replace {L : ℕ} (π : Cube L) (ℓ : Fin L) (lam : Term) : Cube L :=
+  Function.update π ℓ (.term lam)
+
+/-- Replace the specified levels of a leaf with unrestricted stars. -/
+@[expose] def Cube.starAt {L : ℕ} (F : Finset (Fin L)) (τ : Leaf L) : Cube L :=
+  fun ℓ => if ℓ ∈ F then .star else .term (τ ℓ)
+
+/-- Complete every star with the distinguished term, retaining all fixed terms. -/
+@[expose] def Cube.starsToP0 {L : ℕ} (π : Cube L) : Leaf L :=
+  fun ℓ => match π ℓ with
+    | .term lam => lam
+    | .star => .P0
+
+variable {L : ℕ}
+
+@[simp] theorem Cube.mem_leaves {π : Cube L} {τ : Leaf L} :
+    τ ∈ π.leaves ↔ ∀ ℓ, π ℓ = .star ∨ π ℓ = .term (τ ℓ) := by
+  simp only [Cube.leaves, mem_filter, mem_univ, true_and, Cube.HasLeaf]
+
+/-- A fixed symbol determines the corresponding coordinate of every matching leaf. -/
+theorem Cube.eq_of_mem_leaves {π : Cube L} {τ : Leaf L} (hτ : τ ∈ π.leaves)
+    {ℓ : Fin L} {lam : Term} (h : π ℓ = .term lam) : τ ℓ = lam := by
+  simpa [h, eq_comm] using Cube.mem_leaves.mp hτ ℓ
+
+@[simp] theorem Cube.mem_starLevels {π : Cube L} {ℓ : Fin L} :
+    ℓ ∈ π.starLevels ↔ π ℓ = .star := by
+  simp [Cube.starLevels]
+
+@[simp] theorem Cube.mem_P0Levels {π : Cube L} {ℓ : Fin L} :
+    ℓ ∈ π.P0Levels ↔ π ℓ = .term .P0 := by
+  simp [Cube.P0Levels]
+
+/-- A level cannot be both a star and fixed to the distinguished term. -/
+theorem Cube.disjoint_starLevels_P0Levels (π : Cube L) :
+    Disjoint π.starLevels π.P0Levels := by
+  rw [disjoint_left]
+  intro ℓ hs hp
+  rw [Cube.mem_starLevels] at hs
+  rw [Cube.mem_P0Levels, hs] at hp
+  cases hp
+
+private def symbolTerms : CubeSymbol → Finset Term
+  | .term lam => {lam}
+  | .star => univ
+
+private theorem leaves_eq_piFinset (π : Cube L) :
+    π.leaves = Fintype.piFinset fun ℓ => symbolTerms (π ℓ) := by
+  ext τ
+  rw [Cube.mem_leaves, Fintype.mem_piFinset]
+  refine forall_congr' fun ℓ => ?_
+  cases h : π ℓ <;> simp [symbolTerms, eq_comm]
+
+/-- Each star independently contributes ten possible labels, including at zero levels. -/
+theorem Cube.card_leaves (π : Cube L) : π.leaves.card = 10 ^ π.starLevels.card := by
+  have hc : ∀ ℓ, (symbolTerms (π ℓ)).card = if ℓ ∈ π.starLevels then 10 else 1 := by
+    intro ℓ
+    cases h : π ℓ <;> simp [symbolTerms, h, card_term]
+  rw [leaves_eq_piFinset, Fintype.card_piFinset]
+  simp only [hc]
+  rw [prod_ite_mem_const, one_pow, mul_one]
+
+/-- Fixing every coordinate gives a singleton leaf set. -/
+@[simp] theorem Cube.leaves_ofLeaf (τ : Leaf L) : (Cube.ofLeaf τ).leaves = {τ} := by
+  ext σ
+  simp [Cube.ofLeaf, funext_iff, eq_comm]
+
+@[simp] theorem Cube.starLevels_ofLeaf (τ : Leaf L) : (Cube.ofLeaf τ).starLevels = ∅ := by
+  ext ℓ
+  simp [Cube.ofLeaf]
+
+@[simp] theorem Cube.P0Levels_ofLeaf (τ : Leaf L) :
+    (Cube.ofLeaf τ).P0Levels =
+    Cslib.Algorithms.MatrixMultiplication.Schonhage.P0Levels τ := by
+  ext ℓ
+  simp [Cube.ofLeaf]
+
+/-- Replacing a star retains precisely the leaves that use the chosen term there. -/
+theorem Cube.mem_leaves_replace {π : Cube L} {ℓ : Fin L} (hℓ : π ℓ = .star)
+    (lam : Term) (τ : Leaf L) :
+    τ ∈ (π.replace ℓ lam).leaves ↔ τ ∈ π.leaves ∧ τ ℓ = lam := by
+  rw [Cube.mem_leaves, Cube.mem_leaves, Cube.replace,
+    Function.forall_update_iff π fun k s => s = .star ∨ s = .term (τ k)]
+  constructor
+  · rintro ⟨hlam, h⟩
+    refine ⟨fun k => ?_, by simpa [eq_comm] using hlam⟩
+    by_cases hk : k = ℓ
+    · exact Or.inl (hk ▸ hℓ)
+    · exact h k hk
+  · rintro ⟨h, rfl⟩
+    exact ⟨Or.inr rfl, fun k _ => h k⟩
+
+@[simp] theorem Cube.starLevels_starAt (F : Finset (Fin L)) (τ : Leaf L) :
+    (Cube.starAt F τ).starLevels = F := by
+  ext ℓ
+  by_cases h : ℓ ∈ F <;> simp [Cube.starAt, h]
+
+@[simp] theorem Cube.P0Levels_starAt (F : Finset (Fin L)) (τ : Leaf L) :
+    (Cube.starAt F τ).P0Levels =
+    Cslib.Algorithms.MatrixMultiplication.Schonhage.P0Levels τ \ F := by
+  ext ℓ
+  by_cases h : ℓ ∈ F <;> simp [Cube.starAt, h]
+
+/-- Inserting stars never removes the original leaf from the represented set. -/
+theorem Cube.mem_leaves_starAt (F : Finset (Fin L)) (τ : Leaf L) :
+    τ ∈ (Cube.starAt F τ).leaves := by
+  rw [Cube.mem_leaves]
+  intro ℓ
+  by_cases h : ℓ ∈ F <;> simp [Cube.starAt, h]
+
+/-- Completing inserted stars with P0 recovers leaves that originally use P0 there. -/
+theorem Cube.starsToP0_starAt {F : Finset (Fin L)} {τ : Leaf L}
+    (h : F ⊆ Cslib.Algorithms.MatrixMultiplication.Schonhage.P0Levels τ) :
+    (Cube.starAt F τ).starsToP0 = τ := by
+  funext ℓ
+  unfold Cube.starsToP0 Cube.starAt
+  split_ifs with hℓ
+  · exact (Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_P0Levels.mp (h hℓ)).symm
+  · rfl
+
+/-- Fixing a coordinate removes it from the remaining stars. -/
+theorem Cube.starLevels_replace (π : Cube L) (ℓ : Fin L) (lam : Term) :
+    (π.replace ℓ lam).starLevels = π.starLevels.erase ℓ := by
+  ext k
+  by_cases hk : k = ℓ <;> simp [Cube.replace, hk]
+
+/-- Fixing a coordinate can introduce P0 only at that coordinate. -/
+theorem Cube.P0Levels_replace_subset (π : Cube L) (ℓ : Fin L) (lam : Term) :
+    (π.replace ℓ lam).P0Levels ⊆ insert ℓ π.P0Levels := by
+  intro k hk
+  by_cases hkl : k = ℓ
+  · exact mem_insert.2 (Or.inl hkl)
+  · simpa [Cube.replace, hkl] using hk
+
+/-- Completing stars always gives one of the represented leaves. -/
+theorem Cube.starsToP0_mem_leaves (π : Cube L) : π.starsToP0 ∈ π.leaves := by
+  rw [Cube.mem_leaves]
+  intro ℓ
+  unfold Cube.starsToP0
+  cases π ℓ <;> simp
+
+/-- Completion followed by restoring the original stars recovers the cube. -/
+theorem Cube.starAt_starLevels_starsToP0 (π : Cube L) :
+    Cube.starAt π.starLevels π.starsToP0 = π := by
+  funext ℓ
+  unfold Cube.starAt Cube.starsToP0
+  cases h : π ℓ <;> simp [h]
+
+/-- A cube with no stars fixes the leaf given by its completion. -/
+theorem Cube.eq_ofLeaf_of_starLevels_eq_empty (π : Cube L) (hπ : π.starLevels = ∅) :
+    π = Cube.ofLeaf π.starsToP0 := by
+  conv_lhs => rw [← Cube.starAt_starLevels_starsToP0 π, hπ]
+  funext ℓ
+  simp [Cube.starAt, Cube.ofLeaf]
+
+/-- Completion chooses P0 precisely at the stars and the coordinates already fixed to P0. -/
+theorem P0Levels_starsToP0 (π : Cube L) :
+    P0Levels π.starsToP0 = π.starLevels ∪ π.P0Levels := by
+  ext ℓ
+  rw [mem_P0Levels, mem_union, Cube.mem_starLevels, Cube.mem_P0Levels]
+  unfold Cube.starsToP0
+  cases h : π ℓ <;> simp
+
+/-- Completion turns the disjoint star and P0 sets into one P0 set. -/
+theorem card_P0Levels_starsToP0 (π : Cube L) :
+    (P0Levels π.starsToP0).card = π.starLevels.card + π.P0Levels.card := by
+  rw [P0Levels_starsToP0, card_union_of_disjoint (Cube.disjoint_starLevels_P0Levels π)]
+
+/-- A fully fixed cube has the product of its two original encoded values. -/
+@[simp] theorem Cube.val_ofLeaf (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (τ : Leaf L) :
+    Cube.val a b (Cube.ofLeaf τ) = encodeLeft τ a * encodeRight τ b := by
+  rw [Cube.val, Cube.leaves_ofLeaf, sum_singleton]
+
+/-- Partitioning a star by its term partitions the signed value, including cancellation. -/
+theorem Cube.val_eq_sum_replace (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (π : Cube L)
+    (ℓ : Fin L) (hℓ : π ℓ = .star) :
+    Cube.val a b π = ∑ lam : Term, Cube.val a b (π.replace ℓ lam) := by
+  unfold Cube.val
+  rw [← sum_fiberwise π.leaves (fun τ => τ ℓ)]
+  refine sum_congr rfl fun lam _ => sum_congr ?_ fun _ _ => rfl
+  ext τ
+  rw [mem_filter, Cube.mem_leaves_replace hℓ]
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Foundations/Data/Finset/Lowest.lean b/Complexity/Foundations/Data/Finset/Lowest.lean
new file mode 100644
index 0000000000..6398912308
--- /dev/null
+++ b/Complexity/Foundations/Data/Finset/Lowest.lean
@@ -0,0 +1,96 @@
+/-
+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.Init
+public import Mathlib.Data.Finset.Card
+
+/-!
+# Initial segments of finite linearly ordered sets
+
+`Finset.lowest k s` retains the elements with fewer than `k` predecessors in `s`.
+Its members precede every omitted member, and its cardinality is `min k s.card`.
+This finite rank specification avoids choosing an enumeration in the clients.
+
+The proofs generalize the ordered-level argument in
+[AlmanWilliams2026, Section 4.2], primary formal source
+[Boxes.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec4/Boxes.lean) at `anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+The concrete consumer is the canonical tensor-box construction. No execution bound is asserted.
+-/
+
+public section
+
+namespace Finset
+
+variable {α : Type*} [LinearOrder α]
+
+/-- The elements having fewer than `k` predecessors in the finite set. -/
+@[expose] def lowest (k : ℕ) (s : Finset α) : Finset α :=
+  s.filter fun x => (s.filter fun y => y < x).card < k
+
+/-- The selected elements belong to the original set. -/
+theorem lowest_subset (k : ℕ) (S : Finset α) : lowest k S ⊆ S :=
+  filter_subset _ _
+
+/-- Membership is determined by the number of strictly smaller elements in the set. -/
+@[simp] theorem mem_lowest {k : ℕ} {S : Finset α} {ℓ : α} :
+    ℓ ∈ lowest k S ↔ ℓ ∈ S ∧ (S.filter fun ℓ' => ℓ' < ℓ).card < k := by
+  simp [lowest]
+
+private lemma card_below_strictMonoOn (S : Finset α) :
+    StrictMonoOn (fun ℓ => (S.filter fun x => x < ℓ).card) S := by
+  intro ℓ hℓ ℓ' _ hlt
+  refine card_lt_card ⟨fun x hx => ?_, fun hsub => ?_⟩
+  · exact mem_filter.2 ⟨(mem_filter.1 hx).1, (mem_filter.1 hx).2.trans hlt⟩
+  · exact lt_irrefl ℓ (mem_filter.1 (hsub (mem_filter.2 ⟨hℓ, hlt⟩))).2
+
+/-- Every selected element precedes every unselected element of the set. -/
+theorem lowest_lt {k : ℕ} {S : Finset α} {ℓ ℓ' : α} (hℓ : ℓ ∈ lowest k S)
+    (hℓ' : ℓ' ∈ S \ lowest k S) : ℓ < ℓ' := by
+  obtain ⟨hS, hbelow⟩ := mem_lowest.1 hℓ
+  obtain ⟨hS', hnot⟩ := mem_sdiff.1 hℓ'
+  by_contra hlt
+  exact hnot (mem_lowest.2
+    ⟨hS', ((card_below_strictMonoOn S).monotoneOn hS' hS (not_lt.1 hlt)).trans_lt hbelow⟩)
+
+/-- An initial subset is determined by its cardinality. -/
+theorem eq_lowest_of_lt {S T : Finset α} (hT : T ⊆ S)
+    (h : ∀ ℓ ∈ T, ∀ ℓ' ∈ S \ T, ℓ < ℓ') : T = lowest T.card S := by
+  ext ℓ
+  rw [mem_lowest]
+  constructor
+  · -- Predecessors of a selected element belong to the initial subset.
+    refine fun hℓ => ⟨hT hℓ, card_lt_card ⟨fun x hx => ?_, fun hsub => ?_⟩⟩
+    · by_contra hxT
+      exact lt_asymm (mem_filter.1 hx).2 (h ℓ hℓ x (mem_sdiff.2 ⟨(mem_filter.1 hx).1, hxT⟩))
+    · exact lt_irrefl ℓ (mem_filter.1 (hsub hℓ)).2
+  · -- All selected elements precede an omitted element.
+    rintro ⟨hℓS, hcard⟩
+    by_contra hℓT
+    refine absurd (card_le_card fun x hx => ?_) (not_le.2 hcard)
+    exact mem_filter.2 ⟨hT hx, h x hx ℓ (mem_sdiff.2 ⟨hℓS, hℓT⟩)⟩
+
+private lemma image_card_below (S : Finset α) :
+    (S.image fun ℓ => (S.filter fun x => x < ℓ).card) = range S.card := by
+  refine eq_of_subset_of_card_le (fun n hn => ?_) ?_
+  · obtain ⟨ℓ, hℓ, rfl⟩ := mem_image.1 hn
+    exact mem_range.2
+      (card_lt_card ⟨filter_subset _ _, fun hsub => lt_irrefl ℓ (mem_filter.1 (hsub hℓ)).2⟩)
+  · rw [card_image_of_injOn (card_below_strictMonoOn S).injOn, card_range]
+
+/-- Selection saturates at the size of the original set. -/
+theorem card_lowest (k : ℕ) (S : Finset α) : (lowest k S).card = min k S.card := by
+  have hinj := (card_below_strictMonoOn S).injOn.mono (coe_subset.2 (lowest_subset k S))
+  have hrange : ((range S.card).filter fun n => n < k) = range (min k S.card) := by
+    ext n
+    simp only [mem_filter, mem_range, lt_min_iff, and_comm]
+  rw [← card_image_of_injOn hinj, ← card_range (min k S.card), ← hrange, ← image_card_below,
+    filter_image]
+  rfl
+
+end Finset
diff --git a/ComplexityTests/SchonhageBoxes.lean b/ComplexityTests/SchonhageBoxes.lean
new file mode 100644
index 0000000000..bd02d3ae96
--- /dev/null
+++ b/ComplexityTests/SchonhageBoxes.lean
@@ -0,0 +1,93 @@
+/-
+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.BoxesFromLeaves
+
+/-!
+Finite box regressions: both order conditions, saturation/empty boundaries, exact box
+counts, signed value recurrence, and a query whose low-order term cannot be omitted.
+These tests assert no native program, lookup or preprocessing bound.
+-/
+
+open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+namespace SchonhageBoxesTests
+
+example : lowest 2 ({-7, 4, 1} : Finset ℤ) = {-7, 1} := by decide
+example : lowest 10 ({-7, 4, 1} : Finset ℤ) = {-7, 1, 4} := by decide
+example : lowest 0 ({-7, 4, 1} : Finset ℤ) = ∅ := by decide
+
+example : IsBox 2 0 (![.star, .term .P0] : Cube 2) := by decide
+example : ¬IsBox 2 0 (![.term .P0, .star] : Cube 2) := by decide
+example : ¬IsBox 1 1 (![.star] : Cube 1) := by decide
+example : IsBox 1 1 (![.term (.P 0 0)] : Cube 1) := by decide
+example : IsBox 0 0 (Fin.elim0 : Cube 0) := by decide
+
+example : (boxes 0 0 0).card = 1 := by decide +kernel
+example : (boxes 1 1 0).card = 11 := by decide +kernel
+example : (boxes 1 1 1).card = 9 := by decide +kernel
+example : (Cube.leaves (![.star, .star] : Cube 2)).card = 100 := by decide +kernel
+
+-- Real signed inputs with both x/y contributions and a nonzero p/q product.
+private def a (u : LeftStr 1) : ℤ :=
+  match u 0 with
+  | .x i => ![1, 2, -1] i
+  | .p i j => !![-3, 2; 0, 5] i j
+
+private def b (v : RightStr 1) : ℤ :=
+  match v 0 with
+  | .y j => ![3, -2, 1] j
+  | .q i j => !![2, -1; 4, 0] i j
+
+private def inner : OutStr 1 := ![.z0]
+
+example : encodeLeft (![.P0] : Leaf 1) a * encodeRight (![.P0] : Leaf 1) b = -4 := by
+  decide +kernel
+
+-- At threshold 1, omitting the low-order product changes -8 to -4.
+example : ∑ τ ∈ lowLeaves 1 1 inner, encodeLeft τ a * encodeRight τ b = -4 := by
+  decide +kernel
+example : ∑ V ∈ boxLevelSets 1 1 inner, ∑ π ∈ boxesAt inner V, Cube.val a b π = -4 := by
+  decide +kernel
+example : boxQuery 1 1 a b inner = -8 := by decide +kernel
+
+-- At threshold zero, the whole answer is the value of one starred box.
+example : lowLeaves 1 0 inner = ∅ ∧
+    ((boxLevelSets 1 0 inner).biUnion (boxesAt inner)).card = 1 := by decide +kernel
+example : boxQuery 1 0 a b inner = -8 := by decide +kernel
+example : Cube.val a b (![.star] : Cube 1) = -8 := by decide +kernel
+example : boxValue (encodingL a) (encodingR b) 1 (![.star] : Cube 1) = -8 := by
+  decide +kernel
+
+example : boxQuery 1 1 a b inner = bilinearProduct a b inner :=
+  (bilinearProduct_eq_boxQuery 1 1 (by decide) a b inner (by decide)).symm
+
+-- Both signed inputs nonzero, while the full starred sum cancels exactly.
+private def cancelA (u : LeftStr 1) : ℤ :=
+  match u 0 with
+  | .x i => ![1, 2, -1] i
+  | .p _ _ => 0
+private def cancelB (v : RightStr 1) : ℤ :=
+  match v 0 with
+  | .y j => ![3, -2, 1] j
+  | .q _ _ => 0
+
+example : Cube.val cancelA cancelB (![.star] : Cube 1) = 0 ∧
+    encodeLeft (![.P0] : Leaf 1) cancelA * encodeRight (![.P0] : Leaf 1) cancelB = -4 := by
+  decide +kernel
+
+example : boxQuery 0 0 (fun _ : LeftStr 0 => 2) (fun _ : RightStr 0 => -3) Fin.elim0 = -6 := by
+  decide +kernel
+
+-- A concrete client of the cardinal bound and of the exact-threshold indexing bijection.
+example : (boxes 2 1 1).card ≤ 2 * ∑ d ∈ Icc 1 1, beta 2 1 d :=
+  card_boxes_le 2 1 1 (by decide) (by decide)
+
+example : ∃! τ : Leaf 1, (Leaf.Contributes τ inner ∧ order 1 τ = 0) ∧
+    starBelow inner τ = (![.star] : Cube 1) :=
+  existsUnique_starBelow_eq (by decide) (by decide) (by decide +kernel)
+
+end SchonhageBoxesTests
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 42b8f4602a..c88bd0fdb6 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -402,6 +402,18 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   [#1394](https://github.com/cslib-community/complexitylib/issues/1394), including the improved
   Section 4 route needed for the published exponent 1.9992. Anthropic's copyright and attribution
   are retained; the native proofs and representation choices are local.
+* **Finite Section 4 boxes.** The cube/box prerequisite ([#2160](https://github.com/cslib-community/complexitylib/issues/2160))
+  adapts `Sec4/{Boxes,Lemma27_28,BoxesFromLeaves,Lemma29}` at the same formal-math pin,
+  preserving Anthropic's credit and reusing the existing terms, encodings, signed leaf order
+  and alpha/beta counts. Cubes fix terms or admit every term at a star; boxes additionally
+  constrain the star/P0 count and ordering. Output boxes partition exactly the high-order
+  contributing leaves; low-order products remain explicit in the signed sum identity.
+  The finite value recurrence recomputes children and is not a memoized native data structure.
+  Its count bound needs only `m ≤ L` and `t ≤ m`, weakening the source's `10*m ≤ L` premise.
+  The reusable initial-subset argument is generalized to arbitrary linear orders in the small
+  Mathlib-intended `Foundations/Data/Finset/Lowest` topic module, used by the canonical boxes.
+  Native box enumeration/trie construction/query costs and the tuned 1.9992 route remain #1394.
+  No curated abstract or rendering changes are needed for this finite prerequisite.
 * **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