diff --git a/Complexity.lean b/Complexity.lean
index cfa5796f1..11b99ecfe 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -32,6 +32,7 @@ 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.Batch
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Full
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Identity
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Layout
@@ -111,6 +112,17 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Algorithms.WordRAM.Karger.Graph
 public import Complexity.Algorithms.WordRAM.KargerMinCut
 public import Complexity.Algorithms.WordRAM.KargerStein
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Cell
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Controller
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Copy
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Exec
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Flat
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Forms
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Header
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Input
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Meaning
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Stage
 public import Complexity.Algorithms.WordRAM.NatClog
 public import Complexity.Algorithms.WordRAM.NatLog
 public import Complexity.Algorithms.WordRAM.NatSqrt
diff --git a/Complexity/Algorithms/MatrixMultiplication/Schonhage/CoordinateTransform.lean b/Complexity/Algorithms/MatrixMultiplication/Schonhage/CoordinateTransform.lean
new file mode 100644
index 000000000..eb1392c7d
--- /dev/null
+++ b/Complexity/Algorithms/MatrixMultiplication/Schonhage/CoordinateTransform.lean
@@ -0,0 +1,191 @@
+/-
+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 Complexity.Foundations.Algebra.FiniteMagnitude
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.Linarith
+
+/-!
+# Shared coordinate transforms in flat arrays
+
+After `j` coordinates have been transformed, the array has `10^j * 7^k` entries, where
+`j + k = L`. Its entry at `(p, r)` sums the input entries with suffix `r`, weighting their
+prefixes by the product of the selected coefficients. The next coordinate transform computes
+each new entry from seven entries of this shared array. It does not independently enumerate
+all input entries for every final leaf.
+
+## Main definitions
+
+* `CoordinateTransform.weight`: product of coefficients along the transformed prefix.
+* `CoordinateTransform.value`: prefix expansion at a mixed-radix array position.
+
+## Main results
+
+* `CoordinateTransform.value_step`: the seven-to-ten shared coordinate update.
+* `CoordinateTransform.stageSize_le`: every stage has at most `10^L` entries.
+
+## References
+
+An iterative implementation invariant for [AlmanWilliams2026, Section 2.4.1]. The coefficients
+are those of the existing encoding API, adapted from Anthropic, PBC's formal source at
+`16a5ce41304fcdaea4e0be7c132e1c361dc26da5`. This module defines mathematical arrays and sums,
+not a separate machine or an instruction-counting semantics.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform
+
+open Finset
+
+/-- Product of `j` coefficients, reading prefix digits from least significant to most
+significant. Values at noncanonical indices are harmless; clients use indices below the powers. -/
+def weight (c : ℕ → ℕ → ℤ) : ℕ → ℕ → ℕ → ℤ
+  | 0, _, _ => 1
+  | j + 1, p, v => weight c j (p / 10) (v / 7) * c (p % 10) (v % 7)
+
+/-- Value at transformed prefix `p` and original suffix `r`. The remaining suffix has `k`
+base-seven digits; the original input index is `v * 7^k + r`. -/
+def value (c : ℕ → ℕ → ℤ) (j k : ℕ) (a : ℕ → ℤ) (p r : ℕ) : ℤ :=
+  ∑ v ∈ range (7 ^ j), weight c j p v * a (v * 7 ^ k + r)
+
+private theorem sum_blocks (m n : ℕ) (f : ℕ → ℤ) :
+    ∑ i ∈ range (m * n), f i = ∑ q ∈ range m, ∑ s ∈ range n, f (q * n + s) := by
+  induction m with
+  | zero => simp
+  | succ m ih =>
+    rw [Nat.succ_mul, sum_range_add, ih, sum_range_succ]
+
+/-- At the initial stage no coordinate is transformed, so the entry is the input itself. -/
+theorem value_zero (c : ℕ → ℕ → ℤ) (k : ℕ) (a : ℕ → ℤ) (p r : ℕ) :
+    value c 0 k a p r = a r := by
+  simp [value, weight]
+
+/-- The next array entry uses seven already shared values. This is the exact algebraic
+invariant of the mixed-radix native loop. -/
+theorem value_step (c : ℕ → ℕ → ℤ) (j k : ℕ) (a : ℕ → ℤ) (p r : ℕ)
+    {t : ℕ} (ht : t < 10) :
+    value c (j + 1) k a (p * 10 + t) r =
+      ∑ s ∈ range 7, c t s * value c j (k + 1) a p (s * 7 ^ k + r) := by
+  simp only [value, pow_succ, sum_blocks]
+  rw [sum_comm]
+  refine sum_congr rfl fun s hs => ?_
+  have hs7 := mem_range.mp hs
+  simp only [mul_sum]
+  refine sum_congr rfl fun q _ => ?_
+  have hp : (p * 10 + t) / 10 = p := by omega
+  have hq : (q * 7 + s) / 7 = q := by omega
+  simp only [weight, hp, hq, Nat.add_mod, Nat.mul_mod_left, Nat.mod_eq_of_lt ht,
+    Nat.mod_eq_of_lt hs7, zero_add]
+  have hidx : (q * 7 + s) * 7 ^ k + r = q * (7 ^ k * 7) + (s * 7 ^ k + r) := by ring
+  rw [hidx]
+  ring
+
+/-- Each prefix product has absolute value at most one. -/
+theorem abs_weight_le {c : ℕ → ℕ → ℤ} (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1)
+    (j p v : ℕ) : |weight c j p v| ≤ 1 := by
+  induction j generalizing p v with
+  | zero => simp [weight]
+  | succ j ih =>
+    rw [weight, abs_mul]
+    exact (mul_le_mul (ih _ _) (hc _ (Nat.mod_lt _ (by decide)) _
+      (Nat.mod_lt _ (by decide))) (abs_nonneg _) (by decide : (0 : ℤ) ≤ 1)).trans
+        (by norm_num)
+
+/-- Intermediate transformed values are bounded from the original input values. -/
+theorem abs_value_le {c : ℕ → ℕ → ℤ} (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1)
+    (j k p r : ℕ) {a : ℕ → ℤ} {A : ℤ}
+    (ha : ∀ v < 7 ^ j, |a (v * 7 ^ k + r)| ≤ A) :
+    |value c j k a p r| ≤ (7 ^ j : ℕ) * A := by
+  exact (abs_sum_mul_le (range (7 ^ j)) (fun v _ => abs_weight_le hc j p v)
+    (fun v hv => ha v (mem_range.mp hv))).trans_eq (by simp)
+
+/-- Input bounds suffice for every shared intermediate value, including all depths and all
+prefixes. Only the original input segment is used in this estimate. -/
+theorem abs_value_le_of_input {c : ℕ → ℕ → ℤ}
+    (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1) {L j k : ℕ} (hjk : j + k = L)
+    (p r : ℕ) (hr : r < 7 ^ k) {a : ℕ → ℤ} {A : ℤ}
+    (ha : ∀ i < 7 ^ L, |a i| ≤ A) : |value c j k a p r| ≤ (7 ^ j : ℕ) * A := by
+  apply abs_value_le hc
+  intro v hv
+  have hprod := Nat.mul_le_mul_right (7 ^ k) (Nat.succ_le_of_lt hv)
+  have hidx : v * 7 ^ k + r < 7 ^ j * 7 ^ k := by nlinarith only [hprod, hr]
+  rw [← pow_add, hjk] at hidx
+  exact ha _ hidx
+
+private theorem index_cons {b L : ℕ} (s : Fin b) (u : Fin L → Fin b) :
+    (finFunctionFinEquiv (Fin.cons s u) : ℕ) = s.val + b * (finFunctionFinEquiv u : ℕ) := by
+  simp only [finFunctionFinEquiv_apply, Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ,
+    Fin.val_zero, pow_zero, mul_one, Fin.val_succ, pow_succ, Finset.mul_sum]
+  congr 1
+  apply sum_congr rfl
+  intro i _
+  ring
+
+/-- Digitwise coefficients as a total flat table. Only the first ten rows and seven columns
+are read by the transform. -/
+def table (c : Fin 10 → Fin 7 → ℤ) (t s : ℕ) : ℤ :=
+  c ⟨t % 10, Nat.mod_lt _ (by decide)⟩ ⟨s % 7, Nat.mod_lt _ (by decide)⟩
+
+/-- Flat prefix weights are exactly the product of the original coordinate coefficients.
+`finFunctionFinEquiv` supplies the existing Mathlib digit numbering, least significant first. -/
+theorem weight_index (c : Fin 10 → Fin 7 → ℤ) {L : ℕ}
+    (τ : Fin L → Fin 10) (u : Fin L → Fin 7) :
+    weight (table c) L (finFunctionFinEquiv τ) (finFunctionFinEquiv u) =
+      ∏ i, c (τ i) (u i) := by
+  induction L with
+  | zero => simp [weight]
+  | succ L ih =>
+    rw [← Fin.cons_self_tail τ, ← Fin.cons_self_tail u, index_cons, index_cons, weight]
+    have ht : ((τ 0).val + 10 * (finFunctionFinEquiv (Fin.tail τ) : ℕ)) / 10 =
+        (finFunctionFinEquiv (Fin.tail τ) : ℕ) := by omega
+    have hu : ((u 0).val + 7 * (finFunctionFinEquiv (Fin.tail u) : ℕ)) / 7 =
+        (finFunctionFinEquiv (Fin.tail u) : ℕ) := by omega
+    have htmod : ((τ 0).val + 10 * (finFunctionFinEquiv (Fin.tail τ) : ℕ)) % 10 =
+        (τ 0).val := by omega
+    have humod : ((u 0).val + 7 * (finFunctionFinEquiv (Fin.tail u) : ℕ)) % 7 =
+        (u 0).val := by omega
+    rw [ht, hu, htmod, humod, ih, Fin.prod_univ_succ]
+    simp only [table, Nat.mod_eq_of_lt (τ 0).isLt, Nat.mod_eq_of_lt (u 0).isLt,
+      Fin.cons_zero, Fin.cons_succ]
+    exact mul_comm _ _
+
+/-- At the final stage the flat transform is the tensor encoding sum on digit strings.
+The input array is supplied explicitly by its values at Mathlib's numbered string positions. -/
+theorem value_final (c : Fin 10 → Fin 7 → ℤ) (L : ℕ)
+    (a : (Fin L → Fin 7) → ℤ) (arr : ℕ → ℤ)
+    (harr : ∀ u, arr (finFunctionFinEquiv u) = a u) (τ : Fin L → Fin 10) :
+    value (table c) L 0 arr (finFunctionFinEquiv τ) 0 =
+      ∑ u, a u * ∏ i, c (τ i) (u i) := by
+  simp only [value, pow_zero, mul_one, add_zero]
+  rw [← Fin.sum_univ_eq_sum_range]
+  rw [← (finFunctionFinEquiv (m := 7) (n := L)).sum_comp]
+  apply sum_congr rfl
+  intro u _
+  rw [weight_index, harr, mul_comm]
+
+/-- The mixed-radix stage fits into a buffer of `10^(j+k)` entries. -/
+theorem stageSize_le (j k : ℕ) : 10 ^ j * 7 ^ k ≤ 10 ^ (j + k) := by
+  rw [pow_add]
+  exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by decide : 7 ≤ 10) k)
+
+/-- Even charging every one of the `L` stages at the maximum array size gives only
+`L * 10^L` cells. This is a combinatorial bound; native loop and arithmetic costs are separate. -/
+theorem total_stageSize_le (L : ℕ) :
+    ∑ j ∈ range L, 10 ^ (j + 1) * 7 ^ (L - (j + 1)) ≤ L * 10 ^ L := by
+  calc
+    _ ≤ ∑ _j ∈ range L, 10 ^ L := by
+      apply sum_le_sum
+      intro j hj
+      have hjL : j + 1 ≤ L := by have := mem_range.mp hj; omega
+      simpa only [Nat.add_sub_of_le hjL] using stageSize_le (j + 1) (L - (j + 1))
+    _ = _ := by simp
+
+end Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Cell.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Cell.lean
new file mode 100644
index 000000000..160e70cd7
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Cell.lean
@@ -0,0 +1,129 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Forms
+import Mathlib.Tactic.Ring
+
+/-!
+# A native mixed-radix encoding cell
+
+## Main results
+
+* `Encoding.exec_cell`: charged index arithmetic, coefficient dispatch, signed linear form,
+  output store and counter increment for one cell of a shared coordinate transform.
+
+## References
+
+The linear forms are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+
+/-- The registers modified by a cell, apart from the nine signed-arithmetic scratch registers. -/
+def CellLocal (i : Fin 32) : Prop :=
+  i = cell ∨ i = block ∨ i = term ∨ i = suffix ∨ i = address ∨
+    i = accumulator ∨ i = group ∨ i = temporary
+
+instance (i : Fin 32) : Decidable (CellLocal i) :=
+  inferInstanceAs (Decidable (i = cell ∨ i = block ∨ i = term ∨ i = suffix ∨
+    i = address ∨ i = accumulator ∨ i = group ∨ i = temporary))
+
+private theorem cell_preserves (side : Bool) (i : Fin 32) :
+    9 ≤ i.val → ¬CellLocal i → (cellBody side).Preserves i := by
+  decide +kernel +revert
+
+/-- One output entry, with all index arithmetic and the counter increment charged. A single
+ordinary explicit natural-number bound covers the addresses and index products; no fit
+condition is imposed on an unspecified intermediate machine state. -/
+theorem exec_cell {w : ℕ} (hw : 0 < w) (side : Bool) (x : Data 32)
+    (P n s d i : ℕ) (hP : 0 < P) (hnpos : 0 < n) (hi : i < 10 * P * n)
+    (hsrc : x.regs src = s) (hdst : x.regs dst = d) (hcell : x.regs cell = i)
+    (hn : x.regs stride = n) (hseven : x.regs seven = 7)
+    (hten : x.regs ten = 10) (hone : x.regs one = 1)
+    (v : Fin 7 → ℤ) (B : ℤ) (hB : 0 ≤ B) (hv : ∀ a, |v a| ≤ B)
+    (hmem : ∀ a, x.mem (s + (i / (10 * n) * 7 + a.val) * n + i % n) = encode (v a))
+    (hval : 7 * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (s + d + 64 + 64 * P * n)) :
+    ∃ y, ExecWithin (w + 2) (cellBody side) x y 205 ∧
+      y.mem = Function.update x.mem (d + i)
+        (encode (∑ a, coefficients side ⟨i / n % 10, Nat.mod_lt _ (by decide)⟩ a * v a)) ∧
+      y.regs cell = i + 1 ∧
+      (∀ a, 9 ≤ a.val → ¬CellLocal a → y.regs a = x.regs a) := by
+  let p := i / (10 * n)
+  let t : Fin 10 := ⟨i / n % 10, Nat.mod_lt _ (by decide)⟩
+  let r := i % n
+  -- Keep nonlinear arithmetic focused on index bounds, rather than the execution context.
+  have hp : p < P := by
+    apply (Nat.div_lt_iff_lt_mul (by positivity : 0 < 10 * n)).mpr
+    nlinarith only [hi]
+  have hr : r < n := Nat.mod_lt _ hnpos
+  have hn1 : 1 ≤ n := hnpos
+  have hPn : n ≤ P * n := Nat.le_mul_of_pos_left n hP
+  have hmul : p * n < P * n := Nat.mul_lt_mul_of_pos_right hp hnpos
+  have h10n : Fits (w + 2) (10 * n) := haddr.of_le (by nlinarith only [hPn])
+  have hpfit : Fits (w + 2) p := haddr.of_le (by nlinarith only [hp, hn1])
+  have hdiv : i / n ≤ i := Nat.div_le_self _ _
+  have hdivfit : Fits (w + 2) (i / n) := haddr.of_le (by nlinarith only [hdiv, hi])
+  have htfit : Fits (w + 2) t.val := haddr.of_le (by have := t.isLt; omega)
+  have hrfit : Fits (w + 2) r := haddr.of_le (by nlinarith only [hr, hPn])
+  have hp7 : Fits (w + 2) (p * 7) := haddr.of_le (by nlinarith only [hp, hn1])
+  have hp7n : Fits (w + 2) (p * 7 * n) := haddr.of_le (by nlinarith only [hmul])
+  have hp7nr : Fits (w + 2) (p * 7 * n + r) :=
+    haddr.of_le (by nlinarith only [hmul, hr, hPn])
+  have hgroup : Fits (w + 2) (s + (p * 7 * n + r)) :=
+    haddr.of_le (by nlinarith only [hmul, hr, hPn])
+  let z := ((((((((x.set temporary (10 * n)).set block p).set term (i / n)).set term t.val).set
+    suffix r).set group (p * 7)).set group (p * 7 * n)).set group (p * 7 * n + r)).set
+      group (s + (p * 7 * n + r))
+  have hz : ExecWithin (w + 2) cellSetup x z 9 := by
+    ram_eval [cellSetup, z, p, t, r, hsrc, hcell, hn, hseven, hten,
+      h10n, hpfit, hdivfit, htfit, hrfit, hp7, hp7n, hp7nr, hgroup,
+      temporary, block, term, suffix, group, src, cell, stride, seven, ten, Fin.mk.injEq]
+  have hzterm : z.regs term = t.val := by
+    simp [z, temporary, block, term, suffix, group]
+  have hzgroup : z.regs group = s + (p * 7 * n + r) := by simp [z]
+  have hzn : z.regs stride = n := by
+    simpa [z, temporary, block, term, suffix, group, stride, Fin.mk.injEq] using hn
+  have hzmem : ∀ a, z.mem (s + (p * 7 * n + r) + a.val * n) = encode (v a) := by
+    intro a
+    have hidx : s + (p * 7 * n + r) + a.val * n = s + (p * 7 + a.val) * n + r := by ring
+    simpa only [z, Data.set_mem, hidx] using hmem a
+  have hspan : Fits (w + 2) (s + (p * 7 * n + r) + 7 * n) :=
+    haddr.of_le (by nlinarith only [hmul, hr, hPn])
+  obtain ⟨u, hu, huacc, humem, hureg⟩ := exec_dispatch hw side (List.finRange 10) t
+    (List.mem_finRange _) z B (s + (p * 7 * n + r)) n v hzterm hzgroup hzn hzmem
+    hB hv hval hspan (haddr.of_le (by omega))
+  have zucell : u.regs cell = i := by
+    rw [hureg cell (by decide) (by decide) (by decide) (by decide)]
+    simpa [z, temporary, block, term, suffix, group, cell, Fin.mk.injEq] using hcell
+  have zudst : u.regs dst = d := by
+    rw [hureg dst (by decide) (by decide) (by decide) (by decide)]
+    simpa [z, temporary, block, term, suffix, group, dst, Fin.mk.injEq] using hdst
+  have zuone : u.regs one = 1 := by
+    rw [hureg one (by decide) (by decide) (by decide) (by decide)]
+    simpa [z, temporary, block, term, suffix, group, one, Fin.mk.injEq] using hone
+  have hdfit : Fits (w + 2) (d + i) := haddr.of_le (by nlinarith only [hi])
+  have hinc : Fits (w + 2) (i + 1) := haddr.of_le (by nlinarith only [hi])
+  let y := ((u.set address (d + i)).write (d + i) (u.regs accumulator)).set cell (i + 1)
+  have hy : ExecWithin (w + 2) cellFinish u y 3 := by
+    ram_eval [cellFinish, y, zucell, zudst, zuone, hdfit, hinc,
+      address, cell, accumulator, dst, one, Fin.mk.injEq]
+  have he : ExecWithin (w + 2) (cellBody side) x y 205 := by
+    simpa only [cellBody, List.length_finRange] using (hz.seq (hu.seq hy)).mono
+      (by decide : 9 + ((3 * 10 + 163) + 3) ≤ 205)
+  refine ⟨y, he, ?_, ?_, fun a ha hl => he.regs_eq (cell_preserves side a ha hl)⟩
+  · simp only [y, Data.set_mem, Data.write_mem, humem, z, huacc]
+    rfl
+  · simp [y]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Controller.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Controller.lean
new file mode 100644
index 000000000..04eabe5c3
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Controller.lean
@@ -0,0 +1,250 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Header
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Meaning
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Copy
+import Mathlib.Tactic.Ring
+
+/-!
+# Alternating buffers for the shared native encoder
+
+## Main definitions
+
+* `Encoding.destination`, `Encoding.source`: the alternating buffer addresses.
+* `Encoding.Progress`: the mixed-radix array and frame invariant after a stage.
+
+## References
+
+The shared encodings are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open CoordinateTransform
+
+/-- Destination of the next coordinate transform; always one of the two fixed buffers. -/
+def destination (L : ℕ) : ℕ → ℕ
+  | 0 => outputBase L
+  | j + 1 => if destination L j = outputBase L then scratchBase L else outputBase L
+
+/-- Source of the next coordinate transform; initially the preserved input segment. -/
+def source (L : ℕ) : ℕ → ℕ
+  | 0 => 2
+  | j + 1 => destination L j
+
+/-- A destination is either the fixed output block or the scratch block. -/
+theorem destination_cases (L j : ℕ) :
+    destination L j = outputBase L ∨ destination L j = scratchBase L := by
+  cases j with
+  | zero => exact Or.inl rfl
+  | succ j => unfold destination; split <;> simp
+
+/-- After the initial transform, the source is also one of the two buffers. -/
+theorem source_cases {L j : ℕ} (hj : 0 < j) :
+    source L j = outputBase L ∨ source L j = scratchBase L := by
+  cases j with
+  | zero => omega
+  | succ j => exact destination_cases L j
+
+/-- The two alternating buffer addresses differ at every stage. -/
+theorem source_ne_destination (L j : ℕ) : source L j ≠ destination L j := by
+  have hpos : 0 < 10 ^ L := by positivity
+  have h7pos : 0 < 7 ^ L := by positivity
+  cases j with
+  | zero => simp only [source, destination, outputBase]; omega
+  | succ j =>
+    rcases destination_cases L j with h | h
+    · simp only [source, destination, h, ↓reduceIte]
+      unfold scratchBase
+      omega
+    · have hne : scratchBase L ≠ outputBase L := by unfold scratchBase; omega
+      simp only [source, destination, h, hne, ↓reduceIte]
+      exact hne
+
+/-- Both current addresses are bounded by the end of the second buffer. -/
+theorem buffer_address_le (L j : ℕ) :
+    source L j ≤ 2 + 2 * 10 ^ L ∧ destination L j ≤ 2 + 2 * 10 ^ L := by
+  have h7 := Nat.pow_le_pow_left (by decide : 7 ≤ 10) L
+  have hd := destination_cases L j
+  have hs : source L j = 2 ∨ source L j = outputBase L ∨ source L j = scratchBase L := by
+    cases j with
+    | zero => exact Or.inl rfl
+    | succ j => exact Or.inr (destination_cases L j)
+  simp only [scratchBase, outputBase] at hs hd
+  constructor <;> omega
+
+/-- Arrays stored at consecutive buffers are disjoint, in either order. The initial input
+ends exactly at the first output address. -/
+theorem buffers_separated {L j k N : ℕ} (hjk : j + k = L)
+    (hN : N ≤ 10 ^ L) :
+    source L j + 10 ^ j * 7 ^ k ≤ destination L j ∨
+      destination L j + N ≤ source L j := by
+  have hsize : 10 ^ j * 7 ^ k ≤ 10 ^ L := by simpa only [hjk] using stageSize_le j k
+  cases j with
+  | zero =>
+    left
+    simp only [Nat.zero_add] at hjk
+    simp [source, destination, outputBase, hjk]
+  | succ j =>
+    have hs := source_cases (L := L) (j := j + 1) (by omega)
+    have hd := destination_cases L (j + 1)
+    have hne := source_ne_destination L (j + 1)
+    unfold scratchBase at hs hd
+    omega
+
+/-- The shared-array invariant at depth `j`. All fields describe ordinary registers or
+mathematical memory values. Execution, timing and width are proved separately. -/
+structure Progress (side : Bool) (L j : ℕ) (arr : ℕ → ℤ) (initial : ℕ → ℕ)
+    (y : Data 32) : Prop where
+  /-- Fixed parameters retained across coordinate stages. -/
+  fixed : y.regs depth = L ∧ y.regs capacity = 10 ^ L ∧
+    y.regs output = outputBase L ∧ y.regs scratch = scratchBase L ∧
+    y.regs one = 1 ∧ y.regs seven = 7 ∧ y.regs ten = 10
+  /-- Number of transformed coordinates. -/
+  stage : y.regs Encoding.stage = j
+  /-- Number of transformed prefixes. -/
+  prefixes : y.regs Encoding.prefixes = 10 ^ j
+  /-- Original suffix length in the current source. -/
+  stride : y.regs Encoding.stride = 7 ^ (L - j)
+  /-- Current source address. -/
+  src : y.regs Encoding.src = source L j
+  /-- Current destination address. -/
+  dst : y.regs Encoding.dst = destination L j
+  /-- The source holds exactly the shared prefix sums. -/
+  values : ∀ p < 10 ^ j, ∀ r < 7 ^ (L - j),
+    y.mem (source L j + p * 7 ^ (L - j) + r) =
+      encode (value (table (coefficients side)) j (L - j) arr p r)
+  /-- Input, headers and all cells outside both work buffers are preserved. -/
+  frame : ∀ a, ¬(outputBase L ≤ a ∧ a < scratchBase L + 10 ^ L) → y.mem a = initial a
+
+/-- The actual header initialization establishes the zero-stage invariant from the original
+flat input segment. No scratch values or preinitialized coefficient tables are required. -/
+theorem progress_zero (side : Bool) (L : ℕ) (arr : ℕ → ℤ) (x y : Data 32)
+    (hy : SetupPost L x y) (hinput : ∀ i < 7 ^ L, x.mem (2 + i) = encode (arr i)) :
+    Progress side L 0 arr x.mem y := by
+  refine ⟨⟨hy.depth, hy.capacity, hy.output, hy.scratch, hy.one, hy.seven, hy.ten⟩,
+    hy.stage, hy.prefixes, ?_, hy.src, hy.dst, ?_, ?_⟩
+  · simpa only [Nat.sub_zero] using hy.stride
+  · intro p hp r hr
+    have hp0 : p = 0 := by simpa only [pow_zero] using Nat.eq_zero_of_le_zero (by omega : p ≤ 0)
+    subst p
+    rw [hy.mem, value_zero]
+    simpa only [source, Nat.sub_zero, Nat.zero_mul, Nat.add_zero] using hinput r hr
+  · intro a _
+    rw [hy.mem]
+
+/-- One proved native stage advances the mixed-radix invariant. The signed magnitude bound
+comes from the original input and the number of coordinates already transformed. -/
+theorem progress_step {w L j : ℕ} (hw : 0 < w) (hj : j < L) (side : Bool)
+    (arr : ℕ → ℤ) (initial : ℕ → ℕ) (x : Data 32) (hx : Progress side L j arr initial x)
+    (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    ∃ y, ExecWithin (w + 2) (stageBody side) x y (207 * 10 ^ L + 12) ∧
+      Progress side L (j + 1) arr initial y := by
+  let k := L - (j + 1)
+  let n := 7 ^ k
+  let P := 10 ^ j
+  have hn : 0 < n := by dsimp only [n]; positivity
+  have hP : 0 < P := by dsimp only [P]; positivity
+  have hk : L - j = k + 1 := by omega
+  have hjk : j + (k + 1) = L := by omega
+  have hjk' : j + 1 + k = L := by omega
+  have hstride : 7 ^ (L - j) = 7 * n := by rw [hk, pow_succ']
+  have hN : 10 * P * n ≤ 10 ^ L := by
+    have h := stageSize_le (j + 1) k
+    simpa only [hjk', pow_succ', P, n] using h
+  have hcoeff : ∀ t < 10, ∀ s < 7, |table (coefficients side) t s| ≤ 1 := by
+    intro t _ s _
+    unfold table coefficients
+    cases side
+    · exact abs_phi_le_one _ _
+    · exact abs_psi_le_one _ _
+  let v (i : ℕ) (a : Fin 7) : ℤ := value (table (coefficients side)) j (k + 1) arr
+    (i / (10 * n)) (a.val * n + i % n)
+  let B : ℤ := (7 ^ j : ℕ) * A
+  have hB : 0 ≤ B := mul_nonneg (by positivity) hA
+  have hsuffix (i : ℕ) (a : Fin 7) : a.val * n + i % n < 7 ^ (k + 1) := by
+    have hm := Nat.mul_le_mul_right n (Nat.succ_le_of_lt a.isLt)
+    have hr := Nat.mod_lt i hn
+    rw [pow_succ']
+    change a.val * n + i % n < 7 * n
+    nlinarith only [hm, hr]
+  have hv : ∀ i < 10 * P * n, ∀ a, |v i a| ≤ B := by
+    intro i _ a
+    exact abs_value_le_of_input hcoeff hjk _ _ (hsuffix i a) ha
+  have hload : ∀ i < 10 * P * n, ∀ a,
+      x.mem (source L j + (i / (10 * n) * 7 + a.val) * n + i % n) = encode (v i a) := by
+    intro i hi a
+    have hp : i / (10 * n) < 10 ^ j := by
+      apply (Nat.div_lt_iff_lt_mul (by positivity : 0 < 10 * n)).mpr
+      dsimp only [P] at hi
+      nlinarith only [hi]
+    have hidx : source L j + (i / (10 * n) * 7 + a.val) * n + i % n =
+        source L j + i / (10 * n) * 7 ^ (L - j) + (a.val * n + i % n) := by
+      rw [hstride]
+      ring
+    rw [hidx, hx.values _ hp _ (by rw [hk]; exact hsuffix i a)]
+    rw [hk]
+  have hvalue : 7 * B < (2 : ℤ) ^ (w - 1) := by
+    have hpow : 7 ^ (j + 1) ≤ 7 ^ L := Nat.pow_le_pow_right (by decide) (by omega)
+    have hpowZ : ((7 ^ (j + 1) : ℕ) : ℤ) ≤ (7 ^ L : ℕ) := by exact_mod_cast hpow
+    have hprod := mul_le_mul_of_nonneg_right hpowZ hA
+    simpa only [Nat.pow_succ', Nat.cast_mul, Nat.cast_ofNat, mul_assoc, B] using
+      hprod.trans_lt hmag
+  have hbound := buffer_address_le L j
+  have hcap : 1 ≤ 10 ^ L := Nat.one_le_pow L 10 (by decide)
+  have hnative : Fits (w + 2) (source L j + destination L j + 64 + 64 * P * n) :=
+    haddr.of_le (by unfold addressBound; nlinarith only [hbound.1, hbound.2, hN, hcap])
+  have hseparate : source L j + 7 * P * n ≤ destination L j ∨
+      destination L j + 10 * P * n ≤ source L j := by
+    have h := buffers_separated (k := L - j) (by omega : j + (L - j) = L) hN
+    simpa only [hstride, P, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using h
+  obtain ⟨y, he, hm, hf, hsrc, hdst, hstr, hp, hstage, hreg⟩ := exec_stageBody hw side x
+    P n (source L j) (destination L j) j (outputBase L) (scratchBase L) hP hn hx.src hx.dst
+    hx.stage (by simpa only [hstride] using hx.stride) hx.prefixes hx.fixed.2.2.2.2.2.1
+    hx.fixed.2.2.2.2.2.2 hx.fixed.2.2.2.2.1 hx.fixed.2.2.1 hx.fixed.2.2.2.1 v B hB hv hload
+    hvalue hnative (haddr.of_le (by unfold addressBound; omega)) hseparate
+  refine ⟨y, he.mono (by omega), ?_⟩
+  have hr (a : Fin 32) (ha : 9 ≤ a.val) (hl : ¬StageLocal a) : y.regs a = x.regs a := hreg a ha hl
+  refine ⟨?_, hstage, ?_, ?_, hsrc, hdst, ?_, ?_⟩
+  · rcases hx.fixed with ⟨hd, hc, ho, hs, h1, h7, h10⟩
+    exact ⟨(hr depth (by decide) (by decide)).trans hd,
+      (hr capacity (by decide) (by decide)).trans hc,
+      (hr output (by decide) (by decide)).trans ho,
+      (hr scratch (by decide) (by decide)).trans hs,
+      (hr one (by decide) (by decide)).trans h1,
+      (hr seven (by decide) (by decide)).trans h7,
+      (hr ten (by decide) (by decide)).trans h10⟩
+  · simpa only [P, pow_succ'] using hp
+  · exact hstr
+  · intro p hpp r hrr
+    have hrr' : r < n := hrr
+    have hpp' : p < 10 * P := by simpa only [pow_succ', P] using hpp
+    have hprod := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hpp')
+    have hi : p * n + r < 10 * P * n := by nlinarith only [hprod, hrr']
+    have hdiv : (p * n + r) / n = p := by
+      rw [Nat.mul_comm p n, Nat.mul_add_div hn, Nat.div_eq_of_lt hrr', Nat.add_zero]
+    have hmod : (p * n + r) % n = r := Nat.mul_add_mod_of_lt hrr'
+    have hvout := hm (p * n + r) hi
+    rw [show stageResult side n v (p * n + r) = value (table (coefficients side))
+      (j + 1) k arr ((p * n + r) / n) ((p * n + r) % n) from stageResult_value side j k _ arr,
+      hdiv, hmod] at hvout
+    simpa only [source, n, k, Nat.add_assoc] using hvout
+  · intro a haout
+    rw [hf a ?_]
+    · exact hx.frame a haout
+    · rcases destination_cases L j with hd | hd <;> rw [hd] <;> unfold scratchBase at * <;> omega
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Copy.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Copy.lean
new file mode 100644
index 000000000..8ada70338
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Copy.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+/-!
+# Copying the final encoding to its fixed output block
+
+## Main results
+
+* `Encoding.exec_copyOut`: reuse the native array copy, including equal blocks and both
+  possible disjoint address orders, with its charged `7n+4` bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM
+
+/-- The final copy uses seven instructions per output word plus four instructions of setup
+and loop termination. Equal source/output blocks are permitted, so odd and even depths use
+the same fixed program. All other registers retain their values. -/
+theorem exec_copyOut {w : ℕ} (x : Data 32) (h1 : Fits w 1)
+    (hs : Fits w (x.regs src + x.regs capacity))
+    (hd : Fits w (x.regs output + x.regs capacity))
+    (hdisj : x.regs src + x.regs capacity ≤ x.regs output ∨
+      x.regs output + x.regs capacity ≤ x.regs src ∨ x.regs src = x.regs output) :
+    ∃ y, ExecWithin w copyOut x y (7 * x.regs capacity + 4) ∧
+      y.mem = ArrayCopy.copyPrefix x.mem (x.regs src) (x.regs output) (x.regs capacity) ∧
+      (∀ i, i ≠ cell → i ≠ address → i ≠ accumulator → i ≠ one → y.regs i = x.regs i) := by
+  obtain ⟨z, hz, hm, _, _, _⟩ := ArrayCopy.exec_of_separated_or_eq (x.comap copyRegisters)
+    h1 hs hd hdisj
+  have he := hz.rename copyRegisters_injective
+  refine ⟨z.extend copyRegisters x, he, hm, ?_⟩
+  intro i hc ha hv ho
+  apply he.regs_eq
+  have hp : ∀ i : Fin 32, i ≠ cell → i ≠ address → i ≠ accumulator → i ≠ one →
+      copyOut.Preserves i := by decide
+  exact hp i hc ha hv ho
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Encoding.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Encoding.lean
new file mode 100644
index 000000000..10afd12bb
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Encoding.lean
@@ -0,0 +1,244 @@
+/-
+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 Complexity.Computability.WordRAM.Signed.Arithmetic
+public import Complexity.Computability.WordRAM.Copy
+
+/-!
+# Native shared tensor encoding
+
+The two fixed programs use unsigned addresses and counters, and sign-and-magnitude encoded
+integer entries. Address 1 holds the depth; the `7^L` encoded entries begin at address 2.
+The ordinary `State.init` length header is at address 0. Output and scratch are consecutive
+blocks of `10^L` cells immediately after the input. Each coordinate transform reads the
+previous stage and writes the other buffer. No initialization of unread scratch is needed.
+A final charged copy puts the result in the first buffer, also at depth zero.
+
+The coordinate transform is a new iterative implementation of the linear forms in
+[AlmanWilliams2026, Section 2.4.1]. The coefficients and mathematical encoding are selectively
+adapted from Anthropic's formal-math revision `16a5ce41304fcdaea4e0be7c132e1c361dc26da5`,
+[`Step`](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/Step.lean)
+and [`Recursion`](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/Recursion.lean). The source's
+recursive machine and execution semantics are not used.
+
+## Main definitions
+
+* `Encoding.program`: fixed native code for either coefficient table.
+* `Encoding.input`: concrete input for `State.init`, including the depth header.
+* `Encoding.outputBase`, `Encoding.scratchBase`: disjoint output and scratch blocks.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Seven variable digits: the three outer variables, then the four inner variables. -/
+def leftAt (s : Fin 7) : LeftVar :=
+  if h : s.val < 3 then .x ⟨s.val, h⟩
+  else .p ⟨(s.val - 3) / 2, by omega⟩ ⟨(s.val - 3) % 2, Nat.mod_lt _ (by decide)⟩
+
+/-- Right-variable digits use the same order as the left-variable digits. -/
+def rightAt (s : Fin 7) : RightVar :=
+  if h : s.val < 3 then .y ⟨s.val, h⟩
+  else .q ⟨(s.val - 3) / 2, by omega⟩ ⟨(s.val - 3) % 2, Nat.mod_lt _ (by decide)⟩
+
+/-- Row-major order on the nine `P` terms, followed by `P0`. -/
+def termAt (t : Fin 10) : Term :=
+  if h : t.val < 9 then .P ⟨t.val / 3, by omega⟩ ⟨t.val % 3, Nat.mod_lt _ (by decide)⟩
+  else .P0
+
+/-- Explicit numbering of the seven left variables. -/
+def leftDigits : Fin 7 ≃ LeftVar where
+  toFun := leftAt
+  invFun
+    | .x i => ⟨i.val, by omega⟩
+    | .p i j => ⟨3 + 2 * i.val + j.val, by omega⟩
+  left_inv := by decide
+  right_inv := by decide
+
+/-- Explicit numbering of the seven right variables. -/
+def rightDigits : Fin 7 ≃ RightVar where
+  toFun := rightAt
+  invFun
+    | .y j => ⟨j.val, by omega⟩
+    | .q i j => ⟨3 + 2 * i.val + j.val, by omega⟩
+  left_inv := by decide
+  right_inv := by decide
+
+/-- Explicit numbering of all ten terms. -/
+def termDigits : Fin 10 ≃ Term where
+  toFun := termAt
+  invFun
+    | .P i j => ⟨3 * i.val + j.val, by omega⟩
+    | .P0 => 9
+  left_inv := by decide
+  right_inv := by decide
+
+/-- The left and right coefficient tables, with digits made explicit. -/
+def coefficients (rightSide : Bool) (t : Fin 10) (s : Fin 7) : ℤ :=
+  if rightSide then psi (termAt t) (rightAt s) else phi (termAt t) (leftAt s)
+
+/-- Every actual coefficient is zero, one or minus one. -/
+theorem coefficients_values (side : Bool) (t : Fin 10) (s : Fin 7) :
+    coefficients side t s = 0 ∨ coefficients side t s = 1 ∨ coefficients side t s = -1 := by
+  decide +revert
+
+/-- The input block ends where the output block begins. -/
+def outputBase (L : ℕ) : ℕ := 2 + 7 ^ L
+
+/-- The scratch block immediately follows the entire output block. -/
+def scratchBase (L : ℕ) : ℕ := outputBase L + 10 ^ L
+
+/-- Concrete input: depth header followed by the signed input entries in flat order.
+The caller encodes each integer with `Signed.encode` before passing the list to `State.init`.
+The native unsigned length header is installed by `State.init` itself. -/
+def input (L : ℕ) (a : Fin (7 ^ L) → ℤ) : List ℕ :=
+  L :: List.ofFn (fun i => encode (a i))
+
+/-- The concrete left-array input, using Mathlib's base-seven string numbering. -/
+def inputL {L : ℕ} (a : LeftStr L → ℤ) : List ℕ :=
+  input L fun i => a fun ℓ => leftAt (finFunctionFinEquiv.symm i ℓ)
+
+/-- The concrete right-array input, in exactly the same flat memory layout. -/
+def inputR {L : ℕ} (a : RightStr L → ℤ) : List ℕ :=
+  input L fun i => a fun ℓ => rightAt (finFunctionFinEquiv.symm i ℓ)
+
+/-- All thirty-two registers are fixed independently of depth and width. Registers 0–8
+are precisely the existing signed-arithmetic workspace. -/
+abbrev depth : Fin 32 := 9
+@[inherit_doc depth] abbrev inputSize : Fin 32 := 10
+@[inherit_doc depth] abbrev capacity : Fin 32 := 11
+@[inherit_doc depth] abbrev src : Fin 32 := 12
+@[inherit_doc depth] abbrev dst : Fin 32 := 13
+@[inherit_doc depth] abbrev output : Fin 32 := 14
+@[inherit_doc depth] abbrev scratch : Fin 32 := 15
+@[inherit_doc depth] abbrev stride : Fin 32 := 16
+@[inherit_doc depth] abbrev prefixes : Fin 32 := 17
+@[inherit_doc depth] abbrev stage : Fin 32 := 18
+@[inherit_doc depth] abbrev cell : Fin 32 := 19
+@[inherit_doc depth] abbrev block : Fin 32 := 20
+@[inherit_doc depth] abbrev term : Fin 32 := 21
+@[inherit_doc depth] abbrev suffix : Fin 32 := 22
+@[inherit_doc depth] abbrev address : Fin 32 := 23
+@[inherit_doc depth] abbrev accumulator : Fin 32 := 24
+@[inherit_doc depth] abbrev one : Fin 32 := 25
+@[inherit_doc depth] abbrev seven : Fin 32 := 26
+@[inherit_doc depth] abbrev ten : Fin 32 := 27
+@[inherit_doc depth] abbrev group : Fin 32 := 28
+@[inherit_doc depth] abbrev temporary : Fin 32 := 29
+@[inherit_doc depth] abbrev stageSize : Fin 32 := 30
+
+/-- One coefficient in `{0, 1, -1}` times one array entry. Zero coefficients cause no load.
+Nonzero coefficients use the proved native signed addition or subtraction block. -/
+def summand (s : Fin 7) (c : ℤ) : Code .standard 32 :=
+  if c = 0 then ram[ accumulator ← accumulator ]
+  else .seq (ram[
+    temporary ← #s.val;
+    address ← temporary * stride; address ← group + address;
+    right ← *address; left ← accumulator ])
+    (.seq (if c = 1 then add else subtract) (ram[ accumulator ← result ]))
+
+/-- A finite unrolling of the seven coefficients. This recursion constructs code; it does
+not recurse on the input depth. -/
+def sumCode : List (Fin 7 × ℤ) → Code .standard 32
+  | [] => ram[ accumulator ← accumulator ]
+  | (s, c) :: rest => .seq (summand s c) (sumCode rest)
+
+/-- One linear form, including accumulator initialization. -/
+def form (side : Bool) (t : Fin 10) : Code .standard 32 :=
+  .seq (ram[ accumulator ← #0 ])
+    (sumCode (List.ofFn fun s => (s, coefficients side t s)))
+
+/-- A fixed finite dispatch on the ten possible term digits. -/
+def dispatch (side : Bool) : List (Fin 10) → Code .standard 32
+  | [] => ram[ accumulator ← #0 ]
+  | t :: rest => ram[
+      temporary ← #t.val;
+      if term = temporary then [ ⟪form side t⟫ ] else [ ⟪dispatch side rest⟫ ] ]
+
+/-- Decode one flat output index into its mixed-radix coordinates and source group. -/
+def cellSetup : Code .standard 32 := ram[
+  temporary ← ten * stride;
+  block ← cell / temporary;
+  term ← cell / stride; term ← term % ten;
+  suffix ← cell % stride;
+  group ← block * seven; group ← group * stride;
+  group ← group + suffix; group ← src + group ]
+
+/-- Store the computed entry and advance the flat index. -/
+def cellFinish : Code .standard 32 := ram[
+  address ← dst + cell; *address ← accumulator;
+  cell ← cell + one ]
+
+/-- One output cell. The flat index is `(prefix * 10 + term) * stride + suffix`;
+its seven source addresses are `(prefix * 7 + s) * stride + suffix`. -/
+def cellBody (side : Bool) : Code .standard 32 :=
+  .seq cellSetup (.seq (dispatch side (List.finRange 10)) cellFinish)
+
+/-- Divide the suffix stride and compute the next stage size. -/
+def stageHead : Code .standard 32 := ram[
+  stride ← stride / seven;
+  stageSize ← prefixes * ten; stageSize ← stageSize * stride;
+  cell ← #0 ]
+
+/-- Alternate the two buffers and advance the prefix and stage counters. -/
+def stageTail : Code .standard 32 := ram[
+  src ← dst;
+  if dst = output then [ dst ← scratch ] else [ dst ← output ];
+  prefixes ← prefixes * ten; stage ← stage + one ]
+
+/-- Transform the next coordinate, then alternate the output buffers. -/
+def stageBody (side : Bool) : Code .standard 32 :=
+  .seq stageHead (.seq (.loop (.lt cell stageSize) (cellBody side)) stageTail)
+
+/-- Load the actual depth header and initialize the power counters. -/
+def setupHead : Code .standard 32 := ram[
+  one ← #1; seven ← #7; ten ← #10;
+  address ← #1; depth ← *address;
+  inputSize ← #1; capacity ← #1; stage ← #0 ]
+
+/-- One multiplication by each radix and one counter increment. -/
+def powerBody : Code .standard 32 := ram[
+  inputSize ← inputSize * seven; capacity ← capacity * ten; stage ← stage + one ]
+
+/-- Compute the concrete buffer addresses from the powers and initialize the first stage. -/
+def setupTail : Code .standard 32 := ram[
+  temporary ← #2; output ← temporary + inputSize; scratch ← output + capacity;
+  src ← #2; dst ← output; stride ← inputSize; prefixes ← #1; stage ← #0 ]
+
+/-- Read the depth and compute both powers in a charged native loop. -/
+def setup : Code .standard 32 :=
+  .seq setupHead (.seq (.loop (.lt stage depth) powerBody) setupTail)
+
+/-- Reuse the existing seven-register array copy inside the encoder's register file. -/
+def copyRegisters : Fin 7 → Fin 32 := ![src, output, capacity, cell, address, accumulator, one]
+
+/-- The seven copy registers are distinct. -/
+theorem copyRegisters_injective : Function.Injective copyRegisters := by decide
+
+/-- A charged copy into the fixed output block, permitting disjoint blocks in either order
+or identical source and destination. -/
+def copyOut : Code .standard 32 := ArrayCopy.program.rename copyRegisters
+
+/-- The complete fixed native encoder, excluding its final halt. The returned `output`
+register identifies the first output cell; the `capacity` register holds its length. -/
+def program (side : Bool) : Code .standard 32 := ram[
+  ⟪setup⟫;
+  while stage < depth do [ ⟪stageBody side⟫ ];
+  ⟪copyOut⟫ ]
+
+/-- The code performs no word-width queries. -/
+theorem program_readsWidth (side : Bool) : ¬(program side).ReadsWidth := by
+  cases side <;> decide
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Exec.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Exec.lean
new file mode 100644
index 000000000..1d80c56e6
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Exec.lean
@@ -0,0 +1,136 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Controller
+import Mathlib.Tactic.Ring
+
+/-!
+# Complete charged execution of the shared encoder
+
+## Main results
+
+* `Encoding.exec_coordinates`: all shared coordinate transforms, with charged loop control.
+* `Encoding.exec`: complete initialization, transforms and fixed-output copy with an explicit
+  `240 * (L+1) * 10^L` native instruction bound.
+
+The code is directly over the standard unsigned WordRAM. Its signed add/subtract blocks use
+two extra target bits and respectively at most fifteen/seventeen actual instructions. There
+is no whole-program signed compiler in this construction and no uncharged simulation premise.
+
+## References
+
+The encodings are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open CoordinateTransform
+
+/-- Explicit total instruction bound, including header preparation, all index arithmetic,
+stage and cell loop control, and the final copy. A final halt costs one additional instruction. -/
+def timeBound (L : ℕ) : ℕ := 240 * (L + 1) * 10 ^ L
+
+/-- Every coordinate stage is executed natively. Charging every stage at the maximum buffer
+size gives `L * (207 * 10^L + 14) + 2` instructions, including both outer loop controls. -/
+theorem exec_coordinates {w L : ℕ} (hw : 0 < w) (side : Bool) (arr : ℕ → ℤ)
+    (initial : ℕ → ℕ) (x : Data 32) (hx : Progress side L 0 arr initial x)
+    (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    ∃ y, ExecWithin (w + 2) (.loop (.lt stage depth) (stageBody side)) x y
+        (L * (207 * 10 ^ L + 14) + 2) ∧ Progress side L L arr initial y := by
+  let I (y : Data 32) : Prop := ∃ j, j ≤ L ∧ Progress side L j arr initial y
+  have hbody (y : Data 32) (hy : I y) (hc : (Cond.lt stage depth).Holds y) :
+      ∃ z, ExecWithin (w + 2) (stageBody side) y z (207 * 10 ^ L + 12) ∧ I z ∧
+        L - z.regs stage < L - y.regs stage := by
+    obtain ⟨j, hj, hprogress⟩ := hy
+    have hjL : j < L := by simpa only [Cond.holds_lt, hprogress.stage, hprogress.fixed.1] using hc
+    obtain ⟨z, he, hz⟩ := progress_step hw hjL side arr initial y hprogress A hA ha hmag haddr
+    exact ⟨z, he, ⟨j + 1, by omega, hz⟩, by rw [hprogress.stage, hz.stage]; omega⟩
+  obtain ⟨y, he, ⟨j, hj, hy⟩, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => L - y.regs stage) hbody ⟨0, Nat.zero_le _, hx⟩
+  have hjL : j = L := by
+    simp only [Cond.holds_lt, hy.stage, hy.fixed.1] at hc
+    omega
+  subst j
+  refine ⟨y, ?_, hy⟩
+  simpa only [hx.stage, Nat.sub_zero, Nat.add_assoc] using he
+
+/-- The encoder runs from a concrete flat memory layout and preserves every cell outside
+its output/scratch region. Only the original input magnitude and explicit address bounds are
+assumed; every intermediate signed arithmetic fit is derived in the coordinate-stage proof. -/
+theorem exec {w L : ℕ} (hw : 0 < w) (side : Bool) (arr : ℕ → ℤ) (x : Data 32)
+    (hheader : x.mem 1 = L) (hinput : ∀ i < 7 ^ L, x.mem (2 + i) = encode (arr i))
+    (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    ∃ y, ExecWithin (w + 2) (program side) x y (timeBound L) ∧
+      (∀ p < 10 ^ L, y.mem (outputBase L + p) =
+        encode (value (table (coefficients side)) L 0 arr p 0)) ∧
+      (∀ a, ¬(outputBase L ≤ a ∧ a < scratchBase L + 10 ^ L) → y.mem a = x.mem a) ∧
+      y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L := by
+  obtain ⟨z, hz, hsetup⟩ := exec_setup L x hheader haddr
+  have hzero := progress_zero side L arr x z hsetup hinput
+  obtain ⟨u, hu, hp⟩ := exec_coordinates hw side arr x.mem z hzero A hA ha hmag haddr
+  have hsource := hp.src
+  have hout := hp.fixed.2.2.1
+  have hcap := hp.fixed.2.1
+  have hcap1 : 1 ≤ 10 ^ L := Nat.one_le_pow L 10 (by decide)
+  have hsfit : Fits (w + 2) (u.regs src + u.regs capacity) := by
+    rw [hsource, hcap]
+    apply haddr.of_le
+    have hb := (buffer_address_le L L).1
+    unfold addressBound
+    omega
+  have hdfit : Fits (w + 2) (u.regs output + u.regs capacity) := by
+    rw [hout, hcap]
+    apply haddr.of_le
+    have h7 := Nat.pow_le_pow_left (by decide : 7 ≤ 10) L
+    unfold addressBound outputBase
+    omega
+  have hdisj : u.regs src + u.regs capacity ≤ u.regs output ∨
+      u.regs output + u.regs capacity ≤ u.regs src ∨ u.regs src = u.regs output := by
+    rw [hsource, hout, hcap]
+    by_cases hL : L = 0
+    · rcases hL with rfl
+      left
+      decide
+    · rcases source_cases (L := L) (j := L) (by omega) with h | h
+      · exact Or.inr (Or.inr h)
+      · right
+        left
+        rw [h]
+        rfl
+  obtain ⟨y, hy, hymem, hyr⟩ := exec_copyOut u (haddr.of_le (by unfold addressBound; omega))
+    hsfit hdfit hdisj
+  have he : ExecWithin (w + 2) (program side) x y (timeBound L) := by
+    have hwhole := hz.seq (hu.seq hy)
+    apply hwhole.mono
+    rw [hcap]
+    unfold timeBound
+    have hLcap : L ≤ L * 10 ^ L := by nlinarith only [Nat.mul_le_mul_left L hcap1]
+    nlinarith only [hcap1, hLcap]
+  refine ⟨y, he, ?_, ?_, ?_, ?_⟩
+  · intro p hpp
+    rw [hymem, hsource, hout, hcap, ArrayCopy.copyPrefix_read hpp]
+    have h := hp.values p hpp 0 (by simp)
+    simpa only [Nat.sub_self, pow_zero, Nat.mul_one, Nat.add_zero] using h
+  · intro a haout
+    rw [hymem, hsource, hout, hcap, ArrayCopy.copyPrefix_outside ?_]
+    · exact hp.frame a haout
+    · unfold scratchBase at haout
+      omega
+  · exact (hyr output (by decide) (by decide) (by decide) (by decide)).trans hout
+  · exact (hyr capacity (by decide) (by decide) (by decide) (by decide)).trans hcap
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Flat.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Flat.lean
new file mode 100644
index 000000000..9ced15aa5
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Flat.lean
@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Input
+
+/-!
+# Flat standard-WordRAM clients for the complete encoders
+
+## Main results
+
+* `Encoding.runs_left`, `Encoding.runs_right`: actual flat runs from `State.init`, the complete
+  output memory block, preserved outside frame, and a charged final halt.
+* `Encoding.program_length_le`: one finite code-size bound independent of depth and width.
+
+The final halt returns the output block's address. Its length is `10^L` and its cells contain
+the canonical signed encodings of the public mathematical values.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+set_option maxRecDepth 4096 in
+-- Kernel reduction flattens the finite instruction list, including each signed arithmetic block.
+/-- A single code-size bound for both fixed encoders, including the final halt. -/
+theorem program_length_le (side : Bool) : ((program side).program output).length ≤ 4096 := by
+  cases side <;> decide
+
+/-- Every one of the `10^L` flat output cells corresponds to exactly one original leaf. -/
+theorem leafIndex_bijective (L : ℕ) : Function.Bijective (leafIndex (L := L)) := by
+  have h : Function.Bijective (fun τ : Leaf L => fun i => termDigits.symm (τ i)) :=
+    (Equiv.piCongrRight fun _ : Fin L => termDigits.symm).bijective
+  change Function.Bijective (fun τ : Leaf L =>
+    finFunctionFinEquiv (fun i => termDigits.symm (τ i)))
+  exact finFunctionFinEquiv.bijective.comp h
+
+/-- Actual flat native left-encoding execution. The prefix exposes every output memory cell;
+the same run then halts at its fixed final instruction, charging one more instruction. -/
+theorem runs_left {w L : ℕ} (hw : 0 < w) (a : LeftStr L → ℤ) (A : ℤ)
+    (hA : 0 ≤ A) (ha : ∀ u, |a u| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    InputFits (w + 2) (inputL a) ∧
+    ∃ y n, n ≤ timeBound L ∧
+      Runs (w + 2) ((program false).program output) (State.init (inputL a))
+        ⟨(program false).size, y⟩ n ∧
+      Executes (w + 2) ((program false).program output) (State.init (inputL a))
+        (outputBase L) (n + 1) ∧
+      (∀ τ, y.mem (outputBase L + (leafIndex τ).val) = encode (encodingL a τ)) ∧
+      (∀ b, ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) →
+        y.mem b = (State.init (inputL a) : State 32).data.mem b) := by
+  obtain ⟨hi, y, ⟨n, hn, he⟩, _, hv, hf, ho, _⟩ := exec_left hw a A hA ha hmag haddr
+  refine ⟨hi, y, n, hn, ?_, ?_, hv, hf⟩
+  · simpa only [Nat.zero_add, State.init] using he.runs (pc := 0)
+      (p := (program false).program output) (Program.Contains.self _).append_left
+  · simpa only [ho, State.init] using he.executes output
+
+/-- Actual flat native right-encoding execution, with all output cells and the same charged
+standard-WordRAM calling convention and final halt. -/
+theorem runs_right {w L : ℕ} (hw : 0 < w) (a : RightStr L → ℤ) (A : ℤ)
+    (hA : 0 ≤ A) (ha : ∀ u, |a u| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    InputFits (w + 2) (inputR a) ∧
+    ∃ y n, n ≤ timeBound L ∧
+      Runs (w + 2) ((program true).program output) (State.init (inputR a))
+        ⟨(program true).size, y⟩ n ∧
+      Executes (w + 2) ((program true).program output) (State.init (inputR a))
+        (outputBase L) (n + 1) ∧
+      (∀ τ, y.mem (outputBase L + (leafIndex τ).val) = encode (encodingR a τ)) ∧
+      (∀ b, ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) →
+        y.mem b = (State.init (inputR a) : State 32).data.mem b) := by
+  obtain ⟨hi, y, ⟨n, hn, he⟩, _, hv, hf, ho, _⟩ := exec_right hw a A hA ha hmag haddr
+  refine ⟨hi, y, n, hn, ?_, ?_, hv, hf⟩
+  · simpa only [Nat.zero_add, State.init] using he.runs (pc := 0)
+      (p := (program true).program output) (Program.Contains.self _).append_left
+  · simpa only [ho, State.init] using he.executes output
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Forms.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Forms.lean
new file mode 100644
index 000000000..33ed8e881
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Forms.lean
@@ -0,0 +1,235 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Encoding
+public import Complexity.Foundations.Algebra.FiniteMagnitude
+import Mathlib.Tactic.Ring
+
+/-!
+# Native execution of the encoding forms
+
+The form code reads seven strided entries and uses only the existing native signed arithmetic
+blocks. These results account for those blocks' actual instructions and their scratch registers.
+
+## Main results
+
+* `Encoding.exec_summand`: a coefficient in `{0, 1, -1}` takes at most 23 instructions.
+
+## References
+
+The linear forms are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+
+/-- Registers outside the signed workspace and the form's three local registers. -/
+def FormFrame (x y : Data 32) : Prop :=
+  y.mem = x.mem ∧ ∀ i, 9 ≤ i.val → i ≠ address → i ≠ accumulator → i ≠ temporary →
+    y.regs i = x.regs i
+
+/-- Form frames compose without changing any memory cell. -/
+theorem FormFrame.trans {x y z : Data 32} (hxy : FormFrame x y) (hyz : FormFrame y z) :
+    FormFrame x z :=
+  ⟨hyz.1.trans hxy.1, fun i hi ha hc ht =>
+    (hyz.2 i hi ha hc ht).trans (hxy.2 i hi ha hc ht)⟩
+
+private theorem fits_of_abs_lt {w : ℕ} (hw : 0 < w) {a : ℤ}
+    (ha : |a| < (2 : ℤ) ^ (w - 1)) : GenericRAM.Signed.Fits w a := by
+  have h := abs_lt.mp ha
+  exact ⟨hw, h.1.le, h.2⟩
+
+/-- A single coefficient is executed by real loads and signed arithmetic. The seven address
+computations fit whenever the one-past-end address fits. The two operands must fit the signed
+source range; the sum itself may use the two extra target bits supplied by the arithmetic block. -/
+theorem exec_summand {w : ℕ} (x : Data 32) (s : Fin 7) (c a v : ℤ) (base n : ℕ)
+    (hc : c = 0 ∨ c = 1 ∨ c = -1)
+    (hacc : x.regs accumulator = encode a) (hbase : x.regs group = base)
+    (hn : x.regs stride = n) (hmem : x.mem (base + s.val * n) = encode v)
+    (ha : GenericRAM.Signed.Fits w a) (hv : GenericRAM.Signed.Fits w v)
+    (haddr : Fits (w + 2) (base + 7 * n)) (hseven : Fits (w + 2) 7) :
+    ∃ y, ExecWithin (w + 2) (summand s c) x y 23 ∧
+      y.regs accumulator = encode (a + c * v) ∧ FormFrame x y := by
+  rcases hc with rfl | rfl | rfl
+  · refine ⟨x.set accumulator (x.regs accumulator), (ExecWithin.copy).mono (by decide), ?_, ?_⟩
+    · simp [hacc]
+    · refine ⟨rfl, ?_⟩
+      intro i _ _ hi _
+      simp only [Data.set_regs, Function.update_of_ne hi]
+  all_goals
+    have hs : Fits (w + 2) s.val := hseven.of_le (by omega)
+    have hmul : Fits (w + 2) (s.val * n) := haddr.of_le (by nlinarith [s.isLt])
+    have hsum : Fits (w + 2) (base + s.val * n) := haddr.of_le (by nlinarith [s.isLt])
+    let z := ((((x.set temporary s.val).set address (s.val * n)).set address
+      (base + s.val * n)).set right (encode v)).set left (encode a)
+    have hz : ExecWithin (w + 2)
+        (ram[ temporary ← #s.val; address ← temporary * stride;
+          address ← group + address; right ← *address; left ← accumulator ]) x z 5 := by
+      ram_eval [z, hs, hmul, hsum, hn, hbase, hacc, hmem,
+        temporary, address, group, stride, right, left, accumulator, Fin.mk.injEq]
+    have hza : z.regs left = encode a := by simp [z]
+    have hzv : z.regs right = encode v := by
+      simp [z, left, right]
+    have hzframe : FormFrame x z := by
+      refine ⟨rfl, ?_⟩
+      intro i hi hia hic hit
+      have hil : i ≠ left := by intro h; subst i; simp at hi
+      have hir : i ≠ right := by intro h; subst i; simp at hi
+      simp only [z, Data.set_regs, Function.update_of_ne hil, Function.update_of_ne hir,
+        Function.update_of_ne hia, Function.update_of_ne hit]
+  · obtain ⟨y, he, hyr, hym, hyreg⟩ := exec_add ha hv z hza hzv
+    refine ⟨y.set accumulator (y.regs result), ?_, ?_, ?_⟩
+    · simpa only [summand, show ¬(1 : ℤ) = 0 by decide, ↓reduceIte] using
+        (hz.seq (he.seq (ExecWithin.copy (d := accumulator) (s := result)))).mono
+          (by decide : 5 + (15 + 1) ≤ 23)
+    · simp [GenericRAM.Signed.Arithmetic.eval, hyr]
+    · refine ⟨hym.trans hzframe.1, ?_⟩
+      intro i hi hia hic hit
+      simpa only [Data.set_regs, Function.update_of_ne hic] using
+        (hyreg i (Or.inr hi)).trans (hzframe.2 i hi hia hic hit)
+  · obtain ⟨y, he, hyr, hym, hyreg⟩ := exec_subtract ha hv z hza hzv
+    refine ⟨y.set accumulator (y.regs result), ?_, ?_, ?_⟩
+    · simpa only [summand, show ¬(-1 : ℤ) = 0 by decide,
+        show ¬(-1 : ℤ) = 1 by decide, ↓reduceIte] using
+        (hz.seq (he.seq (ExecWithin.copy (d := accumulator) (s := result)))).mono
+          (by decide : 5 + (17 + 1) ≤ 23)
+    · simp [GenericRAM.Signed.Arithmetic.eval, hyr, sub_eq_add_neg]
+    · refine ⟨hym.trans hzframe.1, ?_⟩
+      intro i hi hia hic hit
+      simpa only [Data.set_regs, Function.update_of_ne hic] using
+        (hyreg i (Or.inr hi)).trans (hzframe.2 i hi hia hic hit)
+
+/-- Execute any finite list of the fixed digit/coefficients. Partial sums are bounded by
+`|a| + length * B`; the theorem derives each arithmetic operand's fit from that inequality. -/
+theorem exec_sumCode {w : ℕ} (hw : 0 < w) (pairs : List (Fin 7 × ℤ))
+    (x : Data 32) (a B : ℤ) (base n : ℕ) (v : Fin 7 → ℤ)
+    (hc : ∀ sc ∈ pairs, sc.2 = 0 ∨ sc.2 = 1 ∨ sc.2 = -1)
+    (hacc : x.regs accumulator = encode a) (hbase : x.regs group = base)
+    (hn : x.regs stride = n) (hmem : ∀ s, x.mem (base + s.val * n) = encode (v s))
+    (hB : 0 ≤ B) (hv : ∀ s, |v s| ≤ B) (hfitB : B < (2 : ℤ) ^ (w - 1))
+    (hfit : |a| + pairs.length * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (base + 7 * n)) (hseven : Fits (w + 2) 7) :
+    ∃ y, ExecWithin (w + 2) (sumCode pairs) x y (23 * pairs.length + 1) ∧
+      y.regs accumulator = encode (a + (pairs.map fun sc => sc.2 * v sc.1).sum) ∧
+      FormFrame x y := by
+  induction pairs generalizing x a with
+  | nil =>
+    refine ⟨x.set accumulator (x.regs accumulator), ExecWithin.copy, ?_, ?_⟩
+    · simpa using hacc
+    · refine ⟨rfl, ?_⟩
+      intro i _ _ hi _
+      simp only [Data.set_regs, Function.update_of_ne hi]
+  | cons sc rest ih =>
+    obtain ⟨s, c⟩ := sc
+    have hc0 := hc (s, c) (by simp)
+    have hcv : |c * v s| ≤ B := by
+      rcases hc0 with rfl | rfl | rfl
+      · simpa using hB
+      · simpa using hv s
+      · simpa using hv s
+    have ha : GenericRAM.Signed.Fits w a :=
+      fits_of_abs_lt hw (by have := abs_nonneg a; simp only [List.length_cons,
+        Nat.cast_add, Nat.cast_one] at hfit; nlinarith [Nat.cast_nonneg (α := ℤ) rest.length])
+    have hvs := fits_of_abs_lt hw ((hv s).trans_lt hfitB)
+    obtain ⟨y, he, hyacc, hyframe⟩ := exec_summand x s c a (v s) base n hc0 hacc
+      hbase hn (hmem s) ha hvs haddr hseven
+    have hybase : y.regs group = base := (hyframe.2 group (by decide) (by decide)
+      (by decide) (by decide)).trans hbase
+    have hyn : y.regs stride = n := (hyframe.2 stride (by decide) (by decide)
+      (by decide) (by decide)).trans hn
+    have hfit' : |a + c * v s| + rest.length * B < (2 : ℤ) ^ (w - 1) := by
+      have ht := abs_add_le a (c * v s)
+      simp only [List.length_cons, Nat.cast_add, Nat.cast_one] at hfit
+      nlinarith
+    obtain ⟨z, hz, hzacc, hzframe⟩ := ih y (a + c * v s)
+      (fun sc hsc => hc sc (by simp [hsc])) hyacc hybase hyn
+      (fun s => by rw [hyframe.1]; exact hmem s) hfit'
+    refine ⟨z, ?_, ?_, hyframe.trans hzframe⟩
+    · simpa only [sumCode, List.length_cons, Nat.mul_add, Nat.mul_one,
+        Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using he.seq hz
+    · simpa only [List.map_cons, List.sum_cons, add_assoc] using hzacc
+
+/-- A complete coefficient row, including initialization, costs at most 163 instructions.
+All seven entries have absolute value at most `B`, so every partial sum has magnitude at
+most `7B`; this ordinary explicit width condition is sufficient for every signed operation. -/
+theorem exec_form {w : ℕ} (hw : 0 < w) (side : Bool) (t : Fin 10)
+    (x : Data 32) (B : ℤ) (base n : ℕ) (v : Fin 7 → ℤ)
+    (hbase : x.regs group = base) (hn : x.regs stride = n)
+    (hmem : ∀ s, x.mem (base + s.val * n) = encode (v s))
+    (hB : 0 ≤ B) (hv : ∀ s, |v s| ≤ B) (hfit : 7 * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (base + 7 * n)) (hseven : Fits (w + 2) 7) :
+    ∃ y, ExecWithin (w + 2) (form side t) x y 163 ∧
+      y.regs accumulator = encode (∑ s, coefficients side t s * v s) ∧ FormFrame x y := by
+  let z := x.set accumulator 0
+  have hz : FormFrame x z := by
+    refine ⟨rfl, ?_⟩
+    intro i _ _ hi _
+    simp only [z, Data.set_regs, Function.update_of_ne hi]
+  obtain ⟨y, he, hacc, hf⟩ := exec_sumCode hw
+    (List.ofFn fun s => (s, coefficients side t s)) z 0 B base n v
+    (by intro sc hsc; obtain ⟨s, rfl⟩ := List.mem_ofFn.mp hsc; exact coefficients_values side t s)
+    (by simp [z, encode])
+    ((hz.2 group (by decide) (by decide) (by decide) (by decide)).trans hbase)
+    ((hz.2 stride (by decide) (by decide) (by decide) (by decide)).trans hn)
+    (by simpa only [z, Data.set_mem] using hmem) hB hv (by linarith)
+    (by simpa using hfit) haddr hseven
+  refine ⟨y, ?_, ?_, hz.trans hf⟩
+  · simpa only [form, List.length_ofFn] using
+      (ExecWithin.const (fits_zero (w := w + 2))).seq he
+  · simpa only [List.map_ofFn, List.sum_ofFn, Function.comp_apply, zero_add] using hacc
+
+/-- The finite term dispatch costs at most three instructions per inspected row in addition
+to the row's 163-instruction bound. All ten forms share the same native register file. -/
+theorem exec_dispatch {w : ℕ} (hw : 0 < w) (side : Bool) (rows : List (Fin 10))
+    (t : Fin 10) (ht : t ∈ rows) (x : Data 32) (B : ℤ) (base n : ℕ) (v : Fin 7 → ℤ)
+    (hterm : x.regs term = t.val) (hbase : x.regs group = base) (hn : x.regs stride = n)
+    (hmem : ∀ s, x.mem (base + s.val * n) = encode (v s))
+    (hB : 0 ≤ B) (hv : ∀ s, |v s| ≤ B) (hfit : 7 * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (base + 7 * n)) (hten : Fits (w + 2) 10) :
+    ∃ y, ExecWithin (w + 2) (dispatch side rows) x y (3 * rows.length + 163) ∧
+      y.regs accumulator = encode (∑ s, coefficients side t s * v s) ∧ FormFrame x y := by
+  induction rows generalizing x with
+  | nil => simp at ht
+  | cons q rest ih =>
+    let z := x.set temporary q.val
+    have hz : ExecWithin (B := .standard) (w + 2) (ram[ temporary ← #q.val ]) x z 1 :=
+      ExecWithin.const (hten.of_le (by omega))
+    have hzf : FormFrame x z := by
+      refine ⟨rfl, ?_⟩
+      intro i _ _ _ hi
+      simp only [z, Data.set_regs, Function.update_of_ne hi]
+    have hzt : z.regs term = t.val := by
+      simpa [z, term, temporary, Fin.mk.injEq] using hterm
+    have hzb : z.regs group = base := by
+      simpa [z, group, temporary, Fin.mk.injEq] using hbase
+    have hzn : z.regs stride = n := by
+      simpa [z, stride, temporary, Fin.mk.injEq] using hn
+    have hzm : ∀ s, z.mem (base + s.val * n) = encode (v s) := hmem
+    by_cases hqt : t = q
+    · subst t
+      obtain ⟨y, he, hacc, hf⟩ := exec_form hw side q z B base n v hzb hzn hzm hB hv
+        hfit haddr (hten.of_le (by decide))
+      refine ⟨y, ?_, hacc, hzf.trans hf⟩
+      apply (hz.seq (ExecWithin.branch_pos ?_ he)).mono
+      · simp only [List.length_cons]
+        omega
+      · simp only [Cond.holds_eq, hzt, z, Data.set_regs, Function.update_self]
+    · have htrest : t ∈ rest := (List.mem_cons.mp ht).resolve_left hqt
+      obtain ⟨y, he, hacc, hf⟩ := ih htrest z hzt hzb hzn hzm
+      refine ⟨y, ?_, hacc, hzf.trans hf⟩
+      apply (hz.seq (ExecWithin.branch_neg ?_ he)).mono
+      · simp only [List.length_cons]
+        omega
+      · simp only [Cond.holds_eq, hzt, z, Data.set_regs, Function.update_self]
+        exact fun h => hqt (Fin.ext h)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Header.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Header.lean
new file mode 100644
index 000000000..5beb51aaf
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Header.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+/-!
+# Charged initialization from the actual depth header
+
+## Main results
+
+* `Encoding.exec_setup`: load the header and compute both powers, buffer addresses and
+  loop parameters within `5L+18` native instructions, preserving every memory cell.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM
+
+/-- An explicit bound for the encoder's unsigned addresses, index products and counters. -/
+def addressBound (L : ℕ) : ℕ := L + 64 + 64 * 10 ^ L
+
+/-- Registers and memory after header initialization. This is only a postcondition; it
+contains no execution, resource or intermediate-fit assumption. -/
+structure SetupPost (L : ℕ) (x y : Data 32) : Prop where
+  /-- Memory is unchanged. -/
+  mem : y.mem = x.mem
+  /-- Depth loaded from memory address one. -/
+  depth : y.regs Encoding.depth = L
+  /-- Computed input size. -/
+  inputSize : y.regs Encoding.inputSize = 7 ^ L
+  /-- Computed buffer capacity. -/
+  capacity : y.regs Encoding.capacity = 10 ^ L
+  /-- First output address. -/
+  output : y.regs Encoding.output = outputBase L
+  /-- First scratch address. -/
+  scratch : y.regs Encoding.scratch = scratchBase L
+  /-- Original input base. -/
+  src : y.regs Encoding.src = 2
+  /-- First destination buffer. -/
+  dst : y.regs Encoding.dst = outputBase L
+  /-- First source suffix length. -/
+  stride : y.regs Encoding.stride = 7 ^ L
+  /-- The empty transformed prefix. -/
+  prefixes : y.regs Encoding.prefixes = 1
+  /-- No coordinates transformed yet. -/
+  stage : y.regs Encoding.stage = 0
+  /-- Counter increment. -/
+  one : y.regs Encoding.one = 1
+  /-- Input radix. -/
+  seven : y.regs Encoding.seven = 7
+  /-- Output radix. -/
+  ten : y.regs Encoding.ten = 10
+
+/-- Header loads, both power computations, address arithmetic and counter initialization
+are included. The only fit premise is the explicit bound on ordinary natural numbers. -/
+theorem exec_setup {w : ℕ} (L : ℕ) (x : Data 32) (hheader : x.mem 1 = L)
+    (haddr : Fits w (addressBound L)) :
+    ∃ y, ExecWithin w setup x y (5 * L + 18) ∧ SetupPost L x y := by
+  have h1 : Fits w 1 := haddr.of_le (by unfold addressBound; omega)
+  have h2 : Fits w 2 := haddr.of_le (by unfold addressBound; omega)
+  have h7 : Fits w 7 := haddr.of_le (by unfold addressBound; omega)
+  have h10 : Fits w 10 := haddr.of_le (by unfold addressBound; omega)
+  have hpow (b j : ℕ) (hb : b ≤ 10) (hj : j ≤ L) : Fits w (b ^ j) := by
+    apply haddr.of_le
+    have hbj := Nat.pow_le_pow_left hb j
+    have hjL := Nat.pow_le_pow_right (by decide : 1 ≤ (10 : ℕ)) hj
+    unfold addressBound
+    omega
+  let I (y : Data 32) : Prop :=
+    y.mem = x.mem ∧ y.regs depth = L ∧ y.regs inputSize = 7 ^ y.regs stage ∧
+      y.regs capacity = 10 ^ y.regs stage ∧ y.regs stage ≤ L ∧
+      y.regs one = 1 ∧ y.regs seven = 7 ∧ y.regs ten = 10
+  have hbody (y : Data 32) (hy : I y) (hc : (Cond.lt stage depth).Holds y) :
+      ∃ z, ExecWithin w powerBody y z 3 ∧ I z ∧ L - z.regs stage < L - y.regs stage := by
+    obtain ⟨hm, hd, hi, hcap, hj, ho, hs, ht⟩ := hy
+    have hjL : y.regs stage < L := by simpa only [Cond.holds_lt, hd] using hc
+    have hpi : Fits w (y.regs inputSize * y.regs seven) := by
+      rw [hi, hs, ← pow_succ]
+      exact hpow 7 _ (by decide) (by omega)
+    have hpc : Fits w (y.regs capacity * y.regs ten) := by
+      rw [hcap, ht, ← pow_succ]
+      exact hpow 10 _ (by decide) (by omega)
+    have hjfit : Fits w (y.regs stage + y.regs one) := by
+      rw [ho]
+      exact haddr.of_le (by unfold addressBound; omega)
+    have hpi' : Fits w (y.regs inputSize * 7) := by simpa only [hs] using hpi
+    have hpc' : Fits w (y.regs capacity * 10) := by simpa only [ht] using hpc
+    have hjfit' : Fits w (y.regs stage + 1) := by simpa only [ho] using hjfit
+    let z := ((y.set inputSize (y.regs inputSize * 7)).set capacity
+      (y.regs capacity * 10)).set stage (y.regs stage + 1)
+    have he : ExecWithin w powerBody y z 3 := by
+      ram_eval [powerBody, z, ho, hs, ht, hpi', hpc', hjfit',
+        inputSize, capacity, stage, one, seven, ten, Fin.mk.injEq]
+    refine ⟨z, he, ?_, ?_⟩
+    · refine ⟨hm, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [z, depth, inputSize, capacity, stage, Function.update_apply] using hd
+      · simp +decide [z, inputSize, capacity, stage, pow_succ, hi]
+      · simp +decide [z, inputSize, capacity, stage, pow_succ, hcap]
+      · simpa [z] using Nat.succ_le_of_lt hjL
+      · simpa +decide [z, one, inputSize, capacity, stage, Function.update_apply] using ho
+      · simpa +decide [z, seven, inputSize, capacity, stage, Function.update_apply] using hs
+      · simpa +decide [z, ten, inputSize, capacity, stage, Function.update_apply] using ht
+    · simp only [z, Data.set_regs, Function.update_self]
+      omega
+  let x0 := (((((((x.set one 1).set seven 7).set ten 10).set address 1).set depth L).set
+    inputSize 1).set capacity 1).set stage 0
+  have hx0 : I x0 := by
+    simp +decide [I, x0, depth, inputSize, capacity, stage, one, seven, ten, address]
+  have hxrun : ExecWithin w setupHead x x0 8 := by
+    ram_eval [setupHead, x0, hheader, h1, h7, h10, fits_zero,
+      one, seven, ten, address, depth, inputSize, capacity, stage, Fin.mk.injEq]
+  obtain ⟨u, hu, hi, hc⟩ := ExecWithin.loop_invariant I (fun y => L - y.regs stage) hbody hx0
+  obtain ⟨hm, hd, hin, hcap, hj, ho, hs, ht⟩ := hi
+  have hend : u.regs stage = L := by
+    simp only [Cond.holds_lt, hd] at hc
+    omega
+  rw [hend] at hin hcap
+  have hout : Fits w (2 + 7 ^ L) := haddr.of_le (by
+    have := Nat.pow_le_pow_left (by decide : 7 ≤ 10) L
+    unfold addressBound
+    omega)
+  have hscratch : Fits w (2 + 7 ^ L + 10 ^ L) := haddr.of_le (by
+    have := Nat.pow_le_pow_left (by decide : 7 ≤ 10) L
+    unfold addressBound
+    omega)
+  let y := (((((((u.set temporary 2).set output (outputBase L)).set scratch (scratchBase L)).set
+    src 2).set dst (outputBase L)).set stride (7 ^ L)).set prefixes 1).set stage 0
+  have hyrun : ExecWithin w setupTail u y 8 := by
+    ram_eval [setupTail, y, outputBase, scratchBase, hin, hcap, h2, h1, hout, hscratch,
+      temporary, output, scratch, src, dst, stride, prefixes, stage, inputSize, capacity,
+      Fin.mk.injEq]
+  refine ⟨y, ?_, ?_⟩
+  · have hcost : 8 + ((L - x0.regs stage) * (3 + 2) + 2 + 8) ≤ 5 * L + 18 := by
+      simp only [x0, Data.set_regs, Function.update_self, Nat.sub_zero]
+      omega
+    exact (hxrun.seq (hu.seq hyrun)).mono hcost
+  · constructor
+    all_goals simp +decide [y, outputBase, scratchBase, temporary, output, scratch, src, dst,
+      stride, prefixes, stage, depth, inputSize, capacity, one, seven, ten,
+      hm, hd, hin, hcap, ho, hs, ht]
+
+/-- The actual flat input fits the target machine. Each signed input value uses the existing
+canonical encoding; the depth and the ordinary unsigned length header are bounded separately. -/
+theorem input_fits {w L : ℕ} (hw : 0 < w) (a : Fin (7 ^ L) → ℤ) (A : ℤ)
+    (hA : 0 ≤ A) (ha : ∀ i, |a i| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) : InputFits (w + 2) (input L a) := by
+  have hpow : (1 : ℤ) ≤ (7 ^ L : ℕ) := by
+    exact_mod_cast Nat.one_le_pow L 7 (by decide)
+  have hAfit : A < (2 : ℤ) ^ (w - 1) := by nlinarith
+  refine ⟨?_, ?_⟩
+  · simp only [input, List.length_cons, List.length_ofFn]
+    apply haddr.of_le
+    have := Nat.pow_le_pow_left (by decide : 7 ≤ 10) L
+    unfold addressBound
+    omega
+  · intro v hv
+    rcases List.mem_cons.mp hv with rfl | hv
+    · exact haddr.of_le (by unfold addressBound; omega)
+    · obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hv
+      have hi : GenericRAM.Signed.Fits w (a i) := by
+        have h := abs_lt.mp ((ha i).trans_lt hAfit)
+        exact ⟨hw, h.1.le, h.2⟩
+      exact (Cslib.WordRAM.Signed.encode_fits hi).mono (by omega)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Input.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Input.lean
new file mode 100644
index 000000000..727d0f96f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Input.lean
@@ -0,0 +1,127 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Exec
+import Mathlib.Data.List.GetD
+
+/-!
+# Actual initialized-input clients for the shared encoders
+
+## Main results
+
+* `Encoding.exec_input`: flat signed array, concrete depth header and actual `State.init`.
+* `Encoding.exec_left`, `Encoding.exec_right`: all public tensor encodings, at every depth.
+
+The two programs and their thirty-two registers are independent of depth and word width.
+Inputs are signed words encoded with `WordRAM.Signed.encode`; the depth and the machine's
+length header are ordinary unsigned words. All input and reachable data words fit the target
+width. Output and scratch are disjoint concrete blocks immediately after the input.
+
+## References
+
+The encodings are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open CoordinateTransform
+
+private theorem getD_ofFn {N : ℕ} (f : Fin N → ℤ) (i : Fin N) :
+    (List.ofFn f).getD i.val 0 = f i := by
+  rw [List.getD_eq_getElem _ _ (by simp)]
+  simp
+
+/-- The complete native encoder starts from the ordinary `State.init` convention with a
+real depth header and encoded input words. It returns all flat shared-transform values, keeps
+the input and every outside cell, and leaves only target-sized words in memory and registers. -/
+theorem exec_input {w L : ℕ} (hw : 0 < w) (side : Bool) (a : Fin (7 ^ L) → ℤ)
+    (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i, |a i| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    InputFits (w + 2) (input L a) ∧
+    ∃ y, ExecWithin (w + 2) (program side) (State.init (input L a)).data y (timeBound L) ∧
+      y.Bounded (w + 2) ∧
+      (∀ p < 10 ^ L, y.mem (outputBase L + p) = encode
+        (value (table (coefficients side)) L 0 (fun i => (List.ofFn a).getD i 0) p 0)) ∧
+      (∀ b, ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) →
+        y.mem b = (State.init (input L a) : State 32).data.mem b) ∧
+      y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L := by
+  have hi := input_fits hw a A hA ha hmag haddr
+  let x : Data 32 := (State.init (input L a)).data
+  have hheader : x.mem 1 = L := by
+    simp [x, State.init, Data.init, input]
+  have hinput (i : ℕ) (hi : i < 7 ^ L) :
+      x.mem (2 + i) = encode ((List.ofFn a).getD i 0) := by
+    have hidx : 2 + i = (i + 1) + 1 := by omega
+    change (Data.init (input L a) : Data 32).mem (2 + i) = _
+    rw [hidx, Data.init_mem_succ]
+    simp only [input, List.getD_cons_succ]
+    rw [List.getD_eq_getElem _ _ (by simpa only [List.length_ofFn] using hi)]
+    simpa using congrArg encode (getD_ofFn a ⟨i, hi⟩).symm
+  have ha' (i : ℕ) (hi : i < 7 ^ L) : |(List.ofFn a).getD i 0| ≤ A := by
+    rw [getD_ofFn a ⟨i, hi⟩]
+    exact ha _
+  obtain ⟨y, he, hv, hf, ho, hc⟩ := exec hw side (fun i => (List.ofFn a).getD i 0) x
+    hheader hinput A hA ha' hmag haddr
+  exact ⟨hi, y, he, he.bounded (Data.Bounded.init hi), hv, hf, ho, hc⟩
+
+/-- Complete left encoder on arbitrary signed arrays indexed by the original seven-symbol
+strings. Every one of the `10^L` leaves receives the unchanged public `encodingL` value. -/
+theorem exec_left {w L : ℕ} (hw : 0 < w) (a : LeftStr L → ℤ) (A : ℤ)
+    (hA : 0 ≤ A) (ha : ∀ u, |a u| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    InputFits (w + 2) (inputL a) ∧
+    ∃ y, ExecWithin (w + 2) (program false) (State.init (inputL a)).data y (timeBound L) ∧
+      y.Bounded (w + 2) ∧
+      (∀ τ, y.mem (outputBase L + (leafIndex τ).val) = encode (encodingL a τ)) ∧
+      (∀ b, ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) →
+        y.mem b = (State.init (inputL a) : State 32).data.mem b) ∧
+      y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L := by
+  let f : Fin (7 ^ L) → ℤ := fun i => a (fun ℓ => leftAt (finFunctionFinEquiv.symm i ℓ))
+  obtain ⟨hi, y, he, hb, hv, hf, ho, hc⟩ := exec_input hw false f A hA (fun _ => ha _) hmag haddr
+  refine ⟨hi, y, he, hb, ?_, hf, ho, hc⟩
+  intro τ
+  have harr (u : Fin L → Fin 7) : (List.ofFn f).getD (finFunctionFinEquiv u).val 0 =
+      a (fun i => leftAt (u i)) := by
+    rw [getD_ofFn]
+    simp only [f, Equiv.symm_apply_apply]
+  have h := hv (leafIndex τ) (leafIndex τ).isLt
+  rw [value_final_left a _ harr τ] at h
+  exact h
+
+/-- Complete right encoder on arbitrary signed arrays with the original `encodingR` API. -/
+theorem exec_right {w L : ℕ} (hw : 0 < w) (a : RightStr L → ℤ) (A : ℤ)
+    (hA : 0 ≤ A) (ha : ∀ u, |a u| ≤ A)
+    (hmag : (7 ^ L : ℕ) * A < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (addressBound L)) :
+    InputFits (w + 2) (inputR a) ∧
+    ∃ y, ExecWithin (w + 2) (program true) (State.init (inputR a)).data y (timeBound L) ∧
+      y.Bounded (w + 2) ∧
+      (∀ τ, y.mem (outputBase L + (leafIndex τ).val) = encode (encodingR a τ)) ∧
+      (∀ b, ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) →
+        y.mem b = (State.init (inputR a) : State 32).data.mem b) ∧
+      y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L := by
+  let f : Fin (7 ^ L) → ℤ := fun i => a (fun ℓ => rightAt (finFunctionFinEquiv.symm i ℓ))
+  obtain ⟨hi, y, he, hb, hv, hf, ho, hc⟩ := exec_input hw true f A hA (fun _ => ha _) hmag haddr
+  refine ⟨hi, y, he, hb, ?_, hf, ho, hc⟩
+  intro τ
+  have harr (u : Fin L → Fin 7) : (List.ofFn f).getD (finFunctionFinEquiv u).val 0 =
+      a (fun i => rightAt (u i)) := by
+    rw [getD_ofFn]
+    simp only [f, Equiv.symm_apply_apply]
+  have h := hv (leafIndex τ) (leafIndex τ).isLt
+  rw [value_final_right a _ harr τ] at h
+  exact h
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Meaning.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Meaning.lean
new file mode 100644
index 000000000..a22fed233
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Meaning.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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Stage
+public import Complexity.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform
+
+/-!
+# Agreement of the flat tensor transform with the public encodings
+
+The digit numbering is supplied by Mathlib's `finFunctionFinEquiv`. The explicit alphabet
+numberings contain exactly the original seven variables and ten terms. The final mixed-radix
+transform is `encodingL` or `encodingR` for every depth, including zero.
+
+## Main results
+
+* `Encoding.value_final_left`, `Encoding.value_final_right`: unchanged public encoding semantics.
+
+## References
+
+The original encodings and coefficients are from [AlmanWilliams2026, Section 2.4.1], selectively
+adapted from Anthropic, PBC's formal source; see `Encoding` for the exact pin and paths.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open CoordinateTransform
+
+/-- The numbered output position of a term string. -/
+def leafIndex {L : ℕ} (τ : Leaf L) : Fin (10 ^ L) :=
+  finFunctionFinEquiv fun i => termDigits.symm (τ i)
+
+private theorem value_final_alphabet {α : Type} [Fintype α] (e : Fin 7 ≃ α)
+    (c : Term → α → ℤ) {L : ℕ} (a : (Fin L → α) → ℤ) (arr : ℕ → ℤ)
+    (harr : ∀ u : Fin L → Fin 7, arr (finFunctionFinEquiv u) = a (fun i => e (u i)))
+    (τ : Leaf L) :
+    value (table (fun t s => c (termAt t) (e s))) L 0 arr (leafIndex τ) 0 =
+      encodeWith c τ a := by
+  have h := value_final (fun t s => c (termAt t) (e s)) L
+    (fun u => a (fun i => e (u i))) arr harr (fun i => termDigits.symm (τ i))
+  change value (table (fun t s => c (termAt t) (e s))) L 0 arr
+    (finFunctionFinEquiv fun i => termDigits.symm (τ i)) 0 = _
+  rw [h]
+  unfold encodeWith
+  refine Fintype.sum_equiv (Equiv.piCongrRight fun _ : Fin L => e) _ _ ?_
+  intro u
+  congr 1
+  apply Finset.prod_congr rfl
+  intro i _
+  change c (termDigits (termDigits.symm (τ i))) (e (u i)) = c (τ i) (e (u i))
+  rw [Equiv.apply_symm_apply]
+
+/-- The flat shared left transform equals the existing `encodingL` on every leaf. -/
+theorem value_final_left {L : ℕ} (a : LeftStr L → ℤ) (arr : ℕ → ℤ)
+    (harr : ∀ u : Fin L → Fin 7, arr (finFunctionFinEquiv u) = a (fun i => leftAt (u i)))
+    (τ : Leaf L) :
+    value (table (coefficients false)) L 0 arr (leafIndex τ) 0 = encodingL a τ :=
+  value_final_alphabet leftDigits phi a arr harr τ
+
+/-- The flat shared right transform equals the existing `encodingR` on every leaf. -/
+theorem value_final_right {L : ℕ} (a : RightStr L → ℤ) (arr : ℕ → ℤ)
+    (harr : ∀ u : Fin L → Fin 7, arr (finFunctionFinEquiv u) = a (fun i => rightAt (u i)))
+    (τ : Leaf L) :
+    value (table (coefficients true)) L 0 arr (leafIndex τ) 0 = encodingR a τ :=
+  value_final_alphabet rightDigits psi a arr harr τ
+
+/-- The native stage's row-wise specification is the next shared-prefix value. This includes
+the quotient/remainder decomposition of its actual flat loop counter. -/
+theorem stageResult_value (side : Bool) (j k i : ℕ) (arr : ℕ → ℤ) :
+    stageResult side (7 ^ k)
+      (fun i a => value (table (coefficients side)) j (k + 1) arr
+        (i / (10 * 7 ^ k)) (a.val * 7 ^ k + i % 7 ^ k)) i =
+      value (table (coefficients side)) (j + 1) k arr (i / 7 ^ k) (i % 7 ^ k) := by
+  have hdiv : i / 7 ^ k / 10 = i / (10 * 7 ^ k) := by
+    rw [Nat.div_div_eq_div_mul, Nat.mul_comm (7 ^ k) 10]
+  have hprefix : i / (10 * 7 ^ k) * 10 + i / 7 ^ k % 10 = i / 7 ^ k := by
+    simpa only [hdiv, Nat.mul_comm] using Nat.div_add_mod (i / 7 ^ k) 10
+  have he := value_step (table (coefficients side)) j k arr (i / (10 * 7 ^ k))
+    (i % 7 ^ k) (Nat.mod_lt (i / 7 ^ k) (by decide : 0 < 10))
+  rw [hprefix] at he
+  unfold stageResult
+  rw [he, ← Fin.sum_univ_eq_sum_range]
+  apply Finset.sum_congr rfl
+  intro a _
+  simp only [table, Nat.mod_mod, Nat.mod_eq_of_lt a.isLt]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Stage.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Stage.lean
new file mode 100644
index 000000000..85c382fd0
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Stage.lean
@@ -0,0 +1,203 @@
+/-
+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.WordRAM.MatrixMultiplication.Schonhage.Cell
+
+/-!
+# Charged shared-coordinate array loop
+
+## Main results
+
+* `Encoding.exec_cells`: all cells in one shared coordinate transform, preserving the input
+  and every memory cell outside the destination block.
+
+## References
+
+The forms are from [AlmanWilliams2026, Section 2.4.1]; see `Encoding` for provenance.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+
+/-- The linear-form value at flat output position `i` of a stage with suffix stride `n`. -/
+def stageResult (side : Bool) (n : ℕ) (v : ℕ → Fin 7 → ℤ) (i : ℕ) : ℤ :=
+  ∑ a, coefficients side ⟨i / n % 10, Nat.mod_lt _ (by decide)⟩ a * v i a
+
+/-- The complete cell loop has at most `207 * (10 * P * n) + 2` instructions. The seven
+source entries for each output are shared values from the previous array, not separately
+enumerated original input terms. Disjointness is permitted in either address order. -/
+theorem exec_cells {w : ℕ} (hw : 0 < w) (side : Bool) (x : Data 32)
+    (P n s d : ℕ) (hP : 0 < P) (hnpos : 0 < n)
+    (hsrc : x.regs src = s) (hdst : x.regs dst = d) (hcell : x.regs cell = 0)
+    (hn : x.regs stride = n) (hseven : x.regs seven = 7)
+    (hten : x.regs ten = 10) (hone : x.regs one = 1)
+    (hsize : x.regs stageSize = 10 * P * n)
+    (v : ℕ → Fin 7 → ℤ) (B : ℤ) (hB : 0 ≤ B) (hv : ∀ i < 10 * P * n, ∀ a, |v i a| ≤ B)
+    (hmem : ∀ i < 10 * P * n, ∀ a,
+      x.mem (s + (i / (10 * n) * 7 + a.val) * n + i % n) = encode (v i a))
+    (hval : 7 * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (s + d + 64 + 64 * P * n))
+    (hdisj : s + 7 * P * n ≤ d ∨ d + 10 * P * n ≤ s) :
+    ∃ y, ExecWithin (w + 2) (.loop (.lt cell stageSize) (cellBody side)) x y
+        (207 * (10 * P * n) + 2) ∧
+      (∀ i < 10 * P * n, y.mem (d + i) = encode (stageResult side n v i)) ∧
+      (∀ a, ¬(d ≤ a ∧ a < d + 10 * P * n) → y.mem a = x.mem a) ∧
+      (∀ a, 9 ≤ a.val → ¬CellLocal a → y.regs a = x.regs a) := by
+  let N := 10 * P * n
+  let I (y : Data 32) : Prop :=
+    (∀ a, 9 ≤ a.val → ¬CellLocal a → y.regs a = x.regs a) ∧ y.regs cell ≤ N ∧
+      (∀ i < y.regs cell, y.mem (d + i) = encode (stageResult side n v i)) ∧
+      (∀ a, ¬(d ≤ a ∧ a < d + y.regs cell) → y.mem a = x.mem a)
+  have hbody (y : Data 32) (hy : I y) (hc : (Cond.lt cell stageSize).Holds y) :
+      ∃ z, ExecWithin (w + 2) (cellBody side) y z 205 ∧ I z ∧
+        N - z.regs cell < N - y.regs cell := by
+    obtain ⟨hr, hiN, hm, hf⟩ := hy
+    have hys : y.regs src = s := (hr src (by decide) (by decide)).trans hsrc
+    have hyd : y.regs dst = d := (hr dst (by decide) (by decide)).trans hdst
+    have hyn : y.regs stride = n := (hr stride (by decide) (by decide)).trans hn
+    have hy7 : y.regs seven = 7 := (hr seven (by decide) (by decide)).trans hseven
+    have hy10 : y.regs ten = 10 := (hr ten (by decide) (by decide)).trans hten
+    have hy1 : y.regs one = 1 := (hr one (by decide) (by decide)).trans hone
+    have hysz : y.regs stageSize = N := (hr stageSize (by decide) (by decide)).trans hsize
+    have hi : y.regs cell < N := by simpa only [Cond.holds_lt, hysz] using hc
+    have hyinput (a : Fin 7) :
+        y.mem (s + (y.regs cell / (10 * n) * 7 + a.val) * n + y.regs cell % n) =
+          encode (v (y.regs cell) a) := by
+      have hp : y.regs cell / (10 * n) < P := by
+        apply (Nat.div_lt_iff_lt_mul (by positivity : 0 < 10 * n)).mpr
+        dsimp only [N] at hi
+        nlinarith
+      have hmod := Nat.mod_lt (y.regs cell) hnpos
+      have hprefix : y.regs cell / (10 * n) * 7 + a.val < P * 7 := by omega
+      have hproduct := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hprefix)
+      have hoff : (y.regs cell / (10 * n) * 7 + a.val) * n + y.regs cell % n <
+          P * 7 * n := by nlinarith only [hproduct, hmod]
+      rw [Nat.mul_comm P 7] at hoff
+      rw [hf _ ?_]
+      · exact hmem _ hi a
+      · rcases hdisj with h | h <;> dsimp only [N] at hiN <;> omega
+    obtain ⟨z, he, hzmem, hzcell, hzreg⟩ := exec_cell hw side y P n s d (y.regs cell)
+      hP hnpos hi hys hyd rfl hyn hy7 hy10 hy1 (v (y.regs cell)) B hB (hv _ hi)
+      hyinput hval haddr
+    refine ⟨z, he, ?_, by rw [hzcell]; omega⟩
+    refine ⟨fun a ha hl => (hzreg a ha hl).trans (hr a ha hl), by omega, ?_, ?_⟩
+    · intro i hzi
+      rw [hzcell] at hzi
+      by_cases hic : i = y.regs cell
+      · subst i
+        simp only [hzmem, Function.update_self, stageResult]
+      · have hin : i < y.regs cell := by omega
+        rw [hzmem, Function.update_of_ne (by omega : d + i ≠ d + y.regs cell)]
+        exact hm i hin
+    · intro a ha
+      rw [hzcell] at ha
+      have hne : a ≠ d + y.regs cell := by omega
+      rw [hzmem, Function.update_of_ne hne]
+      exact hf a (by omega)
+  have hx : I x := by
+    refine ⟨fun _ _ _ => rfl, by simp [hcell, N], ?_, ?_⟩
+    · simp only [hcell, Nat.not_lt_zero, false_implies, implies_true]
+    · intro a _
+      rfl
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I (fun y => N - y.regs cell) hbody hx
+  obtain ⟨hr, hi, hm, hf⟩ := hy
+  have hysz : y.regs stageSize = N := (hr stageSize (by decide) (by decide)).trans hsize
+  have hend : y.regs cell = N := by
+    simp only [Cond.holds_lt, hysz] at hc
+    omega
+  refine ⟨y, ?_, ?_, ?_, hr⟩
+  · simpa only [hcell, N, Nat.sub_zero, Nat.add_comm, Nat.mul_comm] using he
+  · simpa only [hend] using hm
+  · simpa only [hend] using hf
+
+/-- Registers changed by the stage controller or its cell loop. -/
+def StageLocal (i : Fin 32) : Prop :=
+  CellLocal i ∨ i = stride ∨ i = stageSize ∨ i = src ∨ i = dst ∨ i = prefixes ∨ i = stage
+
+instance (i : Fin 32) : Decidable (StageLocal i) :=
+  inferInstanceAs (Decidable (CellLocal i ∨ i = stride ∨ i = stageSize ∨ i = src ∨
+    i = dst ∨ i = prefixes ∨ i = stage))
+
+private theorem stage_preserves (side : Bool) (i : Fin 32) :
+    9 ≤ i.val → ¬StageLocal i → (stageBody side).Preserves i := by
+  decide +kernel +revert
+
+/-- A complete coordinate stage, including stride division, stage-size arithmetic, both
+cell-loop control instructions per entry, buffer alternation and the next-stage counters. -/
+theorem exec_stageBody {w : ℕ} (hw : 0 < w) (side : Bool) (x : Data 32)
+    (P n s d j o q : ℕ) (hP : 0 < P) (hnpos : 0 < n)
+    (hsrc : x.regs src = s) (hdst : x.regs dst = d) (hj : x.regs stage = j)
+    (hn : x.regs stride = 7 * n) (hp : x.regs prefixes = P)
+    (hseven : x.regs seven = 7) (hten : x.regs ten = 10) (hone : x.regs one = 1)
+    (hout : x.regs output = o) (hscratch : x.regs scratch = q)
+    (v : ℕ → Fin 7 → ℤ) (B : ℤ) (hB : 0 ≤ B) (hv : ∀ i < 10 * P * n, ∀ a, |v i a| ≤ B)
+    (hmem : ∀ i < 10 * P * n, ∀ a,
+      x.mem (s + (i / (10 * n) * 7 + a.val) * n + i % n) = encode (v i a))
+    (hval : 7 * B < (2 : ℤ) ^ (w - 1))
+    (haddr : Fits (w + 2) (s + d + 64 + 64 * P * n)) (hjfit : Fits (w + 2) (j + 1))
+    (hdisj : s + 7 * P * n ≤ d ∨ d + 10 * P * n ≤ s) :
+    ∃ y, ExecWithin (w + 2) (stageBody side) x y (207 * (10 * P * n) + 12) ∧
+      (∀ i < 10 * P * n, y.mem (d + i) = encode (stageResult side n v i)) ∧
+      (∀ a, ¬(d ≤ a ∧ a < d + 10 * P * n) → y.mem a = x.mem a) ∧
+      y.regs src = d ∧ y.regs dst = (if d = o then q else o) ∧
+      y.regs stride = n ∧ y.regs prefixes = 10 * P ∧ y.regs stage = j + 1 ∧
+      (∀ a, 9 ≤ a.val → ¬StageLocal a → y.regs a = x.regs a) := by
+  have hPn : n ≤ P * n := by nlinarith
+  have h10P : Fits (w + 2) (P * 10) := haddr.of_le (by nlinarith)
+  have hN : Fits (w + 2) (P * 10 * n) := haddr.of_le (by nlinarith)
+  have hnfit : Fits (w + 2) n := haddr.of_le (by nlinarith)
+  have hdiv : 7 * n / 7 = n := by omega
+  let z := (((x.set stride n).set stageSize (P * 10)).set stageSize (P * 10 * n)).set cell 0
+  have hz : ExecWithin (w + 2) stageHead x z 4 := by
+    ram_eval [stageHead, z, hn, hseven, hp, hten, hdiv, hnfit, h10P, hN,
+      stride, prefixes, ten, seven, stageSize, cell, Fin.mk.injEq]
+  have hzr (a : Fin 32) (ha : a ≠ stride ∧ a ≠ stageSize ∧ a ≠ cell) :
+      z.regs a = x.regs a := by
+    simp only [z, Data.set_regs, Function.update_of_ne ha.1, Function.update_of_ne ha.2.1,
+      Function.update_of_ne ha.2.2]
+  obtain ⟨u, hu, hum, huf, hur⟩ := exec_cells hw side z P n s d hP hnpos
+    ((hzr src (by decide)).trans hsrc) ((hzr dst (by decide)).trans hdst)
+    (by simp [z]) (by simp [z, stride, stageSize, cell])
+    ((hzr seven (by decide)).trans hseven) ((hzr ten (by decide)).trans hten)
+    ((hzr one (by decide)).trans hone)
+    (by simp [z, stageSize, cell, Nat.mul_comm]) v B hB hv hmem hval haddr hdisj
+  have ur (a : Fin 32) (ha : 9 ≤ a.val) (hl : ¬CellLocal a)
+      (hzl : a ≠ stride ∧ a ≠ stageSize ∧ a ≠ cell) : u.regs a = x.regs a :=
+    (hur a ha hl).trans (hzr a hzl)
+  have us : u.regs dst = d := (ur dst (by decide) (by decide) (by decide)).trans hdst
+  have uo : u.regs output = o := (ur output (by decide) (by decide) (by decide)).trans hout
+  have uq : u.regs scratch = q := (ur scratch (by decide) (by decide) (by decide)).trans hscratch
+  have up : u.regs prefixes = P := (ur prefixes (by decide) (by decide) (by decide)).trans hp
+  have uj : u.regs stage = j := (ur stage (by decide) (by decide) (by decide)).trans hj
+  have ut : u.regs ten = 10 := (ur ten (by decide) (by decide) (by decide)).trans hten
+  have u1 : u.regs one = 1 := (ur one (by decide) (by decide) (by decide)).trans hone
+  have un : u.regs stride = n := by
+    rw [hur stride (by decide) (by decide)]
+    simp [z, stride, stageSize, cell]
+  let y := (((u.set src d).set dst (if d = o then q else o)).set prefixes (P * 10)).set
+    stage (j + 1)
+  have hy : ExecWithin (w + 2) stageTail u y 6 := by
+    by_cases hdo : d = o
+    all_goals ram_eval [stageTail, y, us, uo, uq, up, uj, ut, u1, hdo, h10P, hjfit,
+      src, dst, output, scratch, prefixes, stage, ten, one, Fin.mk.injEq]
+  have he : ExecWithin (w + 2) (stageBody side) x y (207 * (10 * P * n) + 12) :=
+    (hz.seq (hu.seq hy)).mono (by omega)
+  refine ⟨y, he, hum, huf, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · simp [y, src, dst, prefixes, stage]
+  · simp [y, dst, prefixes, stage]
+  · simpa [y, src, dst, prefixes, stage, stride] using un
+  · simp [y, prefixes, stage, Nat.mul_comm]
+  · simp [y]
+  · intro a ha hl
+    exact he.regs_eq (stage_preserves side a ha hl)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
diff --git a/Complexity/Computability/WordRAM/Copy.lean b/Complexity/Computability/WordRAM/Copy.lean
index 62e6600b3..1652067c0 100644
--- a/Complexity/Computability/WordRAM/Copy.lean
+++ b/Complexity/Computability/WordRAM/Copy.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Copyright (c) 2026 Samuel Schlesinger, Erik Demaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Samuel Schlesinger
+Authors: Samuel Schlesinger, Erik Demaine
 -/
 
 module
@@ -10,10 +10,10 @@ module
 public import Complexity.Computability.WordRAM.Allocation
 
 /-!
-# Copying disjoint arrays on the word RAM
+# Copying arrays on the word RAM
 
 The seven-register copy routine charges every address calculation, load, store, increment,
-and loop test. Its source precedes its destination, as in a bump-allocated growing array.
+and loop test. Source and destination may be disjoint in either order or equal.
 It is a fixed program: neither the length nor either address is baked into the code.
 
 ## Main definitions
@@ -29,6 +29,8 @@ It is a fixed program: neither the length nor either address is baked into the c
 
 * `Cslib.WordRAM.ArrayCopy.exec`: copying `n` words within `7 * n + 4` instructions,
   preserving the source and all cells outside the destination.
+* `Cslib.WordRAM.ArrayCopy.exec_of_separated_or_eq`: the same native program also supports
+  disjoint blocks in the reverse address order or identical source and destination.
 
 ## References
 
@@ -39,7 +41,7 @@ It is a fixed program: neither the length nor either address is baked into the c
 
 namespace Cslib.WordRAM.ArrayCopy
 
-/-- The memory after copying a prefix into a disjoint destination block. -/
+/-- The memory after copying a prefix into a destination block. -/
 def copyPrefix (mem : ℕ → ℕ) (src dst k : ℕ) : ℕ → ℕ :=
   fun a => if dst ≤ a ∧ a < dst + k then mem (src + (a - dst)) else mem a
 
@@ -94,10 +96,11 @@ def program : Code .standard 7 := ram[ idx ← #0; one ← #1; while idx < len d
 /-- Low-level structured copying charges register setup and all loop instructions, excluding
 the final halt. The one-past-end addresses must fit a word. Boundedness of the input memory and
 registers is a separate premise when using `ExecWithin.bounded` to obtain bounded-word execution. -/
-theorem exec {w : ℕ} (x : Data 7) (h1 : Fits w 1)
+theorem exec_of_separated_or_eq {w : ℕ} (x : Data 7) (h1 : Fits w 1)
     (hs : Fits w (x.regs src + x.regs len))
     (hd : Fits w (x.regs dst + x.regs len))
-    (hdisj : x.regs src + x.regs len ≤ x.regs dst) :
+    (hdisj : x.regs src + x.regs len ≤ x.regs dst ∨
+      x.regs dst + x.regs len ≤ x.regs src ∨ x.regs src = x.regs dst) :
     ∃ y, ExecWithin w program x y (7 * x.regs len + 4) ∧
       y.mem = copyPrefix x.mem (x.regs src) (x.regs dst) (x.regs len) ∧
       y.regs src = x.regs src ∧ y.regs dst = x.regs dst ∧ y.regs len = x.regs len := by
@@ -118,7 +121,7 @@ theorem exec {w : ℕ} (x : Data 7) (h1 : Fits w 1)
     have hread : y.mem (y.regs src + y.regs idx) = x.mem (x.regs src + y.regs idx) := by
       rw [hym, hys]
       apply copyPrefix_outside
-      omega
+      rcases hdisj with h | h | h <;> omega
     refine ⟨?z, ?run, ?inv, ?decrease⟩
     case run => ram_eval [body, hsrc, hdst, hinc, hyo]
     case inv =>
@@ -150,6 +153,16 @@ theorem exec {w : ℕ} (x : Data 7) (h1 : Fits w 1)
       omega
   · simpa [hend] using hym
 
+/-- Forward copying between disjoint arrays, retaining the original calling convention. -/
+theorem exec {w : ℕ} (x : Data 7) (h1 : Fits w 1)
+    (hs : Fits w (x.regs src + x.regs len))
+    (hd : Fits w (x.regs dst + x.regs len))
+    (hdisj : x.regs src + x.regs len ≤ x.regs dst) :
+    ∃ y, ExecWithin w program x y (7 * x.regs len + 4) ∧
+      y.mem = copyPrefix x.mem (x.regs src) (x.regs dst) (x.regs len) ∧
+      y.regs src = x.regs src ∧ y.regs dst = x.regs dst ∧ y.regs len = x.regs len :=
+  exec_of_separated_or_eq x h1 hs hd (Or.inl hdisj)
+
 end Cslib.WordRAM.ArrayCopy
 
 end
diff --git a/ComplexityTests/SchonhageEncoding.lean b/ComplexityTests/SchonhageEncoding.lean
new file mode 100644
index 000000000..6f9d10937
--- /dev/null
+++ b/ComplexityTests/SchonhageEncoding.lean
@@ -0,0 +1,142 @@
+/-
+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
+-/
+
+import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Flat
+
+-- Full-program regressions intentionally evaluate the native interpreter at elaboration time.
+set_option linter.hashCommand false
+
+/-!
+# Executed native shared-encoding regressions
+
+These clients start with the actual unsigned input convention. The interpreter charges every
+native arithmetic block, branch, loop and store. They compare observable memory after execution.
+-/
+
+namespace ComplexityTests.SchonhageEncoding
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding
+
+private def observe (side : Bool) (w L fuel : ℕ) (a : Fin (7 ^ L) → ℤ) :
+    Option ((List ℤ × Bool) × ℕ) :=
+  ((program side).eval w fuel (State.init (input L a)).data).map fun (y, time) =>
+    (((List.range (10 ^ L)).map fun i => decode (y.mem (outputBase L + i)),
+      decide (y.mem 0 = (input L a).length ∧ y.mem 1 = L ∧
+        (∀ i : Fin (7 ^ L), y.mem (2 + i.val) = encode (a i)) ∧
+        y.mem (scratchBase L + 10 ^ L) = 0)), time)
+
+-- Kernel reduction follows the finite form dispatch and all actual signed arithmetic blocks.
+-- Its nested code and loop reductions exceed the default elaborator recursion depth.
+set_option maxRecDepth 16384 in
+example : observe false 8 0 2 (fun _ => -3) = some (([-3], true), 31) := by
+  decide +kernel
+
+-- These checks run the actual interpreter as regression tests; the general execution
+-- theorems are kernel checked separately. VM evaluation avoids quadratic kernel reduction
+-- through thousands of functional register updates in each concrete full-program test.
+#guard (observe false 12 1 16 (fun i => (i.val : ℤ) + 1)).map Prod.fst ==
+  some ([5, 6, 1, 8, 9, 2, -7, -9, 3, -6], true)
+
+#guard (observe true 12 1 16 (fun i => (i.val : ℤ) + 1)).map Prod.fst ==
+  some ([5, 7, -6, 7, 9, -10, 1, 2, 3, 6], true)
+
+#guard (observe false 12 1 16 (fun i => -((i.val : ℤ) + 1))).map Prod.fst ==
+  some ([-5, -6, -1, -8, -9, -2, 7, 9, -3, 6], true)
+
+-- At width four, the computed scratch address 19 overflows; width five is the first working
+-- width for this zero-valued depth-one client. Every output and the adjacent frame are checked.
+#guard observe false 4 1 16 (fun _ => 0) == none
+#guard (observe false 5 1 16 (fun _ => 0)).map Prod.fst ==
+  some (List.replicate 10 0, true)
+
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+private def signedLeft (u : LeftStr 2) : ℤ :=
+  if u 0 = .x 0 then -2 else if u 1 = .p 1 0 then 3 else 1
+
+private def signedRight (u : RightStr 2) : ℤ :=
+  if u 0 = .q 0 1 then -3 else if u 1 = .y 2 then 2 else 0
+
+private def leafAt (i : Fin (10 ^ 2)) : Leaf 2 :=
+  fun ℓ => termAt (finFunctionFinEquiv.symm i ℓ)
+
+-- Output addresses can be calculated by ordinary executable finite alphabet numberings.
+#guard (leafIndex (fun _ : Fin 2 => Term.P0)).val == 99
+#guard (leafIndex (fun _ : Fin 2 => Term.P 0 0)).val == 0
+#guard (leftDigits.symm (.p 1 1)).val == 6
+
+-- Two stages alternate buffers and then copy backward from scratch to output. The expected
+-- values use the unchanged public mathematical encodings, including every one of the 100 leaves.
+#guard (observe false 16 2 128 (fun i => signedLeft
+    (fun ℓ => leftAt (finFunctionFinEquiv.symm i ℓ)))).map Prod.fst ==
+  some (List.ofFn (fun i => encodingL signedLeft (leafAt i)), true)
+
+#guard (observe true 16 2 128 (fun i => signedRight
+    (fun ℓ => rightAt (finFunctionFinEquiv.symm i ℓ)))).map Prod.fst ==
+  some (List.ofFn (fun i => encodingR signedRight (leafAt i)), true)
+
+private def copyObserve (s d : ℕ) : Option (List ℕ × Bool × ℕ) :=
+  let x : Data 7 := ⟨![s, d, 3, 0, 0, 0, 0],
+    fun a => if s ≤ a ∧ a < s + 3 then a - s + 1 else 99⟩
+  (ArrayCopy.program.eval 8 4 x).map fun (y, time) =>
+    (List.ofFn (fun i : Fin 3 => y.mem (d + i.val)),
+      decide ((∀ i : Fin 3, y.mem (s + i.val) = i.val + 1) ∧
+        y.mem 0 = 99 ∧ y.mem 12 = 99), time)
+
+-- Execute the generalized helper in both disjoint orders and with equal blocks. The old
+-- forward-copy theorem remains available; these also check nonzero words outside the frame.
+#guard copyObserve 4 8 == some ([1, 2, 3], true, 25)
+#guard copyObserve 8 4 == some ([1, 2, 3], true, 25)
+#guard copyObserve 4 4 == some ([1, 2, 3], true, 25)
+
+-- Nonzero garbage immediately beyond the two work buffers survives the complete encoder.
+#guard ((program false).eval 16 128
+    ((State.init (input 2 (fun _ => -1)) : State 32).data.write
+      (scratchBase 2 + 10 ^ 2) 91)).map
+    (fun (y, _) => y.mem (scratchBase 2 + 10 ^ 2)) == some 91
+
+#guard observe true 8 0 2 (fun _ => -4) == some (([-4], true), 31)
+
+/-- The explicit width condition itself has a checked boundary. -/
+example : ¬Fits 9 (addressBound 1) ∧ Fits 10 (addressBound 1) := by decide
+
+/-- A kernel-checked zero-depth flat execution with a negative value, derived from the
+general theorem rather than from VM evaluation. All calling/width premises are discharged. -/
+example : ∃ y : Data 32, ∃ n, n ≤ 240 ∧
+    Runs 8 ((program false).program output)
+      (State.init (inputL (fun _ : LeftStr 0 => -3))) ⟨(program false).size, y⟩ n ∧
+    Executes 8 ((program false).program output)
+      (State.init (inputL (fun _ : LeftStr 0 => -3))) 3 (n + 1) ∧ y.mem 3 = 7 := by
+  obtain ⟨_, y, n, hn, hr, he, hv, _⟩ := runs_left (w := 6) (by decide)
+    (fun _ : LeftStr 0 => -3) 3 (by decide) (by intro u; decide) (by decide) (by decide)
+  refine ⟨y, n, ?_, hr, he, ?_⟩
+  · simpa only [timeBound, pow_zero, Nat.reduceAdd, Nat.mul_one] using hn
+  · have hidx : (leafIndex (Fin.elim0 : Leaf 0)).val = 0 := by
+      have := (leafIndex (Fin.elim0 : Leaf 0)).isLt
+      norm_num at this ⊢
+    have h := hv (Fin.elim0 : Leaf 0)
+    have hval : encodingL (fun _ : LeftStr 0 => -3) Fin.elim0 = -3 :=
+      encodeWith_zero phi _ _
+    have henc : encode (-3) = 7 := by decide
+    simpa only [outputBase, pow_zero, hidx, hval, henc, Nat.reduceAdd] using h
+
+/-- A nonvacuous two-stage client of the complete flat execution theorem. The checked signed
+array has a zero `P0,P0` leaf through cancellation and also many nonzero leaves in the VM test. -/
+example : ∃ y : Data 32, ∃ n, n ≤ 72000 ∧
+    Runs 18 ((program false).program output) (State.init (inputL signedLeft))
+      ⟨(program false).size, y⟩ n ∧
+    Executes 18 ((program false).program output) (State.init (inputL signedLeft)) 51 (n + 1) ∧
+      y.mem (outputBase 2 + (leafIndex (fun _ : Fin 2 => Term.P0)).val) = 0 := by
+  obtain ⟨_, y, n, hn, hr, he, hv, _⟩ := runs_left (w := 16) (by decide)
+    signedLeft 3 (by decide) (by decide +kernel) (by decide) (by decide)
+  refine ⟨y, n, ?_, hr, he, ?_⟩
+  · norm_num [timeBound] at hn ⊢
+    exact hn
+  · have hmath : encodingL signedLeft (fun _ : Fin 2 => Term.P0) = 0 := by decide +kernel
+    simpa only [hmath, show encode 0 = 0 from rfl] using hv (fun _ : Fin 2 => Term.P0)
+
+end ComplexityTests.SchonhageEncoding
diff --git a/NOTICE b/NOTICE
index dcdc12ee9..468bfa04b 100644
--- a/NOTICE
+++ b/NOTICE
@@ -27,3 +27,7 @@ This product is licensed under the Apache License, Version 2.0 (see LICENSE).
 The prime-window proof also adapts Mathlib/NumberTheory/Bertrand.lean,
 Copyright (c) 2020 Patrick Stevens; authors Patrick Stevens, Bolton Bailey,
 under the Apache License, Version 2.0.
+
+The shared tensor encoder in
+Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/
+is also part of the Anthropic adaptation described above.
diff --git a/ROADMAP.md b/ROADMAP.md
index 5fc6cb5a6..3145a848b 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -434,6 +434,9 @@ each statement against the numbered result. Organize modules by subject, not cha
   theorems; simulating operations by programs over smaller bases; structured programs and time
   classes over arbitrary value domains with weighted or bit costs; simulations between instances;
   the typed core proposed in [CSLib #1158](https://github.com/leanprover/cslib/pull/1158).
+- **Shared native matrix encoders** ([#1493](https://github.com/cslib-community/complexitylib/issues/1493)): compute all `10^L` leaf values from `7^L`
+  signed inputs within `240*(L+1)*10^L` standard WordRAM instructions, plus the final halt,
+  with fixed code/registers and concrete initialized inputs, frames and explicit width bounds.
 - **Word RAM:** an AC⁰ basis; wider-fragment and Turing-machine simulations;
   transfer of Anthropic's modular machine and 3SUM/APSP algorithms; direct 3SUM adaptation ([#1394])
   has the Convolution-3SUM/Exact Triangle correctness reduction, a charged native single-instance
@@ -442,9 +445,9 @@ each statement against the numbered result. Organize modules by subject, not cha
   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. The tensor identity, full recursion,
-  shared encodings and pruned-evaluation core ([#1459]) include exact visited-leaf and passed-set
+  shared encodings and pruned-evaluation core ([#1459](https://github.com/cslib-community/complexitylib/issues/1459)) include exact visited-leaf and passed-set
   bounds, with the empty zero-depth root handled explicitly. The finite thin-product component
-  ([#1463]) proves valid layouts, arbitrary-size padding/tiling, exact queried signed products and
+  ([#1463](https://github.com/cslib-community/complexitylib/issues/1463)) proves valid layouts, arbitrary-size padding/tiling, exact queried signed products and
   sparse encoding/leaf/passed-set totals. These counts are not native instruction costs. It still
   needs native tensor/sparse-query programs, native Chan–He preprocessing, the reduction
   host, the fast Exact Triangle solver and full
diff --git a/UPSTREAM.md b/UPSTREAM.md
index b009e0bce..555634883 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -154,6 +154,22 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   theorems preserve the complete source memory and register bank. This is forward correctness,
   not reflection of source faults; transfer from Anthropic's modular signed machine and its
   3SUM/APSP algorithms remains separate.
+* **Native shared tensor encoder.** `Algorithms/WordRAM/MatrixMultiplication/Schonhage/` implements the complete shared left/right
+  encoding milestone ([#1493](https://github.com/cslib-community/complexitylib/issues/1493)).
+  Fixed standard-WordRAM code with 32 registers transforms one coordinate at a time between
+  two disjoint `10^L` buffers. It starts from `State.init` with a depth header and `7^L`
+  sign-and-magnitude words, computes all public `encodingL`/`encodingR` values, and preserves
+  the input and every cell outside the two buffers. Mathlib's `finFunctionFinEquiv` supplies
+  least-significant-first string numbering. All stages, powers, indices, address arithmetic,
+  signed add/subtract blocks and the final output copy cost at most `240*(L+1)*10^L`
+  instructions; halt adds one. Signed operands have magnitude bounded from the original
+  input by `7^L*A < 2^(w-1)`; the explicit natural bound `L+64+64*10^L` must fit target width
+  `w+2`. The two extra bits and actual arithmetic-block costs come from the existing native
+  signed kernels, without a copied source machine or a whole-program simulation hypothesis.
+  The existing array-copy interface is retained, with a narrow generalization for disjoint
+  blocks in either address order or identical blocks.
+  This is the encoder component only; band/tile preparation and full native composition remain
+  in [#1394](https://github.com/cslib-community/complexitylib/issues/1394).
 * **Direct 3SUM adaptation.** `Algorithms/ThreeSum/Convolution.lean` adapts the explicit
   Convolution-3SUM to Exact Triangle correctness reduction from Anthropic's
   [`formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp),