diff --git a/Complexity.lean b/Complexity.lean
index 2885e220b0..30ac15bbdf 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -30,6 +30,10 @@ public import Complexity.Algorithms.Lean.VanEmdeBoas.Elements
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Layout
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Successor
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Alphabets
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Full
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Identity
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Pruned
 public import Complexity.Algorithms.Reachability.BreadthFirst
 public import Complexity.Algorithms.Reachability.InductiveCounting
 public import Complexity.Algorithms.Reachability.InductiveCounting.Bounds
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Alphabets.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Alphabets.lean
new file mode 100644
index 0000000000..34bcd43e19
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Alphabets.lean
@@ -0,0 +1,251 @@
+/-
+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.LinearAlgebra.Matrix.Notation
+public import Mathlib.Tactic.DeriveFintype
+
+/-!
+# The alphabets and coefficient forms of Schönhage's tensor
+
+Seven left variables, seven right variables, ten output variables and ten multiplication
+terms are represented explicitly. Indices start at zero. Linear forms are coefficient
+functions over integers; no arithmetic operation is treated as a native machine instruction.
+
+## Main definitions
+
+* `LeftVar`, `RightVar`, `OutVar`, `Term`: the four finite alphabets.
+* `phi`, `psi`, `chi`: the left, right and output coefficient forms.
+* `Term.Contributes`: occurrence in an output form.
+
+## Main results
+
+* `card_leftVar`, `card_rightVar`, `card_term`: alphabet sizes.
+* `Term.contributes_iff`, `chi_eq_ite`: output incidence and its coefficient.
+
+## References
+
+Part of [AlmanWilliams2026, Section 2]. Direct mathematical adaptation of
+[Anthropic's pinned formal source](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec2).
+Definitions are selectively extracted from that pin's `PaperStatements.lean`; no machine
+semantics or running-time statement is imported. The docstrings below explain the local
+declarations in our own words.
+-/
+
+@[expose] public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Left input coordinates: three `x` coordinates and a two-by-two family of `p` coordinates. -/
+inductive LeftVar : Type
+  | x (i : Fin 3)
+  | p (i j : Fin 2)
+  deriving DecidableEq, Fintype
+
+/-- Right input coordinates: three `y` coordinates and a two-by-two family of `q` coordinates. -/
+inductive RightVar : Type
+  | y (j : Fin 3)
+  | q (i j : Fin 2)
+  deriving DecidableEq, Fintype
+
+/-- Output coordinates comprise a three-by-three outer family and one distinguished inner
+coordinate.
+-/
+inductive OutVar : Type
+  | z (i j : Fin 3)
+  | z0
+  deriving DecidableEq, Fintype
+
+/-- The multiplication labels consist of nine indexed labels `P i j` and the additional label
+`P0`.
+-/
+inductive Term : Type
+  | P (i j : Fin 3)
+  | P0
+  deriving DecidableEq, Fintype
+
+/-- The linear form consisting of the single left variable `x_i`.
+-/
+def xForm (i : Fin 3) : LeftVar → ℤ := Pi.single (LeftVar.x i) 1
+/-- The linear form consisting of the single left variable `p_ij`.
+-/
+def pForm (i j : Fin 2) : LeftVar → ℤ := Pi.single (LeftVar.p i j) 1
+/-- The linear form consisting of the single right variable `y_j`.
+-/
+def yForm (j : Fin 3) : RightVar → ℤ := Pi.single (RightVar.y j) 1
+/-- The linear form consisting of the single right variable `q_ij`.
+-/
+def qForm (i j : Fin 2) : RightVar → ℤ := Pi.single (RightVar.q i j) 1
+/-- The linear form consisting of the single output variable `z_ij`.
+-/
+def zForm (i j : Fin 3) : OutVar → ℤ := Pi.single (OutVar.z i j) 1
+/-- The linear form consisting of the single output variable `z₀`.
+-/
+def z0Form : OutVar → ℤ := Pi.single OutVar.z0 1
+
+/-- Extend the two-by-two `p` family to three rows by cancelling each column sum; the third column
+is zero.
+-/
+def pHat : Matrix (Fin 3) (Fin 3) (LeftVar → ℤ) :=
+  !![pForm 0 0, pForm 0 1, 0;
+     pForm 1 0, pForm 1 1, 0;
+     -pForm 0 0 - pForm 1 0, -pForm 0 1 - pForm 1 1, 0]
+
+/-- Extend the two-by-two `q` family to three columns by cancelling each row sum; the third row is
+zero.
+-/
+def qHat : Matrix (Fin 3) (Fin 3) (RightVar → ℤ) :=
+  !![qForm 0 0, qForm 0 1, -qForm 0 0 - qForm 0 1;
+     qForm 1 0, qForm 1 1, -qForm 1 0 - qForm 1 1;
+     0, 0, 0]
+
+/-- Left coefficients for each multiplication label. An indexed label adds its `x` coordinate to
+the corresponding `pHat` form; `P0` negates the sum of the three `x` coordinates.
+-/
+def phi : Term → LeftVar → ℤ
+  | .P i j => xForm i + pHat i j
+  | .P0 => -(xForm 0 + xForm 1 + xForm 2)
+
+/-- Right coefficients for each multiplication label. Indexed labels use `y` plus `qHat`, whereas
+`P0` uses the sum of the three `y` coordinates.
+-/
+def psi : Term → RightVar → ℤ
+  | .P i j => yForm j + qHat i j
+  | .P0 => yForm 0 + yForm 1 + yForm 2
+
+/-- Output coefficients: each indexed label occurs in its own outer coordinate and in `z0`; `P0`
+occurs only in `z0`.
+-/
+def chi : Term → OutVar → ℤ
+  | .P i j => zForm i j + z0Form
+  | .P0 => z0Form
+
+/-- Select the distinguished output coordinate, excluding the indexed outer coordinates. -/
+def OutVar.IsInner : OutVar → Prop
+  | .z _ _ => False
+  | .z0 => True
+
+instance OutVar.instDecidablePredIsInner : DecidablePred OutVar.IsInner
+  | .z _ _ => isFalse fun h => h
+  | .z0 => isTrue trivial
+
+/-- A label is relevant to an output coordinate when its output coefficient is nonzero. -/
+def Term.Contributes (lam : Term) (z : OutVar) : Prop := chi lam z ≠ 0
+
+instance Term.instDecidableContributes (lam : Term) (z : OutVar) : Decidable (lam.Contributes z) :=
+  inferInstanceAs (Decidable (chi lam z ≠ 0))
+
+/-- Choose the indexed label for an outer coordinate and `P0` for the inner coordinate. Applying
+this choice coordinatewise defines a private leaf.
+-/
+def OutVar.privateTerm : OutVar → Term
+  | .z i j => .P i j
+  | .z0 => .P0
+
+/-- A length-`L` tuple of left coordinates, indexed from zero. -/
+abbrev LeftStr (L : ℕ) : Type := Fin L → LeftVar
+/-- A length-`L` tuple with entries in `RightVar`. -/
+abbrev RightStr (L : ℕ) : Type := Fin L → RightVar
+/-- A length-`L` tuple with entries in `OutVar`. -/
+abbrev OutStr (L : ℕ) : Type := Fin L → OutVar
+/-- The sequence of multiplication labels identifying a depth-`k` recursion vertex. -/
+abbrev Vertex (k : ℕ) : Type := Fin k → Term
+/-- A terminal vertex, whose label sequence has the full recursion depth. -/
+abbrev Leaf (L : ℕ) : Type := Vertex L
+
+/-! ### The alphabets -/
+
+/-- The left variables, listed: `x i` is `.inl i`, and `p i j` is `.inr (i, j)`.
+-/
+def LeftVar.equiv : LeftVar ≃ Fin 3 ⊕ Fin 2 × Fin 2 where
+  toFun
+    | .x i => .inl i
+    | .p i j => .inr (i, j)
+  invFun
+    | .inl i => .x i
+    | .inr (i, j) => .p i j
+  left_inv s := by cases s <;> rfl
+  right_inv s := by rcases s with _ | ⟨_, _⟩ <;> rfl
+
+/-- The right variables, listed: `y j` is `.inl j`, and `q i j` is `.inr (i, j)`.
+-/
+def RightVar.equiv : RightVar ≃ Fin 3 ⊕ Fin 2 × Fin 2 where
+  toFun
+    | .y j => .inl j
+    | .q i j => .inr (i, j)
+  invFun
+    | .inl j => .y j
+    | .inr (i, j) => .q i j
+  left_inv t := by cases t <;> rfl
+  right_inv t := by rcases t with _ | ⟨_, _⟩ <;> rfl
+
+/-- The terms, listed: `P i j` is `some (i, j)`, and `P0` is `none`.
+-/
+def Term.equiv : Term ≃ Option (Fin 3 × Fin 3) where
+  toFun
+    | .P i j => some (i, j)
+    | .P0 => none
+  invFun
+    | some (i, j) => .P i j
+    | none => .P0
+  left_inv t := by cases t <;> rfl
+  right_inv t := by rcases t with _ | ⟨_, _⟩ <;> rfl
+
+/-- The left alphabet has cardinality seven. -/
+theorem card_leftVar : Fintype.card LeftVar = 7 := by
+  simp [Fintype.card_congr LeftVar.equiv]
+
+/-- The right alphabet has cardinality seven. -/
+theorem card_rightVar : Fintype.card RightVar = 7 := by
+  simp [Fintype.card_congr RightVar.equiv]
+
+/-- There are ten multiplication labels. -/
+theorem card_term : Fintype.card Term = 10 := by
+  simp [Fintype.card_congr Term.equiv]
+
+/-! ### Which terms contribute to which output variables -/
+
+/-- The inner coordinate receives a contribution from every multiplication label. -/
+@[simp]
+theorem Term.contributes_z0 (lam : Term) : lam.Contributes .z0 := by
+  cases lam <;> simp [Term.Contributes, chi, zForm, z0Form]
+
+/-- For an outer coordinate, relevance determines both indices of the multiplication label. -/
+@[simp]
+theorem Term.contributes_z_iff (lam : Term) (i j : Fin 3) :
+    lam.Contributes (.z i j) ↔ lam = .P i j := by
+  cases lam <;> simp [Term.Contributes, chi, zForm, z0Form, Pi.single_apply, eq_comm]
+
+/-- Relevance has two possibilities: the output is inner, or the label is the private label
+selected by that output.
+-/
+theorem Term.contributes_iff (lam : Term) (z : OutVar) :
+    lam.Contributes z ↔ z.IsInner ∨ lam = z.privateTerm := by
+  decide +revert
+
+/-- Separate decoding into its two cases: an outer output selects one summand; the inner output
+sums the whole label family.
+-/
+theorem Term.sum_contributes {A : Type*} [AddCommMonoid A] (c : Term → A) (z : OutVar) :
+    ∑ lam : Term with lam.Contributes z, c lam
+      = match z with
+        | .z i j => c (.P i j)
+        | .z0 => ∑ lam, c lam := by
+  cases z with
+  | z i j => simp [filter_eq']
+  | z0 => simp
+
+/-- Each output coefficient is the zero-or-one indicator of `Term.Contributes`. -/
+theorem chi_eq_ite (lam : Term) (z : OutVar) :
+    chi lam z = if lam.Contributes z then 1 else 0 := by
+  decide +revert
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Full.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Full.lean
new file mode 100644
index 0000000000..801a2b80b3
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Full.lean
@@ -0,0 +1,334 @@
+/-
+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.Alphabets
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Data.Fintype.BigOperators
+public import Mathlib.Data.Finset.Pi
+import Mathlib.Tactic.Ring
+
+/-!
+# Full tensor recursion and shared encodings
+
+The recursion works on mathematical arrays indexed by finite strings. Its multiplication
+record identifies the two encoded integers at each leaf. The returned array equals the
+bilinear tensor expansion. These recursive values and combinatorial counts carry no native
+instruction-cost interpretation.
+
+## Main definitions
+
+* `Full.run`, `Full.result`, `Full.multipliedAt`: full evaluation and leaf operands.
+* `encodeLeft`, `encodeRight`, `encodingL`, `encodingR`: shared leaf encodings.
+* `bilinearProduct`, `coefficient`, `leaves`: the tensor expansion and contributing leaves.
+
+## Main results
+
+* `full_spec`: full evaluation returns the bilinear product and uses the stated encodings.
+* `tensor_expansion`: expansion into products of the one-level tensor coefficients.
+* `abs_phi_le_one`, `abs_psi_le_one`: bounded encoding coefficients.
+
+## References
+
+Part of [AlmanWilliams2026, Section 2]. Direct mathematical adaptation of
+[Anthropic's pinned formal source](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec2).
+Definitions are selectively extracted from that pin's `PaperStatements.lean`; no machine
+semantics or running-time statement is imported. The docstrings below explain the local
+declarations in our own words.
+-/
+
+@[expose] public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Fix the first coordinate of a tuple-indexed array and retain the shorter tuple as its
+argument. The construction works for any coordinate alphabet and value type.
+-/
+def sliceAt {α β : Type} {L : ℕ} (a : (Fin (L + 1) → α) → β) (s : α) : (Fin L → α) → β :=
+  fun u' => a (Fin.cons s u')
+
+/-- Apply the left coefficient form for `lam` to all first-coordinate slices of the input array. -/
+def encodeStepL {L : ℕ} (lam : Term) (a : LeftStr (L + 1) → ℤ) : LeftStr L → ℤ :=
+  fun u' => ∑ s, phi lam s * sliceAt a s u'
+
+/-- Apply the right coefficient form for `lam` to all first-coordinate slices of the input array. -/
+def encodeStepR {L : ℕ} (lam : Term) (b : RightStr (L + 1) → ℤ) : RightStr L → ℤ :=
+  fun v' => ∑ t, psi lam t * sliceAt b t v'
+
+/-- Evaluate the two arrays and retain the operands used at each leaf. At depth zero, multiply
+their unique entries. At positive depth, apply each term’s left and right coefficient forms,
+recurse, and decode the child results into an output array. The second component maps each term
+string to its pair of encoded input values. This is a finite integer recursion, with no
+instruction counter.
+-/
+def Full.run : (L : ℕ) → (LeftStr L → ℤ) → (RightStr L → ℤ) → (OutStr L → ℤ) × (Leaf L → ℤ × ℤ)
+  | 0, a, b => (fun _ => a Fin.elim0 * b Fin.elim0, fun _ => (a Fin.elim0, b Fin.elim0))
+  | L + 1, a, b =>
+    let R : Term → (OutStr L → ℤ) × (Leaf L → ℤ × ℤ) := fun lam =>
+      Full.run L (encodeStepL lam a) (encodeStepR lam b)
+    (fun w =>
+        match w 0 with
+        | .z i j => (R (.P i j)).1 (Fin.tail w)
+        | .z0 => ∑ lam, (R lam).1 (Fin.tail w),
+      fun τ => (R (τ 0)).2 (Fin.tail τ))
+
+/-- Project the output array from full evaluation, discarding its record of leaf operands. -/
+def Full.result (L : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : OutStr L → ℤ :=
+  (Full.run L a b).1
+
+/-- Read the ordered pair of leaf operands recorded by `Full.run`. -/
+def Full.multipliedAt (L : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (τ : Leaf L) : ℤ × ℤ :=
+  (Full.run L a b).2 τ
+
+/-! ### 2.3.2 Unraveling the recursion computation -/
+
+/-- Evaluate the left encoding at one leaf by weighting each input entry with the product of its
+coordinate coefficients.
+-/
+def encodeLeft {L : ℕ} (τ : Leaf L) (a : LeftStr L → ℤ) : ℤ := ∑ u, a u * ∏ ℓ, phi (τ ℓ) (u ℓ)
+
+/-- Evaluate the right encoding at one leaf using the corresponding products of right
+coefficients.
+-/
+def encodeRight {L : ℕ} (τ : Leaf L) (b : RightStr L → ℤ) : ℤ := ∑ v, b v * ∏ ℓ, psi (τ ℓ) (v ℓ)
+
+/-- A leaf is relevant to an output tuple when its labels are relevant at every coordinate. -/
+def Leaf.Contributes {L : ℕ} (τ : Leaf L) (w : OutStr L) : Prop :=
+  ∀ ℓ, (τ ℓ).Contributes (w ℓ)
+
+instance Leaf.instDecidableContributes {L : ℕ} (τ : Leaf L) (w : OutStr L) :
+    Decidable (Leaf.Contributes τ w) :=
+  inferInstanceAs (Decidable (∀ ℓ, (τ ℓ).Contributes (w ℓ)))
+
+/-- For each output tuple, sum the products of left and right encodings over its relevant leaves. -/
+def bilinearProduct {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : OutStr L → ℤ :=
+  fun w => ∑ τ : Leaf L with Leaf.Contributes τ w, encodeLeft τ a * encodeRight τ b
+
+/-- The coefficient linking one left, right and output coordinate, obtained by summing products of
+the relevant label coefficients.
+-/
+def coefficient (s : LeftVar) (t : RightVar) (z : OutVar) : ℤ :=
+  ∑ lam : Term with lam.Contributes z, phi lam s * psi lam t
+
+/-- Package all left-encoding values into an array indexed by leaves. -/
+def encodingL {L : ℕ} (a : LeftStr L → ℤ) : Leaf L → ℤ := fun τ => encodeLeft τ a
+
+/-- Package all right-encoding values into an array indexed by leaves. -/
+def encodingR {L : ℕ} (b : RightStr L → ℤ) : Leaf L → ℤ := fun τ => encodeRight τ b
+
+/-- Take the union of the relevant-leaf sets of all requested output tuples. -/
+def leaves {L : ℕ} (U : Finset (OutStr L)) : Finset (Leaf L) :=
+  univ.filter fun τ => ∃ w ∈ U, Leaf.Contributes τ w
+
+/-- Counting length-`L` left tuples gives `7^L`. -/
+theorem card_leftStr (L : ℕ) : Fintype.card (LeftStr L) = 7 ^ L := by
+  rw [Fintype.card_fun, card_leftVar, Fintype.card_fin]
+
+/-- Counting length-`L` right tuples gives `7^L`. -/
+theorem card_rightStr (L : ℕ) : Fintype.card (RightStr L) = 7 ^ L := by
+  rw [Fintype.card_fun, card_rightVar, Fintype.card_fin]
+
+/-- A depth-`k` label sequence has ten independent choices at each position. -/
+theorem card_vertex (k : ℕ) : Fintype.card (Vertex k) = 10 ^ k := by
+  rw [Fintype.card_fun, card_term, Fintype.card_fin]
+
+/-- Every left coefficient has absolute value at most one. -/
+theorem abs_phi_le_one (lam : Term) (s : LeftVar) : |phi lam s| ≤ 1 := by
+  decide +revert
+
+/-- Every right coefficient has absolute value at most one. -/
+theorem abs_psi_le_one (lam : Term) (t : RightVar) : |psi lam t| ≤ 1 := by
+  decide +revert
+
+/-- The support of any left coefficient form has cardinality at most three. -/
+theorem card_support_phi_le (lam : Term) : (univ.filter fun s => phi lam s ≠ 0).card ≤ 3 := by
+  decide +revert
+
+/-- The support of any right coefficient form has cardinality at most three. -/
+theorem card_support_psi_le (lam : Term) : (univ.filter fun t => psi lam t ≠ 0).card ≤ 3 := by
+  decide +revert
+
+/-! ### Which leaves contribute to an output string -/
+
+/-- Split coordinatewise leaf relevance into the first label and the remaining label tuple. -/
+theorem Leaf.contributes_succ {L : ℕ} {τ : Leaf (L + 1)} {w : OutStr (L + 1)} :
+    Leaf.Contributes τ w
+      ↔ (τ 0).Contributes (w 0) ∧ Leaf.Contributes (Fin.tail τ) (Fin.tail w) := by
+  simp only [Leaf.Contributes, Fin.forall_fin_succ, Fin.tail]
+
+/-- A sum over the strings of length `L + 1` is a sum over the first variable `s` and the rest
+`u'` of the string `s u'`.
+-/
+private theorem sum_strings_succ {α : Type*} [Fintype α] {L : ℕ} (f : (Fin (L + 1) → α) → ℤ) :
+    ∑ u, f u = ∑ s, ∑ u', f (Fin.cons s u') := by
+  rw [← Fintype.sum_prod_type']
+  exact (Fintype.sum_equiv (Fin.consEquiv fun _ => α) _ _ fun _ => rfl).symm
+
+/-- A sum over the leaves contributing to `w`, split by the first term of the leaf.
+-/
+theorem Leaf.sum_contributes_succ {L : ℕ} (w : OutStr (L + 1)) (f : Leaf (L + 1) → ℤ) :
+    ∑ τ : Leaf (L + 1) with Leaf.Contributes τ w, f τ
+      = ∑ lam : Term with lam.Contributes (w 0),
+          ∑ τ' : Leaf L with Leaf.Contributes τ' (Fin.tail w), f (Fin.cons lam τ') := by
+  simp only [sum_filter, sum_strings_succ, Leaf.contributes_succ, Fin.cons_zero,
+    Fin.tail_cons]
+  refine sum_congr rfl fun lam _ => ?_
+  by_cases h : lam.Contributes (w 0) <;> simp [h]
+
+/-- The relevant-leaf filter is a product of the allowed label sets at individual coordinates. -/
+theorem Leaf.filter_contributes_eq_piFinset {L : ℕ} (w : OutStr L) :
+    (univ.filter fun τ : Leaf L => Leaf.Contributes τ w)
+      = Fintype.piFinset fun ℓ => univ.filter fun lam : Term => lam.Contributes (w ℓ) := by
+  ext τ
+  simp only [mem_filter, mem_univ, true_and, Fintype.mem_piFinset]
+  rfl
+
+/-- Membership in `leaves(U)`.
+-/
+@[simp]
+theorem mem_leaves {L : ℕ} {U : Finset (OutStr L)} {τ : Leaf L} :
+    τ ∈ leaves U ↔ ∃ w ∈ U, Leaf.Contributes τ w := by
+  simp [leaves]
+
+/-! ### The two encodings at once -/
+
+section encodeWith
+
+variable {α : Type} [Fintype α] (c : Term → α → ℤ) {L : ℕ}
+
+/-- Encoding for an arbitrary coefficient family: weight each array entry by the product of
+coefficients selected by the leaf. This specializes to both input encodings.
+-/
+def encodeWith (τ : Leaf L) (a : (Fin L → α) → ℤ) : ℤ := ∑ u, a u * ∏ ℓ, c (τ ℓ) (u ℓ)
+
+/-- With no coordinates, the encoding evaluates the array at its unique empty argument. -/
+theorem encodeWith_zero (τ : Leaf 0) (a : (Fin 0 → α) → ℤ) : encodeWith c τ a = a Fin.elim0 := by
+  simp [encodeWith, Subsingleton.elim (default : Fin 0 → α) Fin.elim0]
+
+/-- Process the first label of an encoding by combining the first-coordinate slices, then encode
+the resulting shorter array.
+-/
+theorem encodeWith_cons (lam : Term) (τ' : Leaf L) (a : (Fin (L + 1) → α) → ℤ) :
+    encodeWith c (Fin.cons lam τ' : Leaf (L + 1)) a
+      = encodeWith c τ' fun u' => ∑ s, c lam s * sliceAt a s u' := by
+  simp only [encodeWith, sum_strings_succ, Fin.prod_univ_succ, Fin.cons_zero, Fin.cons_succ,
+    sliceAt, sum_mul]
+  rw [sum_comm]
+  exact sum_congr rfl fun u' _ => sum_congr rfl fun s _ => by ring
+
+end encodeWith
+
+/-! ### Lemma 7 -/
+
+/-- The left encoding at a cons leaf is the tail encoding of the array produced by `encodeStepL`. -/
+theorem encodeLeft_cons {L : ℕ} (lam : Term) (τ' : Leaf L) (a : LeftStr (L + 1) → ℤ) :
+    encodeLeft (Fin.cons lam τ' : Leaf (L + 1)) a = encodeLeft τ' (encodeStepL lam a) :=
+  encodeWith_cons phi lam τ' a
+
+/-- The right encoding at a cons leaf is the tail encoding of the array produced by
+`encodeStepR`.
+-/
+theorem encodeRight_cons {L : ℕ} (lam : Term) (τ' : Leaf L) (b : RightStr (L + 1) → ℤ) :
+    encodeRight (Fin.cons lam τ' : Leaf (L + 1)) b = encodeRight τ' (encodeStepR lam b) :=
+  encodeWith_cons psi lam τ' b
+
+/-- The zero-depth left encoding reads the array at the empty tuple. -/
+private theorem encodeLeft_zero (τ : Leaf 0) (a : LeftStr 0 → ℤ) : encodeLeft τ a = a Fin.elim0 :=
+  encodeWith_zero phi τ a
+
+/-- At depth zero, the right encoding equals the input entry at the unique empty string.
+-/
+private theorem encodeRight_zero (τ : Leaf 0) (b : RightStr 0 → ℤ) :
+    encodeRight τ b = b Fin.elim0 :=
+  encodeWith_zero psi τ b
+
+/-- The operand record of full evaluation agrees with `encodeLeft` and `encodeRight` at every
+leaf.
+-/
+theorem Full.multipliedAt_eq_encoding {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ)
+    (τ : Leaf L) :
+    Full.multipliedAt L a b τ = (encodeLeft τ a, encodeRight τ b) := by
+  induction L with
+  | zero =>
+    rw [encodeLeft_zero, encodeRight_zero]
+    rfl
+  | succ L ih =>
+    -- The leaf `τ` is `λ τ'` with `λ = τ 0` and `τ' = Fin.tail τ`. By steps (2) and (3) it is the
+    -- leaf `τ'` of `Full.result(A_λ, B_λ)`.
+    have hstep : Full.multipliedAt (L + 1) a b τ
+        = Full.multipliedAt L (encodeStepL (τ 0) a) (encodeStepR (τ 0) b) (Fin.tail τ) := rfl
+    rw [hstep, ih, ← encodeLeft_cons, ← encodeRight_cons, Fin.cons_self_tail]
+
+/-- Unfold full evaluation once and express decoding as a sum over labels relevant to the leading
+output coordinate.
+-/
+theorem Full.result_succ {L : ℕ} (a : LeftStr (L + 1) → ℤ) (b : RightStr (L + 1) → ℤ)
+    (w : OutStr (L + 1)) :
+    Full.result (L + 1) a b w = ∑ lam : Term with lam.Contributes (w 0),
+      Full.result L (encodeStepL lam a) (encodeStepR lam b) (Fin.tail w) := by
+  rw [Term.sum_contributes]
+  rfl
+
+/-- The bilinear product obeys the same first-coordinate decoding recurrence as full evaluation. -/
+theorem bilinearProduct_succ {L : ℕ} (a : LeftStr (L + 1) → ℤ) (b : RightStr (L + 1) → ℤ)
+    (w : OutStr (L + 1)) :
+    bilinearProduct a b w = ∑ lam : Term with lam.Contributes (w 0),
+      bilinearProduct (encodeStepL lam a) (encodeStepR lam b) (Fin.tail w) := by
+  simp only [bilinearProduct, Leaf.sum_contributes_succ, encodeLeft_cons, encodeRight_cons]
+
+/-- Full evaluation computes the bilinear tensor expansion `bilinearProduct`.
+-/
+theorem Full.result_eq_bilinearProduct {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) :
+    Full.result L a b = bilinearProduct a b := by
+  induction L with
+  | zero =>
+    funext w
+    simp [Full.result, Full.run, bilinearProduct, Leaf.Contributes, encodeLeft_zero,
+      encodeRight_zero]
+  | succ L ih =>
+    funext w
+    simp only [Full.result_succ, bilinearProduct_succ, ih]
+
+/-- The complete value specification of full evaluation: its result is `bilinearProduct`, and each
+leaf’s operands are the corresponding left and right encodings.
+-/
+theorem full_spec {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) :
+    (∀ τ : Leaf L, Full.multipliedAt L a b τ = (encodeLeft τ a, encodeRight τ b)) ∧
+      Full.result L a b = bilinearProduct a b :=
+  ⟨Full.multipliedAt_eq_encoding a b, Full.result_eq_bilinearProduct a b⟩
+
+/-! ### Lemma 8 -/
+
+/-- Expand the product of one-coordinate coefficients as a sum of coefficient products indexed by
+relevant leaves.
+-/
+theorem prod_gamma_eq_sum_contributes {L : ℕ} (u : LeftStr L) (v : RightStr L) (w : OutStr L) :
+    ∏ ℓ, coefficient (u ℓ) (v ℓ) (w ℓ)
+      = ∑ τ : Leaf L with Leaf.Contributes τ w, (∏ ℓ, phi (τ ℓ) (u ℓ)) * ∏ ℓ, psi (τ ℓ) (v ℓ) := by
+  simp only [coefficient]
+  rw [prod_univ_sum, Leaf.filter_contributes_eq_piFinset]
+  exact sum_congr rfl fun τ _ => prod_mul_distrib
+
+/-- Expand `bilinearProduct` as a double sum of input-entry products. The coefficient of each pair
+is the product, over string positions, of the one-level coefficients.
+-/
+theorem tensor_expansion {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (w : OutStr L) :
+    bilinearProduct a b w = ∑ u, ∑ v, (∏ ℓ, coefficient (u ℓ) (v ℓ) (w ℓ)) * a u * b v := by
+  -- Expand the encoded factors and reorder the finite sums. The coefficient of each input
+  -- product is the product of its one-level coefficients.
+  simp only [bilinearProduct, encodeLeft, encodeRight, sum_mul_sum]
+  rw [sum_comm]
+  refine sum_congr rfl fun u _ => ?_
+  rw [sum_comm]
+  refine sum_congr rfl fun v _ => ?_
+  rw [prod_gamma_eq_sum_contributes, sum_mul, sum_mul]
+  exact sum_congr rfl fun τ _ => by ring
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Identity.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Identity.lean
new file mode 100644
index 0000000000..27995291ad
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Identity.lean
@@ -0,0 +1,201 @@
+/-
+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.Alphabets
+public import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.LinearAlgebra.Finsupp.LinearCombination
+import Mathlib.Tactic.LinearCombination
+
+/-!
+# Schönhage's ten-term polynomial identity
+
+The ten products of linear forms equal the wanted inner/outer product polynomial plus
+an explicit error polynomial. This is an identity over integers in 24 formal variables.
+The error term is retained; it cannot be discarded for unrestricted inputs.
+
+## Main definitions
+
+* `TriPoly`, `formL`, `formR`, `formO`: the polynomial interpretation of the forms.
+* `G`, `E`: the wanted polynomial and the error polynomial.
+
+## Main results
+
+* `identity`: the complete ten-term polynomial identity, including its error.
+
+## References
+
+Part of [AlmanWilliams2026, Section 2]. Direct mathematical adaptation of
+[Anthropic's pinned formal source](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec2).
+Definitions are selectively extracted from that pin's `PaperStatements.lean`; no machine
+semantics or running-time statement is imported. The docstrings below explain the local
+declarations in our own words.
+-/
+
+@[expose] public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- All 24 variables of the identity: the left, the right and the output variables.
+-/
+abbrev Var : Type := LeftVar ⊕ RightVar ⊕ OutVar
+
+/-- The polynomials in which Schönhage's identity is an identity.
+-/
+abbrev TriPoly : Type := MvPolynomial Var ℤ
+
+/-- A left variable, as a polynomial.
+-/
+noncomputable def polyL (s : LeftVar) : TriPoly := MvPolynomial.X (Sum.inl s)
+/-- A right variable, as a polynomial.
+-/
+noncomputable def polyR (t : RightVar) : TriPoly := MvPolynomial.X (Sum.inr (Sum.inl t))
+/-- An output variable, as a polynomial.
+-/
+noncomputable def polyO (z : OutVar) : TriPoly := MvPolynomial.X (Sum.inr (Sum.inr z))
+
+/-- A linear form in the left variables, as a polynomial.
+-/
+noncomputable def formL (f : LeftVar → ℤ) : TriPoly := ∑ s, MvPolynomial.C (f s) * polyL s
+/-- A linear form in the right variables, as a polynomial.
+-/
+noncomputable def formR (f : RightVar → ℤ) : TriPoly := ∑ t, MvPolynomial.C (f t) * polyR t
+/-- A linear form in the output variables, as a polynomial.
+-/
+noncomputable def formO (f : OutVar → ℤ) : TriPoly := ∑ z, MvPolynomial.C (f z) * polyO z
+
+/-- The target polynomial combines the nine outer `x`-`y` products with the four `p`-`q` products
+attached to the inner coordinate.
+-/
+noncomputable def G : TriPoly :=
+  (∑ i : Fin 3, ∑ j : Fin 3, polyL (.x i) * polyR (.y j) * polyO (.z i j))
+    + (∑ i : Fin 2, ∑ j : Fin 2, polyL (.p i j) * polyR (.q i j)) * polyO .z0
+
+/-- The error polynomial collects the additional outer-coordinate terms involving `pHat` or
+`qHat`. It has no inner-coordinate summand.
+-/
+noncomputable def E : TriPoly :=
+  ∑ i : Fin 3, ∑ j : Fin 3,
+    (polyL (.x i) * formR (qHat i j) + formL (pHat i j) * polyR (.y j)
+      + formL (pHat i j) * formR (qHat i j)) * polyO (.z i j)
+
+/-- A sum over the ten terms, split into the `P_ij` and `P₀`.
+-/
+private theorem sum_term {A : Type*} [AddCommMonoid A] (f : Term → A) :
+    ∑ lam, f lam = ∑ i, ∑ j, f (.P i j) + f .P0 := by
+  rw [← Term.equiv.symm.sum_comp f, Fintype.sum_option, Fintype.sum_prod_type, add_comm]
+  rfl
+
+/-! ### Linear forms as polynomials -/
+
+/-- `formL` is the linear map that sends the form consisting of the single variable `s` to the
+polynomial `s`.
+-/
+theorem formL_eq_linearCombination (f : LeftVar → ℤ) :
+    formL f = Fintype.linearCombination ℤ polyL f := by
+  simp only [formL, Fintype.linearCombination_apply, MvPolynomial.smul_eq_C_mul]
+
+/-- `formR` is the linear map that sends the form consisting of the single variable `t` to the
+polynomial `t`.
+-/
+theorem formR_eq_linearCombination (f : RightVar → ℤ) :
+    formR f = Fintype.linearCombination ℤ polyR f := by
+  simp only [formR, Fintype.linearCombination_apply, MvPolynomial.smul_eq_C_mul]
+
+/-- `formO` is the linear map that sends the form consisting of the single variable `z` to the
+polynomial `z`.
+-/
+theorem formO_eq_linearCombination (f : OutVar → ℤ) :
+    formO f = Fintype.linearCombination ℤ polyO f := by
+  simp only [formO, Fintype.linearCombination_apply, MvPolynomial.smul_eq_C_mul]
+
+/-- The form consisting of a single left variable is that variable.
+-/
+theorem formL_single (s : LeftVar) : formL (Pi.single s 1) = polyL s := by
+  simp [formL_eq_linearCombination]
+
+/-- The form consisting of a single right variable is that variable.
+-/
+theorem formR_single (t : RightVar) : formR (Pi.single t 1) = polyR t := by
+  simp [formR_eq_linearCombination]
+
+/-- The form consisting of a single output variable is that variable.
+-/
+theorem formO_single (z : OutVar) : formO (Pi.single z 1) = polyO z := by
+  simp [formO_eq_linearCombination]
+
+/-- Interpret an indexed left coefficient form as the sum of its `x` variable and its extended `p`
+form.
+-/
+theorem formL_phi_P (i j : Fin 3) : formL (phi (.P i j)) = polyL (.x i) + formL (pHat i j) := by
+  simp [phi, xForm, formL_eq_linearCombination]
+
+/-- Interpret an indexed right coefficient form as the sum of its `y` variable and its extended
+`q` form.
+-/
+theorem formR_psi_P (i j : Fin 3) : formR (psi (.P i j)) = polyR (.y j) + formR (qHat i j) := by
+  simp [psi, yForm, formR_eq_linearCombination]
+
+/-- Interpret an indexed output form as the sum of the corresponding outer variable and the inner
+variable.
+-/
+theorem formO_chi_P (i j : Fin 3) : formO (chi (.P i j)) = polyO (.z i j) + polyO .z0 := by
+  simp [chi, zForm, z0Form, formO_eq_linearCombination]
+
+/-- The distinguished left form is the negative sum of the three `x` polynomials. -/
+theorem formL_phi_P0 : formL (phi .P0) = -(polyL (.x 0) + polyL (.x 1) + polyL (.x 2)) := by
+  simp [phi, xForm, formL_eq_linearCombination]
+
+/-- The distinguished right form is the sum of the three `y` polynomials. -/
+theorem formR_psi_P0 : formR (psi .P0) = polyR (.y 0) + polyR (.y 1) + polyR (.y 2) := by
+  simp [psi, yForm, formR_eq_linearCombination]
+
+/-- The distinguished output form denotes the inner polynomial variable alone. -/
+theorem formO_chi_P0 : formO (chi .P0) = polyO .z0 :=
+  formO_single .z0
+
+/-! ### Lemma 6 -/
+
+/-- Summing `pHat` over the row index gives the zero coefficient function. -/
+theorem pHat_column_sum (j : Fin 3) : ∑ i, pHat i j = 0 := by
+  fin_cases j <;> simp [Fin.sum_univ_three, pHat]
+
+/-- Summing `qHat` over the column index gives the zero coefficient function. -/
+theorem qHat_row_sum (i : Fin 3) : ∑ j, qHat i j = 0 := by
+  fin_cases i <;> simp [Fin.sum_univ_three, qHat]
+
+/-- The product sum for the extended arrays reduces to the four products from their original
+two-by-two arrays.
+-/
+theorem sum_pHat_mul_qHat :
+    ∑ i : Fin 3, ∑ j : Fin 3, formL (pHat i j) * formR (qHat i j)
+      = ∑ i : Fin 2, ∑ j : Fin 2, polyL (.p i j) * polyR (.q i j) := by
+  simp [Fin.sum_univ_three, Fin.sum_univ_two, pHat, qHat, pForm, qForm,
+    formL_eq_linearCombination, formR_eq_linearCombination]
+
+/-- The ten products of the coefficient forms equal the wanted polynomial `G` plus the explicit
+error polynomial `E`.
+-/
+theorem identity : ∑ lam, formL (phi lam) * formR (psi lam) * formO (chi lam) = G + E := by
+  -- The column sums of p̂ and the row sums of q̂, as identities of polynomials.
+  have hcol : ∀ j, ∑ i, formL (pHat i j) = 0 := fun j => by
+    simp only [formL_eq_linearCombination, ← map_sum, pHat_column_sum, map_zero]
+  have hrow : ∀ i, ∑ j, formR (qHat i j) = 0 := fun i => by
+    simp only [formR_eq_linearCombination, ← map_sum, qHat_row_sum, map_zero]
+  simp only [Fin.sum_univ_three] at hcol hrow
+  -- Write out the ten terms, and write the inner product in G as ∑ p̂_ij q̂_ij.
+  simp only [sum_term, formL_phi_P, formR_psi_P, formO_chi_P, formL_phi_P0, formR_psi_P0,
+    formO_chi_P0, G, E, ← sum_pHat_mul_qHat, Fin.sum_univ_three]
+  -- The coefficients of the z_ij agree term by term.  In the coefficient of z₀ the products x_i y_j
+  -- cancel, and the cross terms are ∑_i x_i ∑_j q̂_ij + ∑_j y_j ∑_i p̂_ij = 0.
+  linear_combination polyO .z0 * (polyL (.x 0) * hrow 0 + polyL (.x 1) * hrow 1
+    + polyL (.x 2) * hrow 2 + polyR (.y 0) * hcol 0 + polyR (.y 1) * hcol 1 + polyR (.y 2) * hcol 2)
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/Pruned.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Pruned.lean
new file mode 100644
index 0000000000..ac6930015f
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/Pruned.lean
@@ -0,0 +1,697 @@
+/-
+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.Full
+public import Mathlib.Data.Multiset.Bind
+public import Mathlib.Data.Finset.Piecewise
+
+/-!
+# Pruned tensor evaluation and the calls it makes
+
+The recursion skips children with no requested output strings, reading only precomputed
+leaf encodings. Its values agree with the full recursion on the requested set and vanish
+elsewhere. A call trace records finite recursive calls and passed sets; it is not a machine
+execution or an instruction counter.
+
+The root is always called. At depth zero with an empty request set it is itself a visited
+leaf, although the set of contributing leaves is empty. The leaf characterization therefore
+requires positive depth or a nonempty request set. The value and total-set-size statements
+hold without that qualification.
+
+## Main definitions
+
+* `Pruned.run`, `Pruned.result`, `Pruned.calls`: pruned evaluation and its call trace.
+* `Pruned.Visits`, `Pruned.totalSize`: visited leaves and total size of passed sets.
+* `computeEncoding`: recursive computation of either input encoding.
+
+## Main results
+
+* `Pruned.result_eq_piecewise_full`: agreement on requested strings and zero elsewhere.
+* `Pruned.visits_iff_mem_leaves`: exact visited-leaf characterization with the root exception.
+* `Pruned.totalSize_le`: passed-set total bounded by depth plus one times leaf count.
+* `pruned_spec`: all three properties together for the two input encodings.
+
+## References
+
+Part of [AlmanWilliams2026, Section 2]. Direct mathematical adaptation of
+[Anthropic's pinned formal source](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Sec2).
+Definitions are selectively extracted from that pin's `PaperStatements.lean`; no machine
+semantics or running-time statement is imported. The docstrings below explain the local
+declarations in our own words.
+-/
+
+@[expose] public section
+
+open Finset
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Retain the tails of requested tuples whose first coordinate equals `z`. -/
+def sliceSet {n : ℕ} (S : Finset (OutStr (n + 1))) (z : OutVar) : Finset (OutStr n) :=
+  univ.filter fun w' => (Fin.cons z w' : OutStr (n + 1)) ∈ S
+
+/-- The requests for a child label are the union of slices for output coordinates to which that
+label contributes.
+-/
+def childSet {n : ℕ} (S : Finset (OutStr (n + 1))) (lam : Term) : Finset (OutStr n) :=
+  (univ.filter fun z => lam.Contributes z).biUnion fun z => sliceSet S z
+
+/-- One mathematical call record, pairing its label-sequence position with the request set
+supplied there. The dependent pairs retain the two tuple lengths.
+-/
+structure PrunedCall where
+  /-- The call depth and the terms identifying its vertex.
+-/
+  vertex : Σ k, Vertex k
+  /-- The remaining string length and requested output strings.
+-/
+  passed : Σ n, Finset (OutStr n)
+
+/-- Embed a child call into its parent by prepending the child label to its recorded vertex. -/
+def PrunedCall.under (lam : Term) (c : PrunedCall) : PrunedCall where
+  vertex := ⟨c.vertex.1 + 1, (Fin.cons lam c.vertex.2 : Vertex (c.vertex.1 + 1))⟩
+  passed := c.passed
+
+/-- Evaluate requested outputs from the two supplied leaf-encoding arrays. For each term, form its
+child request set and recurse only when that set is nonempty. Decode the child values and set
+unrequested outputs to zero. The second component records recursive calls and their requested sets
+as a multiset. Each child receives the corresponding slices of the encoding arrays. The root call
+is always recorded, including at depth zero with an empty request set. These are mathematical
+values and call records, without a native execution cost.
+-/
+def Pruned.run : (n : ℕ) → (Leaf n → ℤ) → (Leaf n → ℤ) → Finset (OutStr n) →
+    (OutStr n → ℤ) × Multiset PrunedCall
+  | 0, encA, encB, S =>
+    (S.piecewise (fun _ => encA Fin.elim0 * encB Fin.elim0) 0, {⟨⟨0, Fin.elim0⟩, ⟨0, S⟩⟩})
+  | n + 1, encA, encB, S =>
+    let R : Term → (OutStr n → ℤ) × Multiset PrunedCall := fun lam =>
+      if (childSet S lam).Nonempty then
+        Pruned.run n (sliceAt encA lam) (sliceAt encB lam) (childSet S lam)
+      else (0, 0)
+    (S.piecewise (fun w =>
+        match w 0 with
+        | .z i j => (R (.P i j)).1 (Fin.tail w)
+        | .z0 => ∑ lam, (R lam).1 (Fin.tail w)) 0,
+      ⟨⟨0, Fin.elim0⟩, ⟨n + 1, S⟩⟩ ::ₘ
+        univ.val.bind fun lam => ((R lam).2).map (PrunedCall.under lam))
+
+/-- Project the output values from the pruned recursion and discard the call multiset. -/
+def Pruned.result (n : ℕ) (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) : OutStr n → ℤ :=
+  (Pruned.run n encA encB S).1
+
+/-- Project the multiset of call records, retaining repetitions and the root record. -/
+def Pruned.calls (n : ℕ) (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) : Multiset PrunedCall :=
+  (Pruned.run n encA encB S).2
+
+/-- A leaf is visited when some recorded call has that full-depth vertex. -/
+def Pruned.Visits {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Leaf L) : Prop :=
+  ∃ c ∈ Pruned.calls L encA encB U, c.vertex = ⟨L, τ⟩
+
+/-- Add the cardinalities of the request sets carried by all call records, with multiplicity. -/
+def Pruned.totalSize {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) : ℕ :=
+  ((Pruned.calls L encA encB U).map fun c => c.passed.2.card).sum
+
+/-- Choose the private label at every output coordinate. The resulting leaf is relevant to that
+output tuple and distinguishes it from every other output tuple.
+-/
+def privateLeaf {L : ℕ} (w : OutStr L) : Leaf L := fun ℓ => (w ℓ).privateTerm
+
+/-! ### Section 2.4.1: the encodings -/
+
+/-- Recursively apply the coefficient family `c` along a term string. Each level replaces the
+input array by a weighted sum of its first-letter slices; depth zero returns its unique entry.
+Choosing `phi` or `psi` computes the corresponding shared input encoding.
+-/
+def computeEncoding {α : Type} [Fintype α] (c : Term → α → ℤ) :
+    (L : ℕ) → ((Fin L → α) → ℤ) → Leaf L → ℤ
+  | 0, a, _ => a Fin.elim0
+  | L + 1, a, τ => computeEncoding c L (fun u' => ∑ s, c (τ 0) s * sliceAt a s u') (Fin.tail τ)
+
+/-- Recursive encoding agrees with the closed coefficient-product formula `encodeWith`. -/
+theorem computeEncoding_eq_encodeWith {α : Type} [Fintype α] (c : Term → α → ℤ) {L : ℕ}
+    (a : (Fin L → α) → ℤ) (τ : Leaf L) : computeEncoding c L a τ = encodeWith c τ a := by
+  induction L with
+  | zero => rw [computeEncoding, encodeWith_zero]
+  | succ n ih => rw [computeEncoding, ih, ← encodeWith_cons, Fin.cons_self_tail]
+
+/-- Specializing recursive encoding to `phi` gives the existing left-encoding array. -/
+theorem computeEncoding_phi {L : ℕ} (a : LeftStr L → ℤ) : computeEncoding phi L a = encodingL a :=
+  funext (computeEncoding_eq_encodeWith phi a)
+
+/-- Specializing recursive encoding to `psi` gives the existing right-encoding array. -/
+theorem computeEncoding_psi {L : ℕ} (b : RightStr L → ℤ) : computeEncoding psi L b = encodingR b :=
+  funext (computeEncoding_eq_encodeWith psi b)
+
+/-! ### Section 2.4.2: the sets `S_λ` of step (2) -/
+
+/-- Membership in a slice of a set of output strings.
+-/
+@[simp]
+theorem mem_sliceSet {n : ℕ} (S : Finset (OutStr (n + 1))) (z : OutVar) (w' : OutStr n) :
+    w' ∈ sliceSet S z ↔ (Fin.cons z w' : OutStr (n + 1)) ∈ S := by
+  simp [sliceSet]
+
+/-- An indexed child combines the matching outer slice with the inner slice of the request set. -/
+theorem childSet_P {n : ℕ} (S : Finset (OutStr (n + 1))) (i j : Fin 3) :
+    childSet S (.P i j) = sliceSet S (.z i j) ∪ sliceSet S .z0 := by
+  have hz : (univ.filter fun z => (Term.P i j).Contributes z) = {.z i j, .z0} := by
+    decide +revert
+  rw [childSet, hz, biUnion_insert, singleton_biUnion]
+
+/-- The distinguished child needs only the inner slice of the request set. -/
+theorem childSet_P0 {n : ℕ} (S : Finset (OutStr (n + 1))) :
+    childSet S .P0 = sliceSet S .z0 := by
+  have hz : (univ.filter fun z => Term.P0.Contributes z) = {.z0} := by decide
+  rw [childSet, hz, singleton_biUnion]
+
+/-- Every requested suffix in a relevant output slice belongs to the corresponding child request
+set.
+-/
+theorem sliceSet_subset_childSet {n : ℕ} (S : Finset (OutStr (n + 1))) {lam : Term} {z : OutVar}
+    (h : lam.Contributes z) : sliceSet S z ⊆ childSet S lam :=
+  subset_biUnion_of_mem (fun z => sliceSet S z) (mem_filter.mpr ⟨mem_univ z, h⟩)
+
+/-- A suffix belongs to a child request set precisely when it comes from a requested parent tuple
+whose leading coordinate is relevant to that child label.
+-/
+theorem mem_childSet {n : ℕ} {S : Finset (OutStr (n + 1))} {lam : Term} {w' : OutStr n} :
+    w' ∈ childSet S lam ↔ ∃ w ∈ S, lam.Contributes (w 0) ∧ Fin.tail w = w' := by
+  simp only [childSet, mem_biUnion, mem_filter, mem_univ, true_and, mem_sliceSet]
+  constructor
+  · rintro ⟨z, hz, hw⟩
+    exact ⟨_, hw, by simpa using hz, by simp⟩
+  · rintro ⟨w, hw, hz, rfl⟩
+    exact ⟨w 0, hz, by rwa [Fin.cons_self_tail]⟩
+
+/-! ### Lemma 10, first claim: the values -/
+
+/-- Evaluate a child on its requested suffixes, using the zero array when that child has no
+requests.
+-/
+def Pruned.childResult {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1)))
+    (lam : Term) : OutStr n → ℤ :=
+  if (childSet S lam).Nonempty then
+    Pruned.result n (sliceAt encA lam) (sliceAt encB lam) (childSet S lam)
+  else 0
+
+/-- Unfold the pruned values once, exposing the child arrays used for decoding. -/
+theorem Pruned.result_succ {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) :
+    Pruned.result (n + 1) encA encB S = S.piecewise (fun w =>
+      match w 0 with
+      | .z i j => Pruned.childResult encA encB S (.P i j) (Fin.tail w)
+      | .z0 => ∑ lam, Pruned.childResult encA encB S lam (Fin.tail w)) 0 := by
+  simp only [Pruned.result, Pruned.run, Pruned.childResult, apply_ite Prod.fst]
+
+/-- At a requested tuple, decoding sums child values at its tail over labels relevant to its
+leading coordinate; every unrequested tuple has value zero.
+-/
+theorem Pruned.result_succ_apply {n : ℕ} (encA encB : Leaf (n + 1) → ℤ)
+    (S : Finset (OutStr (n + 1))) (w : OutStr (n + 1)) :
+    Pruned.result (n + 1) encA encB S w = if w ∈ S then
+      ∑ lam : Term with lam.Contributes (w 0), Pruned.childResult encA encB S lam (Fin.tail w)
+    else 0 := by
+  rw [Pruned.result_succ, Finset.piecewise, Term.sum_contributes]
+  rfl
+
+/-- For arbitrary supplied leaf arrays, the pruned result is zero off the request set and is a sum
+of relevant leaf products on that set.
+-/
+theorem Pruned.result_eq_piecewise_sum {n : ℕ} (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) :
+    Pruned.result n encA encB S
+      = S.piecewise (fun w => ∑ τ : Leaf n with Leaf.Contributes τ w, encA τ * encB τ) 0 := by
+  induction n with
+  | zero =>
+    -- The only leaf is the empty string, and it contributes to the empty output string.
+    have hleaf (w : OutStr 0) :
+        (univ.filter fun τ : Leaf 0 => Leaf.Contributes τ w) = {Fin.elim0} :=
+      eq_singleton_iff_unique_mem.mpr
+        ⟨mem_filter.mpr ⟨mem_univ _, fun ℓ => ℓ.elim0⟩, fun _ _ => Subsingleton.elim _ _⟩
+    simp only [Pruned.result, Pruned.run, hleaf, sum_singleton]
+  | succ n ih =>
+    -- The induction hypothesis describes each `C_λ`, also when `S_λ = ∅`.
+    have hC (lam : Term) : Pruned.childResult encA encB S lam
+        = (childSet S lam).piecewise (fun w' =>
+          ∑ τ' : Leaf n with Leaf.Contributes τ' w',
+            encA (Fin.cons lam τ') * encB (Fin.cons lam τ')) 0 := by
+      unfold Pruned.childResult
+      split_ifs with hne
+      · exact ih _ _ _
+      · rw [not_nonempty_iff_eq_empty.mp hne, Finset.piecewise_empty]
+    -- Step (4) reads `C_λ` only at strings of `S_λ`, and a leaf is its first term and the rest.
+    funext w
+    rw [Pruned.result_succ_apply, Finset.piecewise, Leaf.sum_contributes_succ]
+    split_ifs with hw
+    · refine sum_congr rfl fun lam hlam => ?_
+      have hmem : Fin.tail w ∈ childSet S lam :=
+        mem_childSet.mpr ⟨w, hw, (mem_filter.mp hlam).2, rfl⟩
+      rw [hC, Finset.piecewise_eq_of_mem _ _ _ hmem]
+    · rfl
+
+/-- Pruning the two input encodings yields `bilinearProduct` on the requested strings and zero
+elsewhere.
+-/
+theorem Pruned.result_eq_piecewise_bilinearProduct {L : ℕ} (a : LeftStr L → ℤ)
+    (b : RightStr L → ℤ) (U : Finset (OutStr L)) :
+    Pruned.result L (encodingL a) (encodingR b) U = U.piecewise (bilinearProduct a b) 0 :=
+  -- Sum the products of the encoded numbers over the contributing leaves.
+  Pruned.result_eq_piecewise_sum _ _ U
+
+/-- Pruning precomputed input encodings agrees with full evaluation at every requested string and
+is zero elsewhere.
+-/
+theorem Pruned.result_eq_piecewise_full {n : ℕ} (a : LeftStr n → ℤ) (b : RightStr n → ℤ)
+    (S : Finset (OutStr n)) :
+    Pruned.result n (encodingL a) (encodingR b) S = S.piecewise (Full.result n a b) 0 := by
+  rw [Pruned.result_eq_piecewise_bilinearProduct, Full.result_eq_bilinearProduct]
+
+/-! ### Lemma 10, second claim: the calls that are made and the sets passed to them -/
+
+/-- Test relevance for an initial label sequence against the matching prefix of an output tuple.
+Longer label sequences fail the depth condition.
+-/
+def Vertex.Contributes {k L : ℕ} (τ : Vertex k) (w : OutStr L) : Prop :=
+  ∀ (ℓ : Fin k) (h : (ℓ : ℕ) < L), (τ ℓ).Contributes (w ⟨ℓ, h⟩)
+
+/-- At full depth, vertex relevance coincides with the existing leaf-relevance predicate. -/
+theorem Vertex.contributes_iff_leaf {L : ℕ} (τ : Leaf L) (w : OutStr L) :
+    Vertex.Contributes τ w ↔ Leaf.Contributes τ w :=
+  ⟨fun h ℓ => h ℓ ℓ.2, fun h ℓ _ => h ℓ⟩
+
+/-- Decompose relevance of a nonempty vertex into relevance of its head and relevance of its
+tail.
+-/
+theorem Vertex.contributes_cons {k L : ℕ} {lam : Term} {τ : Vertex k} {w : OutStr (L + 1)} :
+    Vertex.Contributes (Fin.cons lam τ : Vertex (k + 1)) w
+      ↔ lam.Contributes (w 0) ∧ Vertex.Contributes τ (Fin.tail w) := by
+  constructor
+  · intro h
+    exact ⟨h 0 (Nat.succ_pos L), fun ℓ hℓ => h ℓ.succ (Nat.succ_lt_succ hℓ)⟩
+  · rintro ⟨h0, h1⟩ ℓ h
+    induction ℓ using Fin.cases with
+    | zero => exact h0
+    | succ i => exact h1 i (Nat.lt_of_succ_lt_succ h)
+
+/-- Obtain a child call multiset from its recursion, or the empty multiset when its request set is
+empty.
+-/
+def Pruned.childCalls {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1)))
+    (lam : Term) : Multiset PrunedCall :=
+  if (childSet S lam).Nonempty then
+    Pruned.calls n (sliceAt encA lam) (sliceAt encB lam) (childSet S lam)
+  else 0
+
+/-- Unfold call recording into the parent record and the embedded records from nonempty children. -/
+theorem Pruned.calls_succ {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) :
+    Pruned.calls (n + 1) encA encB S = ⟨⟨0, Fin.elim0⟩, ⟨n + 1, S⟩⟩ ::ₘ
+      univ.val.bind fun lam => (Pruned.childCalls encA encB S lam).map (.under lam) := by
+  simp only [Pruned.calls, Pruned.run, Pruned.childCalls, apply_ite Prod.snd]
+
+/-- Membership in the positive-depth call multiset means being the root record or an embedded call
+of some nonempty child.
+-/
+theorem Pruned.mem_calls_succ {n : ℕ} {encA encB : Leaf (n + 1) → ℤ}
+    {S : Finset (OutStr (n + 1))} {c : PrunedCall} :
+    c ∈ Pruned.calls (n + 1) encA encB S ↔
+      c = ⟨⟨0, Fin.elim0⟩, ⟨n + 1, S⟩⟩
+        ∨ ∃ lam : Term, (childSet S lam).Nonempty
+            ∧ ∃ c' ∈ Pruned.calls n (sliceAt encA lam) (sliceAt encB lam) (childSet S lam),
+                c = c'.under lam := by
+  rw [Pruned.calls_succ, Multiset.mem_cons, Multiset.mem_bind]
+  refine or_congr Iff.rfl ⟨?_, ?_⟩
+  · rintro ⟨lam, -, h⟩
+    obtain ⟨c', hc', rfl⟩ := Multiset.mem_map.mp h
+    unfold Pruned.childCalls at hc'
+    split_ifs at hc' with hne
+    · exact ⟨lam, hne, c', hc', rfl⟩
+    · simp at hc'
+  · rintro ⟨lam, hne, c', hc', rfl⟩
+    refine ⟨lam, mem_univ lam, Multiset.mem_map.mpr ⟨c', ?_, rfl⟩⟩
+    rwa [Pruned.childCalls, ite_eq_left hne]
+
+/-- A call below the child `λ` is at the vertex `τ` of depth `k + 1` exactly if `λ` is the first
+term of `τ` and, seen from the child, the call is at the rest of `τ`.
+-/
+private theorem PrunedCall.vertex_under_eq_iff {lam : Term} {c : PrunedCall} {k : ℕ}
+    {τ : Vertex (k + 1)} :
+    (c.under lam).vertex = ⟨k + 1, τ⟩ ↔ lam = τ 0 ∧ c.vertex = ⟨k, Fin.tail τ⟩ := by
+  obtain ⟨⟨k', τ'⟩, T⟩ := c
+  constructor
+  · intro h
+    simp only [PrunedCall.under, Sigma.mk.injEq, Nat.add_right_cancel_iff] at h
+    obtain ⟨rfl, h⟩ := h
+    obtain rfl := eq_of_heq h
+    simp
+  · rintro ⟨rfl, h⟩
+    simp only [Sigma.mk.injEq] at h
+    obtain ⟨rfl, h⟩ := h
+    obtain rfl := eq_of_heq h
+    simp [PrunedCall.under]
+
+/-- A vertex is called when its depth and label tuple occur in the recorded call multiset. -/
+def Pruned.Called {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Vertex k) :
+    Prop :=
+  ∃ c ∈ Pruned.calls L encA encB U, c.vertex = ⟨k, τ⟩
+
+/-- The root is called.
+-/
+theorem Pruned.called_root {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L))
+    (τ : Vertex 0) : Pruned.Called encA encB U τ := by
+  obtain rfl : τ = Fin.elim0 := Subsingleton.elim _ _
+  cases L with
+  | zero => exact ⟨_, Multiset.mem_singleton_self _, rfl⟩
+  | succ n => exact ⟨_, Pruned.mem_calls_succ.mpr (.inl rfl), rfl⟩
+
+/-- A non-root vertex is called exactly when its leading child has requests and the tail vertex is
+called within that child.
+-/
+theorem Pruned.called_succ {n k : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1)))
+    (τ : Vertex (k + 1)) :
+    Pruned.Called encA encB S τ ↔ (childSet S (τ 0)).Nonempty ∧
+      Pruned.Called (sliceAt encA (τ 0)) (sliceAt encB (τ 0)) (childSet S (τ 0)) (Fin.tail τ) := by
+  constructor
+  · rintro ⟨c, hc, hcτ⟩
+    rcases Pruned.mem_calls_succ.mp hc with rfl | ⟨lam, hne, c', hc', rfl⟩
+    · exact absurd (congrArg Sigma.fst hcτ) (by simp)
+    · obtain ⟨rfl, hc'τ⟩ := PrunedCall.vertex_under_eq_iff.mp hcτ
+      exact ⟨hne, c', hc', hc'τ⟩
+  · rintro ⟨hne, c', hc', hc'τ⟩
+    exact ⟨c'.under (τ 0), Pruned.mem_calls_succ.mpr (.inr ⟨τ 0, hne, c', hc', rfl⟩),
+      PrunedCall.vertex_under_eq_iff.mpr ⟨rfl, hc'τ⟩⟩
+
+/-- Existence of a requested tuple relevant to a cons vertex reduces to the same question for the
+tail vertex and the child request set.
+-/
+private theorem exists_contributes_childSet {n k : ℕ} (S : Finset (OutStr (n + 1)))
+    (τ : Vertex (k + 1)) :
+    (∃ w' ∈ childSet S (τ 0), Vertex.Contributes (Fin.tail τ) w')
+      ↔ ∃ w ∈ S, Vertex.Contributes τ w := by
+  have hcons (w : OutStr (n + 1)) : Vertex.Contributes τ w
+      ↔ (τ 0).Contributes (w 0) ∧ Vertex.Contributes (Fin.tail τ) (Fin.tail w) := by
+    rw [← Vertex.contributes_cons, Fin.cons_self_tail]
+  constructor
+  · rintro ⟨w', hw', hτ'⟩
+    obtain ⟨w, hw, hz, rfl⟩ := mem_childSet.mp hw'
+    exact ⟨w, hw, (hcons w).mpr ⟨hz, hτ'⟩⟩
+  · rintro ⟨w, hw, hτ⟩
+    exact ⟨_, mem_childSet.mpr ⟨w, hw, ((hcons w).mp hτ).1, rfl⟩, ((hcons w).mp hτ).2⟩
+
+/-- For vertices within the recursion depth, being called is equivalent to being the root or being
+relevant to at least one requested tuple.
+-/
+theorem Pruned.called_iff_root_or {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L))
+    (hkL : k ≤ L) (τ : Vertex k) :
+    Pruned.Called encA encB U τ ↔ k = 0 ∨ ∃ w ∈ U, Vertex.Contributes τ w := by
+  induction L generalizing k with
+  | zero =>
+    obtain rfl : k = 0 := by omega
+    exact iff_of_true (Pruned.called_root encA encB U τ) (.inl rfl)
+  | succ n ih =>
+    cases k with
+    | zero => exact iff_of_true (Pruned.called_root encA encB U τ) (.inl rfl)
+    | succ k =>
+      have ihτ := ih (sliceAt encA (τ 0)) (sliceAt encB (τ 0)) (childSet U (τ 0))
+        (Nat.le_of_succ_le_succ hkL) (Fin.tail τ)
+      rw [Pruned.called_succ, ← exists_contributes_childSet]
+      constructor
+      · rintro ⟨⟨w', hw'⟩, hcalled⟩
+        rcases ihτ.mp hcalled with rfl | hτ'
+        · -- The child `λ` itself, as a vertex at depth 0, contributes to every string of `U_λ`.
+          exact .inr ⟨w', hw', fun ℓ => ℓ.elim0⟩
+        · exact .inr hτ'
+      · rintro (hk | ⟨w', hw', hτ'⟩)
+        · exact absurd hk (Nat.succ_ne_zero k)
+        · exact ⟨⟨w', hw'⟩, ihτ.mpr (.inr ⟨w', hw', hτ'⟩)⟩
+
+/-- Away from the empty-request root exception, a vertex within the recursion depth is called
+exactly when some requested tuple is relevant to it. The hypothesis `hk` admits every
+positive-depth vertex and also admits the root when requests are nonempty.
+-/
+theorem Pruned.called_iff {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L))
+    (hk : 1 ≤ k ∨ U.Nonempty) (hkL : k ≤ L) (τ : Vertex k) :
+    Pruned.Called encA encB U τ ↔ ∃ w ∈ U, Vertex.Contributes τ w := by
+  rw [Pruned.called_iff_root_or _ _ U hkL τ]
+  constructor
+  · rintro (rfl | h)
+    · obtain ⟨w, hw⟩ := hk.resolve_left (by omega)
+      exact ⟨w, hw, fun ℓ => ℓ.elim0⟩
+    · exact h
+  · exact Or.inr
+
+/-- A call at depth `k` is passed strings of length `L - k`.
+-/
+theorem Pruned.depth_add_length {L : ℕ} {encA encB : Leaf L → ℤ} {U : Finset (OutStr L)}
+    {c : PrunedCall} (hc : c ∈ Pruned.calls L encA encB U) : c.vertex.1 + c.passed.1 = L := by
+  induction L generalizing c with
+  | zero =>
+    obtain rfl := Multiset.mem_singleton.mp hc
+    rfl
+  | succ n ih =>
+    rcases Pruned.mem_calls_succ.mp hc with rfl | ⟨lam, -, c', hc', rfl⟩
+    · exact Nat.zero_add _
+    · have hlen := ih hc'
+      change c'.vertex.1 + 1 + c'.passed.1 = n + 1
+      omega
+
+/-- `w'` is the suffix of `w` that is left when the first `k` variables are removed.
+-/
+def IsSuffixFrom {n L : ℕ} (k : ℕ) (w' : OutStr n) (w : OutStr L) : Prop :=
+  ∀ (i : Fin n) (hi : k + (i : ℕ) < L), w' i = w ⟨k + i, hi⟩
+
+/-- Removing no variable leaves the string as it is.
+-/
+private theorem isSuffixFrom_zero {n : ℕ} (w' w : OutStr n) : IsSuffixFrom 0 w' w ↔ w' = w := by
+  have hidx (i : Fin n) (hi : 0 + (i : ℕ) < n) : (⟨0 + i, hi⟩ : Fin n) = i :=
+    Fin.ext (Nat.zero_add _)
+  constructor
+  · intro h
+    funext i
+    rw [h i (by simp), hidx]
+  · rintro rfl i hi
+    rw [hidx]
+
+/-- Removing `k + 1` variables is removing the first variable and then `k` more.
+-/
+private theorem isSuffixFrom_succ {n L k : ℕ} {w' : OutStr n} {w : OutStr (L + 1)} :
+    IsSuffixFrom (k + 1) w' w ↔ IsSuffixFrom k w' (Fin.tail w) := by
+  have hidx (i : Fin n) (h₁ : k + 1 + (i : ℕ) < L + 1) (h₂ : k + (i : ℕ) < L) :
+      w ⟨k + 1 + i, h₁⟩ = Fin.tail w ⟨k + i, h₂⟩ :=
+    congrArg w (Fin.ext (by simp only [Fin.val_succ]; omega))
+  exact ⟨fun h i hi => (h i (by omega)).trans (hidx i _ hi),
+    fun h i hi => (h i (by omega)).trans (hidx i hi _).symm⟩
+
+/-- The set passed to the root is `U`, and the root contributes to every string.
+-/
+private theorem mem_iff_root {L : ℕ} (U : Finset (OutStr L)) (w' : OutStr L) :
+    w' ∈ U ↔ ∃ w ∈ U, Vertex.Contributes (Fin.elim0 : Vertex 0) w ∧ IsSuffixFrom 0 w' w := by
+  simp only [isSuffixFrom_zero]
+  exact ⟨fun h => ⟨w', h, fun ℓ => ℓ.elim0, rfl⟩, fun ⟨_, hw, _, h⟩ => h ▸ hw⟩
+
+/-- A recorded call receives exactly the suffixes of original requests relevant to its vertex. Its
+recorded remaining length and depth identify the suffix position.
+-/
+theorem Pruned.mem_passed_iff {L : ℕ} {encA encB : Leaf L → ℤ} {U : Finset (OutStr L)}
+    {c : PrunedCall} (hc : c ∈ Pruned.calls L encA encB U) (w' : OutStr c.passed.1) :
+    w' ∈ c.passed.2 ↔
+      ∃ w ∈ U, Vertex.Contributes c.vertex.2 w ∧ IsSuffixFrom c.vertex.1 w' w := by
+  induction L generalizing c with
+  | zero =>
+    obtain rfl := Multiset.mem_singleton.mp hc
+    exact mem_iff_root U w'
+  | succ n ih =>
+    rcases Pruned.mem_calls_succ.mp hc with rfl | ⟨lam, -, c', hc', rfl⟩
+    · exact mem_iff_root U w'
+    · -- A vertex below the child `λ`: the induction hypothesis for `S_λ`, whose strings are the
+      -- rests of the strings of `U` to whose first variable `λ` contributes.
+      refine (ih hc' w').trans ⟨?_, ?_⟩
+      · rintro ⟨_, hw₁, hτ, hsuffix⟩
+        obtain ⟨w, hw, hz, rfl⟩ := mem_childSet.mp hw₁
+        exact ⟨w, hw, Vertex.contributes_cons.mpr ⟨hz, hτ⟩, isSuffixFrom_succ.mpr hsuffix⟩
+      · rintro ⟨w, hw, hτ, hsuffix⟩
+        obtain ⟨hz, hτ'⟩ := Vertex.contributes_cons.mp hτ
+        exact ⟨Fin.tail w, mem_childSet.mpr ⟨w, hw, hz, rfl⟩, hτ', isSuffixFrom_succ.mp hsuffix⟩
+
+/-- A leaf is visited exactly when it is the zero-depth root or contributes to a request. This
+includes the empty request set without an exceptional hypothesis.
+-/
+theorem Pruned.visits_iff_root_or_mem_leaves {L : ℕ} (encA encB : Leaf L → ℤ)
+    (U : Finset (OutStr L)) (τ : Leaf L) :
+    Pruned.Visits encA encB U τ ↔ L = 0 ∨ τ ∈ leaves U := by
+  change Pruned.Called encA encB U τ ↔ _
+  simpa only [mem_leaves, Vertex.contributes_iff_leaf] using
+    Pruned.called_iff_root_or encA encB U (le_refl L) τ
+
+/-- With positive depth or nonempty requests, the visited-leaf set is exactly `leaves U`. The
+unconditional root case is given separately by `Pruned.visits_iff_root_or_mem_leaves`.
+-/
+theorem Pruned.visits_iff_mem_leaves {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L))
+    (h : 0 < L ∨ U.Nonempty) (τ : Leaf L) : Pruned.Visits encA encB U τ ↔ τ ∈ leaves U :=
+  -- A leaf is a vertex at depth `L`.
+  (Pruned.called_iff encA encB U h le_rfl τ).trans
+    (by simp only [mem_leaves, Vertex.contributes_iff_leaf])
+
+/-! ### Lemma 10, third claim: the total size of the sets passed -/
+
+/-- Membership in a positive-depth relevant-leaf set reduces to membership of the tail in the
+child relevant-leaf set.
+-/
+theorem mem_leaves_succ {n : ℕ} {S : Finset (OutStr (n + 1))} {τ : Leaf (n + 1)} :
+    τ ∈ leaves S ↔ Fin.tail τ ∈ leaves (childSet S (τ 0)) := by
+  rw [mem_leaves, mem_leaves]
+  constructor
+  · rintro ⟨w, hw, hcon⟩
+    obtain ⟨h0, h1⟩ := Leaf.contributes_succ.mp hcon
+    exact ⟨Fin.tail w, mem_childSet.mpr ⟨w, hw, h0, rfl⟩, h1⟩
+  · rintro ⟨w', hw', h1⟩
+    obtain ⟨w, hw, h0, rfl⟩ := mem_childSet.mp hw'
+    exact ⟨w, hw, Leaf.contributes_succ.mpr ⟨h0, h1⟩⟩
+
+/-- Count relevant leaves by summing the relevant-leaf counts of all children; distinct leading
+labels keep these families disjoint.
+-/
+theorem card_leaves_succ {n : ℕ} (S : Finset (OutStr (n + 1))) :
+    (leaves S).card = ∑ lam, (leaves (childSet S lam)).card := by
+  rw [card_eq_sum_card_fiberwise (f := fun τ : Leaf (n + 1) => τ 0) (t := univ)
+    (fun _ _ => mem_coe.mpr (mem_univ _))]
+  refine sum_congr rfl fun lam _ => ?_
+  rw [← card_image_of_injective (leaves (childSet S lam))
+    (Fin.cons_right_injective (α := fun _ : Fin (n + 1) => Term) lam)]
+  congr 1
+  ext τ
+  simp only [mem_filter, mem_image]
+  constructor
+  · rintro ⟨hτ, rfl⟩
+    exact ⟨Fin.tail τ, mem_leaves_succ.mp hτ, Fin.cons_self_tail τ⟩
+  · rintro ⟨τ', hτ', rfl⟩
+    refine ⟨mem_leaves_succ.mpr ?_, Fin.cons_zero _ _⟩
+    simpa using hτ'
+
+/-- Different output strings have different private leaves.
+-/
+theorem privateLeaf_injective {L : ℕ} : Function.Injective (privateLeaf (L := L)) :=
+  have hterm : Function.Injective OutVar.privateTerm := by decide
+  fun _ _ h => funext fun ℓ => hterm (congrFun h ℓ)
+
+/-- The private-leaf injection bounds the number of requested tuples by the number of their
+relevant leaves.
+-/
+theorem card_le_card_leaves {n : ℕ} (S : Finset (OutStr n)) : S.card ≤ (leaves S).card := by
+  refine card_le_card_of_injOn privateLeaf (fun w hw => ?_) privateLeaf_injective.injOn
+  exact mem_coe.mpr (mem_leaves.mpr
+    ⟨w, hw, fun _ => (Term.contributes_iff _ _).mpr (.inr rfl)⟩)
+
+/-- The total size of the sets passed to the calls at depth `k` in a list of calls.
+-/
+private def sizeAt (s : Multiset PrunedCall) (k : ℕ) : ℕ :=
+  ((s.filter fun c => c.vertex.1 = k).map fun c => c.passed.2.card).sum
+
+/-- The size at depth `k` of a list of calls with one more call.
+-/
+private theorem sizeAt_cons (c : PrunedCall) (s : Multiset PrunedCall) (k : ℕ) :
+    sizeAt (c ::ₘ s) k
+      = (if c.vertex.1 = k then c.passed.2.card else 0) + sizeAt s k := by
+  unfold sizeAt
+  rw [Multiset.filter_cons]
+  split_ifs <;> simp
+
+/-- The size at depth `k` of the lists of calls of the ten children together.
+-/
+private theorem sizeAt_bind (f : Term → Multiset PrunedCall) (k : ℕ) :
+    sizeAt (univ.val.bind f) k = ∑ lam, sizeAt (f lam) k := by
+  unfold sizeAt
+  rw [Multiset.filter_bind, Multiset.map_bind, Multiset.sum_bind]
+  rfl
+
+/-- Seen from one level higher, the calls at depth `k` are at depth `k + 1`.
+-/
+private theorem sizeAt_under_succ (lam : Term) (s : Multiset PrunedCall) (k : ℕ) :
+    sizeAt (s.map (PrunedCall.under lam)) (k + 1) = sizeAt s k := by
+  unfold sizeAt
+  rw [Multiset.filter_map, Multiset.map_map]
+  rw [Multiset.filter_congr (q := fun c => c.vertex.1 = k) (by simp [PrunedCall.under])]
+  rfl
+
+/-- Seen from one level higher, no call is at depth `0`.
+-/
+private theorem sizeAt_under_zero (lam : Term) (s : Multiset PrunedCall) :
+    sizeAt (s.map (PrunedCall.under lam)) 0 = 0 := by
+  unfold sizeAt
+  rw [Multiset.filter_map, Multiset.filter_eq_nil.mpr (by simp [PrunedCall.under])]
+  rfl
+
+/-- The total size of the sets passed is the sum, over the depths, of the sizes at each depth.
+-/
+private theorem sum_sizeAt (s : Multiset PrunedCall) (N : ℕ) (h : ∀ c ∈ s, c.vertex.1 < N) :
+    (s.map fun c => c.passed.2.card).sum = ∑ k ∈ range N, sizeAt s k := by
+  induction s using Multiset.induction_on with
+  | empty => simp [sizeAt]
+  | cons c s ih =>
+    simp only [sizeAt_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_distrib]
+    rw [ih fun c' hc' => h c' (Multiset.mem_cons_of_mem hc'), sum_ite_eq,
+      ite_eq_left (mem_range.mpr (h c (Multiset.mem_cons_self c s)))]
+
+/-- At any fixed depth, the sum of all passed request-set cardinalities is bounded by the root
+request set's relevant-leaf count.
+-/
+theorem Pruned.sum_card_passed_le {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (k : ℕ) :
+    (((Pruned.calls L encA encB U).filter fun c => c.vertex.1 = k).map fun c => c.passed.2.card).sum
+      ≤ (leaves U).card := by
+  -- The paper's injection (vertex, suffix) ↦ leaf, organised as an induction on `L`: the strings
+  -- passed to the root inject into `leaves(U)`, and the calls at depth `k + 1` are the calls at
+  -- depth `k` of the children `λ`, whose leaves, with `λ` put in front, are pairwise disjoint parts
+  -- of `leaves(U)`.
+  change sizeAt (Pruned.calls L encA encB U) k ≤ _
+  induction L generalizing k with
+  | zero =>
+    have hcalls : Pruned.calls 0 encA encB U = ⟨⟨0, Fin.elim0⟩, ⟨0, U⟩⟩ ::ₘ 0 := rfl
+    rw [hcalls, sizeAt_cons]
+    split_ifs
+    · simpa [sizeAt] using card_le_card_leaves U
+    · simp [sizeAt]
+  | succ n ih =>
+    rw [Pruned.calls_succ, sizeAt_cons, sizeAt_bind]
+    cases k with
+    | zero =>
+      simp only [sizeAt_under_zero, sum_const_zero, ite_true, add_zero]
+      exact card_le_card_leaves U
+    | succ k =>
+      simp only [sizeAt_under_succ]
+      rw [ite_eq_right (by simp), zero_add, card_leaves_succ]
+      refine sum_le_sum fun lam _ => ?_
+      unfold Pruned.childCalls
+      split_ifs
+      · exact ih _ _ _ _
+      · simp [sizeAt]
+
+/-- The sum of the cardinalities of all passed request sets is at most `(L + 1) * (leaves
+U).card`.
+-/
+theorem Pruned.totalSize_le {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) :
+    Pruned.totalSize encA encB U ≤ (L + 1) * (leaves U).card := by
+  have hdepth : ∀ c ∈ Pruned.calls L encA encB U, c.vertex.1 < L + 1 :=
+    fun c hc => by have := Pruned.depth_add_length hc; omega
+  rw [Pruned.totalSize, sum_sizeAt _ (L + 1) hdepth]
+  calc ∑ k ∈ range (L + 1), sizeAt (Pruned.calls L encA encB U) k
+      ≤ ∑ _k ∈ range (L + 1), (leaves U).card :=
+        sum_le_sum fun k _ => Pruned.sum_card_passed_le _ _ U k
+    _ = (L + 1) * (leaves U).card := by simp
+
+/-- Combine value correctness, the visited-leaf characterization and the passed-set cardinality
+bound for the two input encodings. Values and the set-size bound apply at every depth and request
+set. The leaf equivalence excludes the empty zero-depth root;
+`Pruned.visits_iff_root_or_mem_leaves` gives the unconditional alternative for that case.
+-/
+theorem pruned_spec {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (U : Finset (OutStr L)) :
+    Pruned.result L (encodingL a) (encodingR b) U = U.piecewise (bilinearProduct a b) 0
+      ∧ (0 < L ∨ U.Nonempty →
+          ∀ τ : Leaf L, Pruned.Visits (encodingL a) (encodingR b) U τ ↔ τ ∈ leaves U)
+      ∧ Pruned.totalSize (encodingL a) (encodingR b) U ≤ (L + 1) * (leaves U).card :=
+  ⟨Pruned.result_eq_piecewise_bilinearProduct a b U, Pruned.visits_iff_mem_leaves _ _ U,
+    Pruned.totalSize_le _ _ U⟩
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage
diff --git a/ComplexityTests/Schonhage.lean b/ComplexityTests/Schonhage.lean
new file mode 100644
index 0000000000..a70da4e167
--- /dev/null
+++ b/ComplexityTests/Schonhage.lean
@@ -0,0 +1,100 @@
+/-
+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.Identity
+import Complexity.Algorithms.MatrixMultiplication.Schonhage.Pruned
+
+/-! Concrete tensor evaluations, signed cancellation and pruning boundary cases. -/
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+namespace SchonhageTests
+
+private def left : LeftStr 1 → ℤ := fun u =>
+  match u 0 with
+  | .x i => ![1, 2, 3] i
+  | .p i j => !![4, 5; 6, 7] i j
+
+private def right : RightStr 1 → ℤ := fun v =>
+  match v 0 with
+  | .y j => ![8, 9, 10] j
+  | .q i j => !![11, 12; 13, 14] i j
+
+-- The negative tenth term cancels the unwanted outer products in the inner output.
+example : Full.multipliedAt 1 left right ![.P0] = (-6, 27) := by decide
+
+example : Full.result 1 left right ![.z0] = 280 := by decide
+
+example : Full.result 1 left right ![.z 0 0] = 95 := by decide
+
+example : Full.result 1 left right ![.z 2 2] = 30 := by decide
+
+-- Unrestricted outer outputs include error terms: 95 is not the wanted product 1 * 8.
+example : Full.result 1 left right ![.z 0 0] ≠ 1 * 8 := by decide
+
+example : coefficient (.x 0) (.y 0) .z0 = 0 := by decide
+
+example : coefficient (.p 0 1) (.q 0 1) .z0 = 1 := by decide
+
+example : coefficient (.p 0 1) (.q 1 0) .z0 = 0 := by decide
+
+example : coefficient (.x 0) (.q 0 0) (.z 0 0) = 1 := by decide
+
+private def outerQuery : Finset (OutStr 1) := {![.z 0 0]}
+
+private def innerQuery : Finset (OutStr 1) := {![.z0]}
+
+example : Pruned.result 1 (encodingL left) (encodingR right) outerQuery ![.z 0 0] = 95 := by
+  decide
+
+example : Pruned.result 1 (encodingL left) (encodingR right) outerQuery ![.z0] = 0 := by
+  decide
+
+example : (leaves outerQuery).card = 1 := by decide
+
+example : (Pruned.calls 1 (encodingL left) (encodingR right) outerQuery).card = 2 := by
+  decide
+
+example : Pruned.totalSize (encodingL left) (encodingR right) outerQuery = 2 := by decide
+
+example : (leaves innerQuery).card = 10 := by decide
+
+example : Pruned.totalSize (encodingL left) (encodingR right) innerQuery = 11 := by decide
+
+-- The shared contributing leaf of these two outputs is included only once.
+private def mixedQuery : Finset (OutStr 1) := {![.z 0 0], ![.z0]}
+
+example : (leaves mixedQuery).card = 10 := by decide
+
+example : (Pruned.calls 1 (encodingL left) (encodingR right) mixedQuery).card = 11 := by
+  decide
+
+example : Pruned.totalSize (encodingL left) (encodingR right) mixedQuery = 12 := by decide
+
+example : Pruned.result 1 (encodingL left) (encodingR right) ∅ ![.z0] = 0 := by decide
+
+example : (Pruned.calls 1 (encodingL left) (encodingR right) ∅).card = 1 := by decide
+
+example : Pruned.totalSize (encodingL left) (encodingR right) ∅ = 0 := by decide
+
+-- Below a two-level query, the outer level keeps one child and the inner one keeps ten.
+example : Pruned.result 2 (fun _ => 3) (fun _ => -4) {![.z 1 2, .z0]}
+    ![.z 1 2, .z0] = -120 := by decide
+
+example : Pruned.totalSize (fun _ : Leaf 2 => 3) (fun _ => -4) {![.z 1 2, .z0]} = 12 := by
+  decide
+
+example : Pruned.result 0 (fun _ => -3) (fun _ => 7) {Fin.elim0} Fin.elim0 = -21 := by
+  decide
+
+-- The unqualified visited-leaf equivalence fails at the empty, zero-depth root.
+example : Pruned.Visits (fun _ : Leaf 0 => 1) (fun _ => 1) ∅ Fin.elim0 ∧
+    Fin.elim0 ∉ leaves (∅ : Finset (OutStr 0)) := by
+  constructor
+  · exact (Pruned.visits_iff_root_or_mem_leaves _ _ ∅ Fin.elim0).mpr (.inl rfl)
+  · simp [leaves]
+
+end SchonhageTests
diff --git a/NOTICE b/NOTICE
index e48c2ecb6c..5fb9b6c145 100644
--- a/NOTICE
+++ b/NOTICE
@@ -1,5 +1,6 @@
-The 3SUM/Exact Triangle reductions, their finite counting lemmas and native matrix builder in
+The 3SUM/Exact Triangle reductions, finite counting/tensor lemmas and native matrix builder in
 Complexity/Algorithms/ExactTriangle/{Defs,Weights,Lopsided,Hashing,Splitting,Witnesses}.lean,
+Complexity/Algorithms/MatrixMultiplication/Schonhage/,
 Complexity/Algorithms/ThreeSum/,
 Complexity/Algorithms/WordRAM/ThreeSum/,
 Complexity/Foundations/Data/Finset/{Average,Quotient}.lean,
diff --git a/ROADMAP.md b/ROADMAP.md
index 2ae3bfeb3c..cf10317339 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -424,8 +424,11 @@ each statement against the numbered result. Organize modules by subject, not cha
   ordinary distinct-position inputs and explicit size bounds. The finite lopsided matrix/counting
   interface ([#1438]) adds padding, detection and signed digit reconstruction. Modular counting
   and the selected-prime false-positive bound ([#1442]), finite residue/chunk/piece splitting and
-  witness recovery ([#1447]) are proved mathematically. It still needs tensor/sparse-query programs,
-  native Chan–He preprocessing, the reduction host, the fast Exact Triangle solver and full
+  witness recovery ([#1447]) are proved mathematically. The tensor identity, full recursion,
+  shared encodings and pruned-evaluation core ([#1459]) include exact visited-leaf and passed-set
+  bounds, with the empty zero-depth root handled explicitly. It still needs tiling and sparse
+  leaf bounds, native tensor/sparse-query programs, native Chan–He preprocessing, the reduction
+  host, the fast Exact Triangle solver and full
   input/time/width/asymptotic composition, then the improved Section 4 route to exponent 1.9992;
   size-based width
   selection with an input-fit guarantee and explicit overhead; expected-time rules for unbounded
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 1023dc2cb9..153abe289b 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -193,7 +193,15 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   `Algorithms/ExactTriangle/{Splitting,Witnesses}.lean` adapts the complete finite splitting and
   witness recovery component ([#1447](https://github.com/cslib-community/complexitylib/issues/1447)),
   using the existing matrices, lopsided graph and `Set.EqOn` answer API. Computable integer parameters
-  retain the source's exact real floor/ceiling specifications through checked bridges. The existing
+  retain the source's exact real floor/ceiling specifications through checked bridges.
+  `Algorithms/MatrixMultiplication/Schonhage/` adapts the tensor-recursion core from the same pin's
+  `Sec2/{Lemma6,Recursion,Lemma7_8,Lemma10}.lean`: the ten-term polynomial identity with explicit
+  error, full evaluation, shared encodings, pruned values, visited leaves and passed-set totals.
+  Its pure finite recursion traces are not native machine semantics or charged instruction costs.
+  The zero-depth empty-query root exception is explicit, with an unconditional root-or-leaf API.
+  See [#1459](https://github.com/cslib-community/complexitylib/issues/1459); tiling/sparse leaf bounds
+  remain in #1394.
+  The existing
   signed and unsigned APIs were reused; no source machine or separate run semantics were copied.
   Tensor/sparse query programs, the full reduction host, native Chan–He preprocessing, fast Exact
   Triangle and full input/time/width/asymptotic composition remain in