diff --git a/Complexity.lean b/Complexity.lean
index c6f6b4ef51..227ff8d31a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -158,6 +158,16 @@ public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandR
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandSplit
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandTables
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandThin
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Bounds
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Core
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Exec
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Flat
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Input
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Program
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Return
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Setup
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Width
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Cell
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Controller
 public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Copy
@@ -1957,6 +1967,7 @@ public import Complexity.Computability.USTCON.Reader.Invariant
 public import Complexity.Computability.USTCON.Space
 public import Complexity.Computability.WordRAM.Allocation
 public import Complexity.Computability.WordRAM.ArrayAppend
+public import Complexity.Computability.WordRAM.ArrayNormalize
 public import Complexity.Computability.WordRAM.Basis
 public import Complexity.Computability.WordRAM.Compile
 public import Complexity.Computability.WordRAM.Controller
@@ -1971,6 +1982,7 @@ public import Complexity.Computability.WordRAM.Heap
 public import Complexity.Computability.WordRAM.InputArray
 public import Complexity.Computability.WordRAM.ListArray
 public import Complexity.Computability.WordRAM.MapOp
+public import Complexity.Computability.WordRAM.MemoryWindow
 public import Complexity.Computability.WordRAM.Multiword
 public import Complexity.Computability.WordRAM.Multiword.Arithmetic
 public import Complexity.Computability.WordRAM.Multiword.Bank
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable.lean
new file mode 100644
index 0000000000..c70237b148
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable.lean
@@ -0,0 +1,52 @@
+/-
+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.Init
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Width
+
+/-!
+# Caller-safe native queried thin products
+
+## Main definitions
+
+* `CallableProduct.program`: fixed standard unsigned code on 163 registers, with a runtime
+  source-memory base in register 160 and an absolute answer pointer returned in register zero.
+* `CallableProduct.entryProgram`, `CallableProduct.input`: actual initialized client, with a
+  protected caller prefix and original raw matrices/interleaved request coordinates.
+* `CallableProduct.windowSize`: explicit polynomial virtual address-space reservation;
+  this interval is not initialized or copied in bulk.
+
+## Main results
+
+* `CallableProduct.exec`: actual caller-safe product execution from original zero/one matrices,
+  arbitrary query occurrences and dirty scratch, with exact local-input restoration and full
+  outside-window frame. A bounded caller state supplies physical word validity throughout.
+* `CallableProduct.runs_wide`: actual `State.init` input fit, same-data prefix `Runs` and charged
+  halt at every physical width at least `256*clog₂(base+N+Q+P+5)`, for caller-word bound `P`.
+* `CallableProduct.runs_caller`, `CallableProduct.caller_prefix_bounded`: the corresponding
+  callable flat run and every-prefix physical fit with `P` bounding all initial caller words,
+  including dirty memory words loaded before the real remainder. In initialized clients,
+  scratch is zero and `P` only needs to bound the protected caller prefix.
+* `CallableProduct.timeBound_le`: at most three times the original charged product plus
+  `2048*(N*D+Q+1)` standalone adaptation work, including halt.
+* `CallableProduct.runs_thin`: at `L=19m`, `D=4^m`, `D^18≤N` and `Q*2^m≤N²`, the actual charge
+  is at most `17301504*(19m+1)*N²/D^(1/18)`. Distinct-set sparsity instead retains an explicit
+  additive charge for duplicate occurrences through `CallableProduct.thin_timeBound`.
+
+The original product program is unchanged. `MemoryWindow.compile` translates each load into
+actual base addition, load and remainder, each store into addition and store, and preserves
+native branching/loop decisions. Computed logarithm/power setup and two linear normalization
+loops are charged. Raw zero/one input is doubled by the original actual matrix-input loop.
+No source-Light semantics, new ALU operation, assumed execution or fast solver is used.
+
+The finite tensor, band and query mathematics and their source mapping remain those of
+`QueriedProduct`; the compiler and callable controller are original native work. Stage APIs
+are internal implementation interfaces. The concrete ET-record adapter, backend/witness
+composition, whole ordinary-3SUM solver and improved 1.9992 endpoint remain open under #1394.
+-/
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Bounds.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Bounds.lean
new file mode 100644
index 0000000000..a0744f350a
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Bounds.lean
@@ -0,0 +1,134 @@
+/-
+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.Callable.Flat
+
+/-!
+# Original-parameter width, space and charge for callable products
+
+The virtual window reservation is polynomial in the original row and occurrence counts. Its
+large fixed exponent is explicit; the program does not initialize that whole interval. Actual
+setup and return work is linear in original matrix/input size, plus the translated product.
+Distinct-set sparsity retains the additive occurrence charge; occurrence sparsity absorbs it.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- The reserved window has a fixed polynomial size in original dimensions and query count. -/
+theorem windowSize_le (N Q : ℕ) : windowSize N Q ≤ (2 * (N + Q + 3)) ^ 128 := by
+  have hc := Nat.clog_pos (by decide : 1 < (2 : ℕ)) (by omega : 1 < N + Q + 3)
+  have hp := Nat.pow_pred_clog_lt_self (by decide : 1 < (2 : ℕ)) (by omega : 1 < N + Q + 3)
+  have he : Nat.clog 2 (N + Q + 3) = (Nat.clog 2 (N + Q + 3)).pred + 1 :=
+    (Nat.succ_pred_eq_of_pos hc).symm
+  have hceil : 2 ^ Nat.clog 2 (N + Q + 3) ≤ 2 * (N + Q + 3) := by
+    rw [he, pow_succ]
+    omega
+  have h := Nat.pow_le_pow_left hceil 128
+  simpa only [windowSize, sourceWidth, ← pow_mul, Nat.mul_comm 128] using h
+
+/-- Every physical width at least a positive logarithmic threshold admits the complete runtime
+window and all setup/return addresses. No intermediate-fit certificate is needed. -/
+theorem physical_fits {W b N Q : ℕ}
+    (hW : 256 * Nat.clog 2 (b + N + Q + 5) ≤ W) :
+    Fits W (b + 4 * windowSize N Q + 1024) := by
+  let c := Nat.clog 2 (b + N + Q + 5)
+  have hc : 0 < c := Nat.clog_pos (by decide) (by omega)
+  have hceil := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (b + N + Q + 5)
+  change b + N + Q + 5 ≤ 2 ^ c at hceil
+  have hm : windowSize N Q ≤ 2 ^ (128 * c) := by
+    apply Nat.pow_le_pow_right (by decide)
+    apply Nat.mul_le_mul_left 128
+    exact Nat.clog_mono_right 2 (by omega)
+  have hb : b ≤ 2 ^ (128 * c) := by
+    have he : c ≤ 128 * c := by omega
+    exact (show b ≤ 2 ^ c by omega).trans (Nat.pow_le_pow_right (by decide) he)
+  have hpos : 1 ≤ 2 ^ (128 * c) := Nat.one_le_pow _ _ (by decide)
+  have hsum : b + 4 * windowSize N Q + 1024 < 2 ^ (128 * c + 11) := by
+    rw [pow_add]
+    norm_num only [Nat.reducePow]
+    omega
+  exact hsum.trans_le (Nat.pow_le_pow_right (by decide) (by change 256 * c ≤ W at hW; omega))
+
+/-- Full standalone charge (including its base load and halt): constant-factor actual product
+cost plus linear adaptation. No bulk-window or caller-catalogue copy is hidden in this bound. -/
+theorem timeBound_le {m N : ℕ} (qs : List (Fin N × Fin N)) :
+    timeBound (m := m) qs + 3 ≤
+      3 * (QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs + 1) +
+        2048 * (N * D m + qs.length + 1) := by
+  have hlog : Nat.clog 2 (N + qs.length + 3) ≤ N + qs.length + 3 :=
+    Nat.clog_le_of_le_pow (Nat.lt_two_pow_self.le)
+  have hD : 0 < D m := Nat.pow_pos (by decide)
+  have hND : N ≤ N * D m := Nat.le_mul_of_pos_right N hD
+  unfold timeBound coreTime QueriedProduct.inputEnd
+  omega
+
+/-- Under distinct-position sparsity, every duplicate occurrence retains its additive charge.
+This quantitative saving bounds the real callable program, including initialization and halt. -/
+theorem thin_timeBound {m N : ℕ} (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hQ : qs.toFinset.card * 2 ^ m ≤ N ^ 2) :
+    ((timeBound (m := m) qs + 3 : ℕ) : ℝ) ≤
+      262144 * ((19 * m + 1 : ℕ) : ℝ) *
+        (65 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2) + qs.length) := by
+  have hNpos : 0 < N := (Nat.pow_pos (Nat.pow_pos (by decide : 0 < (4 : ℕ)))).trans_le hN
+  have hp := preparation_shape_le (show m ≤ 19 * m by omega) hNpos
+  have hpR : ((1 + N * D m : ℕ) : ℝ) ≤
+      ((5 * (numBands (19 * m) m N * 10 ^ (19 * m)) : ℕ) : ℝ) := by
+    exact_mod_cast ((Nat.le_add_right (1 + N * D m) (2 ^ (19 * m))).trans
+      (Nat.le_add_right _ (2 * numBands (19 * m) m N * 10 ^ (19 * m)))).trans hp
+  have he := encodings_total_le m N hN
+  have hlinear : ((N * D m + qs.length + 1 : ℕ) : ℝ) ≤
+      10 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2) + qs.length := by
+    push_cast at hpR he ⊢
+    nlinarith only [hpR, he]
+  have hbase := QueriedProduct.thin_timeBound m N qs hN hQ
+  have htime : ((timeBound (m := m) qs + 3 : ℕ) : ℝ) ≤
+      3 * ((QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs + 1 : ℕ) : ℝ) +
+        2048 * ((N * D m + qs.length + 1 : ℕ) : ℝ) := by exact_mod_cast timeBound_le qs
+  have hL : (1 : ℝ) ≤ ((19 * m + 1 : ℕ) : ℝ) := by norm_cast; omega
+  have hG : 0 ≤ (D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2 := by positivity
+  have hQ0 : 0 ≤ (qs.length : ℝ) := Nat.cast_nonneg _
+  nlinarith only [htime, hbase, hlinear, mul_nonneg (sub_nonneg.mpr hL) hG,
+    mul_nonneg (sub_nonneg.mpr hL) hQ0, hG, hQ0]
+
+/-- Occurrence sparsity absorbs the duplicate charge and yields the complete charged saving. -/
+theorem thin_timeBound_sparse {m N : ℕ} (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hQ : qs.length * 2 ^ m ≤ N ^ 2) :
+    ((timeBound (m := m) qs + 3 : ℕ) : ℝ) ≤
+      17301504 * ((19 * m + 1 : ℕ) : ℝ) * (N : ℝ) ^ 2 / (D m : ℝ) ^ (1 / 18 : ℝ) := by
+  have hset : qs.toFinset.card * 2 ^ m ≤ N ^ 2 :=
+    (Nat.mul_le_mul_right _ (List.toFinset_card_le qs)).trans hQ
+  have h := thin_timeBound qs hN hset
+  have hQr : (qs.length : ℝ) * (2 : ℝ) ^ m ≤ (N : ℝ) ^ 2 := by exact_mod_cast hQ
+  have hlen := mul_le_mul_of_nonneg_left hQr (saving_pos m).le
+  have hpow : 1 ≤ saving m * (2 : ℝ) ^ m := by
+    rw [← saving_mul_two_rpow m]
+    apply mul_le_mul_of_nonneg_left _ (saving_pos m).le
+    rw [← Real.rpow_natCast]
+    apply Real.rpow_le_rpow_of_exponent_le (by norm_num)
+    have := Nat.cast_nonneg (α := ℝ) m
+    linarith
+  have hlen' : (qs.length : ℝ) ≤
+      (D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2 := by
+    rw [← saving_eq_D_rpow]
+    nlinarith only [hlen, mul_le_mul_of_nonneg_left hpow (Nat.cast_nonneg qs.length :
+      (0 : ℝ) ≤ qs.length)]
+  have hL : 0 ≤ ((19 * m + 1 : ℕ) : ℝ) := Nat.cast_nonneg _
+  have hfinal : ((timeBound (m := m) qs + 3 : ℕ) : ℝ) ≤
+      17301504 * ((19 * m + 1 : ℕ) : ℝ) *
+        ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2) := by
+    nlinarith only [h, mul_nonneg hL (sub_nonneg.mpr hlen')]
+  rw [Real.rpow_neg (by positivity)] at hfinal
+  simpa only [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hfinal
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Core.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Core.lean
new file mode 100644
index 0000000000..c05bc0cac8
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Core.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Setup
+
+/-!
+# Actual translated queried-product execution
+
+The execution is derived from original zero/one matrices and request occurrences. The source
+register bank and dirty source scratch are normalized by actual setup and translated loads.
+No execution, routing, layout or cost certificate is a premise. These stage lemmas are internal
+implementation APIs; exact physical answer/input words are normalized by the final spans.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Internal stage charge, before the two final span normalizations. -/
+@[expose] def coreTime {m N : ℕ} (qs : List (Fin N × Fin N)) : ℕ :=
+  517 * Nat.clog 2 (N + qs.length + 3) + 184 +
+    3 * QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs
+
+/-- Source admission follows from the original thin geometry and zero/one entry bound. -/
+theorem source_admission {m N Q : ℕ} (hN : D m ^ 18 ≤ N) :
+    0 < sourceWidth N Q - 2 ∧
+      QueriedProduct.magnitudeBound (19 * m) 1 < 2 ^ ((sourceWidth N Q - 2) - 1) ∧
+      Fits (sourceWidth N Q) (QueriedProduct.wordBudget (19 * m) m N Q) := by
+  exact QueriedProduct.admission_bounds (QueriedProduct.thin_admissionWidth_le m N Q 1 hN)
+
+/-- Original words initialize an actual callable native product prefix, even with arbitrary
+dirty target memory in the reserved window. Answers here are clipped physical words; the
+subsequent real normalization makes them exact. Original duplicate requests retain their order. -/
+theorem exec_core {W b m N : ℕ}
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (x : Data 163) (hb : x.regs Reg.base = b)
+    (hinput : ∀ a, a < QueriedProduct.inputEnd m N qs.length →
+      x.mem (b + a) =
+        (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hN : D m ^ 18 ≤ N) (hfit : Fits W (b + 4 * windowSize N qs.length + 1024)) :
+    ∃ y, ExecWithin W core x y (coreTime (m := m) qs) ∧
+      y.regs Reg.base = b ∧ y.regs Reg.modulus = windowSize N qs.length ∧
+      y.regs Reg.inputSize = QueriedProduct.inputEnd m N qs.length ∧
+      y.regs Reg.queryCount = qs.length ∧
+      y.regs Reg.output = QueriedProduct.outputBase (19 * m) m N qs.length ∧
+      (∀ i : Fin qs.length,
+        y.mem (b + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) %
+            windowSize N qs.length = Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length →
+        y.mem (b + a) % windowSize N qs.length = x.mem (b + a)) ∧
+      (∀ a, a < b ∨ b + windowSize N qs.length ≤ a → y.mem a = x.mem a) := by
+  have hXabs (i k) : |X i k| ≤ (1 : ℤ) := by rw [abs_of_nonneg (hX i k).1]; exact (hX i k).2
+  have hYabs (k j) : |Y k j| ≤ (1 : ℤ) := by rw [abs_of_nonneg (hY k j).1]; exact (hY k j).2
+  have hbits : true = true → (∀ i k, 0 ≤ X i k) ∧ (∀ k j, 0 ≤ Y k j) :=
+    fun _ => ⟨fun i k => (hX i k).1, fun k j => (hY k j).1⟩
+  obtain ⟨hw, hmag, hbudget⟩ := source_admission (Q := qs.length) hN
+  have htwo : sourceWidth N qs.length - 2 + 2 = sourceWidth N qs.length := by omega
+  have hbudget' : Fits (sourceWidth N qs.length - 2 + 2)
+      (QueriedProduct.wordBudget (19 * m) m N qs.length) := by simpa only [htwo] using hbudget
+  have hi := QueriedProduct.input_fits hw (show m ≤ 19 * m by omega)
+    true X Y qs hXabs hYabs hmag hbudget'
+  have hi' : (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.Bounded
+      (sourceWidth N qs.length) := by
+    simpa only [htwo, State.init] using (Data.Bounded.init (r := 160) hi)
+  have hrow : x.mem (b + 3) = N := by
+    rw [hinput 3 (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  have hcount : x.mem (b + 4) = qs.length := by
+    rw [hinput 4 (by unfold QueriedProduct.inputEnd; omega)]
+    simp [State.init, Data.init, QueriedProduct.input]
+  obtain ⟨s, hs, smem, smatch, sbound⟩ := exec_setup x hb hrow hcount hfit
+  let v := MemoryWindow.view (sourceWidth N qs.length) b s
+  have vinput (a : ℕ) (ha : a < QueriedProduct.inputEnd m N qs.length) :
+      v.mem a =
+        (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a := by
+    change s.mem (b + a) % 2 ^ sourceWidth N qs.length = _
+    rw [smem, hinput a ha, Nat.mod_eq_of_lt (hi'.2 a)]
+  obtain ⟨p, hp, pp, pv, pf⟩ := QueriedProduct.exec hw (show m ≤ 19 * m by omega)
+    true X Y qs v (fun a _ ha => vinput a ha) hXabs hYabs hbits hmag hbudget'
+  have hp' : ExecWithin (sourceWidth N qs.length) (QueriedProduct.program true) v p
+      (QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs) := by
+    simpa only [htwo] using hp
+  have hwindow : Fits W (b + 2 ^ sourceWidth N qs.length) := hfit.of_le (by
+    change b + windowSize N qs.length ≤ _
+    omega)
+  obtain ⟨y, hy, ymatch, yframe⟩ := MemoryWindow.execWithin hp'
+    (QueriedProduct.not_readsWidth true) sbound smatch (setup_fits hfit).1 hwindow
+  refine ⟨y, hs.seq hy, ymatch.base_eq, ymatch.modulus_eq,
+    (ymatch.regs _).trans pp.inputSize, (ymatch.regs _).trans pp.queryCount,
+    (ymatch.regs _).trans pp.output, ?_, ?_, ?_⟩
+  · intro i
+    exact (ymatch.mem _).trans (pv i)
+  · intro a ha
+    change y.mem (b + a) % 2 ^ sourceWidth N qs.length = _
+    rw [ymatch.mem, pf a (by omega)]
+    change s.mem (b + a) % 2 ^ sourceWidth N qs.length = _
+    rw [smem, hinput a ha, Nat.mod_eq_of_lt (hi'.2 a)]
+  · intro a ha
+    exact (yframe a ha).trans (congrFun smem a)
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Exec.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Exec.lean
new file mode 100644
index 0000000000..926311e424
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Exec.lean
@@ -0,0 +1,109 @@
+/-
+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.Callable.Core
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Return
+
+/-!
+# Complete native callable queried-product execution
+
+The caller supplies original zero/one matrices and coordinate occurrences in a local original
+input block. The product computes its own tables, layouts, groups, encoded bands, epochs and
+answers. Every source memory access is translated to actual base addition and load/store code;
+dirty words are normalized without bulk clearing. The final answer pointer is absolute.
+
+This is the callable product prerequisite for an ET-record adapter, not that adapter, an
+Exact Triangle solver or the complete ordinary-3SUM bound under #1394.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- The complete charge includes two linear span normalizations and the computed setup. -/
+@[expose] def timeBound {m N : ℕ} (qs : List (Fin N × Fin N)) : ℕ :=
+  coreTime (m := m) qs + 7 * QueriedProduct.inputEnd m N qs.length + 7 * qs.length + 14
+
+private theorem spans_le_budget (L m N Q : ℕ) :
+    QueriedProduct.inputEnd m N Q ≤ QueriedProduct.outputBase L m N Q ∧
+      QueriedProduct.inputEnd m N Q + QueriedProduct.outputBase L m N Q + Q + 2 ≤
+        QueriedProduct.wordBudget L m N Q := by
+  have hsep : QueriedProduct.inputEnd m N Q ≤ QueriedProduct.outputBase L m N Q := by
+    unfold QueriedProduct.outputBase QueriedProduct.groupedBase QueriedProduct.originalBase
+      QueriedProduct.codeBase QueriedProduct.offsetBase QueriedProduct.snapshotBase
+    omega
+  have hend : QueriedProduct.outputBase L m N Q + Q ≤ QueriedProduct.memoryEnd L m N Q := by
+    unfold QueriedProduct.memoryEnd QueriedProduct.stampBase QueriedProduct.scratchBase
+    have := Nat.zero_le (2 * (L + 1) * 10 ^ L)
+    have := Nat.zero_le (10 ^ L)
+    omega
+  refine ⟨hsep, ?_⟩
+  unfold QueriedProduct.wordBudget
+  omega
+
+/-- Caller-safe actual native product execution. The only local memory premise is the original
+input block; all remaining target memory may be dirty. Every original occurrence is answered
+exactly, original input words are restored exactly, and the caller memory outside the window
+is preserved. The numerical width hypothesis is derived from original dimensions and base. -/
+theorem exec {W b m N : ℕ}
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (x : Data 163) (hb : x.regs Reg.base = b)
+    (hinput : ∀ a, a < QueriedProduct.inputEnd m N qs.length →
+      x.mem (b + a) =
+        (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hN : D m ^ 18 ≤ N) (hfit : Fits W (b + 4 * windowSize N qs.length + 1024)) :
+    ∃ y, ExecWithin W program x y (timeBound (m := m) qs) ∧
+      y.regs Reg.result = b + QueriedProduct.outputBase (19 * m) m N qs.length ∧
+      y.regs Reg.base = b ∧ y.regs Reg.modulus = windowSize N qs.length ∧
+      (∀ i : Fin qs.length,
+        y.mem (b + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length → y.mem (b + a) = x.mem (b + a)) ∧
+      (∀ a, a < b ∨ b + windowSize N qs.length ≤ a → y.mem a = x.mem a) := by
+  obtain ⟨hsep, hspan⟩ := spans_le_budget (19 * m) m N qs.length
+  have hbudget := (source_admission (Q := qs.length) hN).2.2
+  have hbound : QueriedProduct.inputEnd m N qs.length +
+      QueriedProduct.outputBase (19 * m) m N qs.length + qs.length + 2 <
+        windowSize N qs.length := hspan.trans_lt hbudget
+  have hM : 0 < windowSize N qs.length := Nat.two_pow_pos _
+  obtain ⟨c, hc, cb, cM, cI, cQ, cO, cv, ci, cf⟩ := exec_core X Y qs x hb hinput hX hY hN hfit
+  have hIfit : Fits W (b + QueriedProduct.inputEnd m N qs.length +
+      windowSize N qs.length + 2) := hfit.of_le (by omega)
+  obtain ⟨s, hs, sm, sr⟩ := exec_restoreInput c cb cI cM hM hIfit
+  have sb : s.regs Reg.base = b := (sr _ (by decide)).trans cb
+  have sM : s.regs Reg.modulus = windowSize N qs.length := (sr _ (by decide)).trans cM
+  have sQ : s.regs Reg.queryCount = qs.length := (sr _ (by decide)).trans cQ
+  have sO : s.regs Reg.output = QueriedProduct.outputBase (19 * m) m N qs.length :=
+    (sr _ (by decide)).trans cO
+  have hOfit : Fits W (b + QueriedProduct.outputBase (19 * m) m N qs.length + qs.length +
+      windowSize N qs.length + 2) := hfit.of_le (by omega)
+  obtain ⟨y, hy, ym, yr, yf⟩ := exec_returnOutput s sb sO sQ sM hM hOfit
+  refine ⟨y, (hc.seq (hs.seq hy)).mono (by unfold timeBound; omega), yr,
+    (yf _ (by decide)).trans sb, (yf _ (by decide)).trans sM, ?_, ?_, ?_⟩
+  · intro i
+    rw [ym]
+    rw [show b + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val) =
+      (b + QueriedProduct.outputBase (19 * m) m N qs.length) + i.val by omega]
+    rw [ArrayNormalize.normalizePrefix_read _ _ _ _ _ i.isLt, sm,
+      ArrayNormalize.normalizePrefix_outside _ _ _ _ _ (by omega)]
+    simpa only [Nat.add_assoc] using cv i
+  · intro a ha
+    rw [ym, ArrayNormalize.normalizePrefix_outside _ _ _ _ _ (by omega), sm,
+      ArrayNormalize.normalizePrefix_read _ _ _ _ _ ha]
+    exact ci a ha
+  · intro a ha
+    rw [ym, ArrayNormalize.normalizePrefix_outside _ _ _ _ _ (by omega), sm,
+      ArrayNormalize.normalizePrefix_outside _ _ _ _ _ (by omega)]
+    exact cf a ha
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Flat.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Flat.lean
new file mode 100644
index 0000000000..9eac7b35c9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Flat.lean
@@ -0,0 +1,97 @@
+/-
+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.Callable.Input
+
+/-!
+# Initialized flat callable products
+
+The same final native data witnesses the charged prefix run, exact physical product words,
+restored local original input, protected caller memory and the final halt. The program and its
+163 registers are fixed independently of dimensions, runtime base and physical word width.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Actual initialized execution with no computed-layout, bounded-scratch or execution premise.
+Every original duplicate request has its own exact physical answer cell. The `n+1` charge
+includes the halt reached by the same final data `y` in the prefix `Runs`. -/
+theorem runs {W m N : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hcaller : ∀ v ∈ caller, Fits W v)
+    (hfit : Fits W (inputBase caller + 4 * windowSize N qs.length + 1024)) :
+    InputFits W (input caller X Y qs) ∧
+    ∃ y n, n ≤ timeBound (m := m) qs + 2 ∧
+      Runs W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        ⟨entryProgram.size, y⟩ n ∧
+      Executes W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        (inputBase caller + QueriedProduct.outputBase (19 * m) m N qs.length) (n + 1) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length,
+        y.mem (inputBase caller + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length →
+        y.mem (inputBase caller + a) =
+          (State.init (input caller X Y qs) : State 163).data.mem (inputBase caller + a)) ∧
+      (∀ a, a < inputBase caller ∨ inputBase caller + windowSize N qs.length ≤ a →
+        y.mem a = (State.init (input caller X Y qs) : State 163).data.mem a) := by
+  have hi := input_fits caller X Y qs hN hX hY hcaller hfit
+  let x := (State.init (input caller X Y qs) : State 163).data
+  let s := (x.set Reg.address 1).set Reg.base (inputBase caller)
+  have h1 : Fits W 1 := hfit.of_le (by omega)
+  have hread : x.mem 1 = inputBase caller := by simp [x, input, State.init, Data.init]
+  have hs : ExecWithin (B := .standard) W
+      (ram[ Reg.address ← #1; Reg.base ← *Reg.address ]) x s 2 := by
+    ram_eval [s, h1, hread, Reg.address, Reg.base, Fin.mk.injEq]
+  obtain ⟨y, hy, yr, yb, yM, yv, yi, yf⟩ := exec X Y qs s
+    (by simp [s]) (fun a _ => input_word caller X Y qs a) hX hY hN hfit
+  have he : ExecWithin W entryProgram x y (2 + timeBound (m := m) qs) := hs.seq hy
+  have ybound : y.Bounded W := he.bounded (by simpa only [x, State.init] using Data.Bounded.init hi)
+  obtain ⟨n, hn, he⟩ := he
+  refine ⟨hi, y, n, by omega, ?_, ?_, ybound, yv, yi, yf⟩
+  · simpa only [Nat.zero_add, x, State.init] using he.runs (pc := 0)
+      (p := entryProgram.program Reg.result) (Program.Contains.self _).append_left
+  · simpa only [yr, x, State.init] using he.executes Reg.result
+
+set_option maxRecDepth 4096 in
+-- This finite syntactic check visits the fixed 160-register normalization sequence.
+private theorem setup_size : setup.size ≤ 1024 := by decide +kernel
+
+set_option maxRecDepth 4096 in
+-- This finite syntactic check visits the fixed normalization and reused arithmetic routines.
+private theorem setup_not_readsWidth : ¬setup.ReadsWidth := by decide +kernel
+
+/-- The complete standalone caller has a fixed finite flat program, including halt. -/
+theorem program_length_le : (entryProgram.program Reg.result).length ≤ 131072 := by
+  have hp := QueriedProduct.program_length_le true
+  simp only [Code.program, List.length_append, Code.length_assemble,
+    List.length_singleton] at hp ⊢
+  have hc := MemoryWindow.size_compile (QueriedProduct.program true)
+  have hs := setup_size
+  have hi : restoreInput.size = 13 := by decide +kernel
+  have ho : returnOutput.size = 13 := by decide +kernel
+  simp only [entryProgram, program, Code.size] at *
+  omega
+
+/-- The width-independent code computes its own virtual modulus without reading physical width. -/
+theorem not_readsWidth : ¬entryProgram.ReadsWidth := by
+  have hr : ¬restoreInput.ReadsWidth := by decide +kernel
+  have ho : ¬returnOutput.ReadsWidth := by decide +kernel
+  simp only [entryProgram, program, Code.ReadsWidth, Op.ReadsWidth,
+    MemoryWindow.readsWidth_compile, QueriedProduct.not_readsWidth, setup_not_readsWidth,
+    hr, ho, not_false_eq_true, or_self]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Input.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Input.lean
new file mode 100644
index 0000000000..336f6a0b8c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Input.lean
@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Exec
+import Mathlib.Data.List.GetD
+
+/-!
+# Ordinary initialized input for a callable product
+
+The first input word is a runtime base pointer. An arbitrary caller prefix follows, then a
+local ordinary input-length word and the unchanged original product input. No computed tables,
+grouping, encodings, bounded scratch contents or execution certificates occur in this input.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Runtime location of the local length word after an arbitrary caller prefix. -/
+@[expose] def inputBase (caller : List ℕ) : ℕ := caller.length + 2
+
+/-- Original scalar headers, raw matrices and request pairs above a protected caller prefix. -/
+@[expose] def input {m N : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) : List ℕ :=
+  let payload := QueriedProduct.input true (19 * m) X Y qs
+  [inputBase caller] ++ caller ++ payload.length :: payload
+
+/-- The initialized client loads the supplied runtime base before invoking the real kernel. -/
+@[expose] def entryProgram : Code .standard 163 :=
+  .seq (ram[ Reg.address ← #1; Reg.base ← *Reg.address ]) program
+
+private theorem block_word (caller payload : List ℕ) (a : ℕ) :
+    (Data.init ([inputBase caller] ++ caller ++ payload.length :: payload) : Data 163).mem
+        (inputBase caller + a) = (Data.init payload : Data 160).mem a := by
+  change (Data.init _ : Data 163).mem (caller.length + 2 + a) = _
+  rw [show caller.length + 2 + a = (caller.length + 1 + a) + 1 by omega, Data.init_mem_succ]
+  rw [List.getD_append_right _ _ _ _ (by simp)]
+  simp only [List.length_append, List.length_singleton]
+  have hoff : caller.length + 1 + a - (1 + caller.length) = a := by omega
+  rw [hoff]
+  cases a with
+  | zero => simp [Data.init]
+  | succ a => simp [Data.init_mem_succ, List.getD_eq_getElem?_getD]
+
+/-- Every local original input word has its actual initialized meaning at the runtime base. -/
+theorem input_word {m N : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (a : ℕ) :
+    (State.init (input caller X Y qs) : State 163).data.mem (inputBase caller + a) =
+      (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a :=
+  block_word caller _ a
+
+/-- Original caller words and admitted original product words suffice for the global input fit. -/
+theorem input_fits {W m N : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hcaller : ∀ v ∈ caller, Fits W v)
+    (hfit : Fits W (inputBase caller + 4 * windowSize N qs.length + 1024)) :
+    InputFits W (input caller X Y qs) := by
+  have hXabs (i k) : |X i k| ≤ (1 : ℤ) := by rw [abs_of_nonneg (hX i k).1]; exact (hX i k).2
+  have hYabs (k j) : |Y k j| ≤ (1 : ℤ) := by rw [abs_of_nonneg (hY k j).1]; exact (hY k j).2
+  obtain ⟨hw, hmag, hbudget⟩ := source_admission (Q := qs.length) hN
+  have htwo : sourceWidth N qs.length - 2 + 2 = sourceWidth N qs.length := by omega
+  have hi := QueriedProduct.input_fits hw (show m ≤ 19 * m by omega)
+    true X Y qs hXabs hYabs hmag (by simpa only [htwo] using hbudget)
+  have hi' : InputFits (sourceWidth N qs.length) (QueriedProduct.input true (19 * m) X Y qs) := by
+    simpa only [htwo] using hi
+  have hlen : (QueriedProduct.input true (19 * m) X Y qs).length < windowSize N qs.length := hi'.1
+  refine ⟨?_, ?_⟩
+  · apply hfit.of_le
+    simp only [input, List.length_append, List.length_cons, List.length_nil, inputBase]
+    unfold inputBase at hfit
+    omega
+  · intro v hv
+    simp only [input, List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hv
+    rcases hv with ((rfl | hv) | rfl | hv)
+    · exact hfit.of_le (by omega)
+    · exact hcaller _ hv
+    · exact (hi'.1.mono (setup_fits hfit).1)
+    · exact (hi'.2 v hv).mono (setup_fits hfit).1
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Program.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Program.lean
new file mode 100644
index 0000000000..3cbb582cd5
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Program.lean
@@ -0,0 +1,107 @@
+/-
+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.Product.ThinWidth
+public import Complexity.Algorithms.WordRAM.NatClog
+public import Complexity.Computability.WordRAM.MemoryWindow
+public import Complexity.Computability.WordRAM.ArrayNormalize
+public import Complexity.Computability.WordRAM.Power
+
+/-!
+# Callable queried-product code
+
+The source product is unchanged. Its translated memory accesses use a runtime base in register
+160 and a source-word modulus computed from the original row and query counts. The 160 source
+registers occupy the low bank; registers 161 and 162 are the modulus and address temporary.
+
+Raw zero/one entries are still doubled by the original charged matrix-input loop. Setup and
+final normalization touch only the original input and answer spans, never the whole reserved
+window or caller catalogue. The code definitions here are internal implementation APIs.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+
+namespace Reg
+
+/-- Absolute result pointer returned to the caller. Also a setup argument register. -/
+abbrev result : Fin 163 := 0
+/-- Setup argument register. -/
+abbrev second : Fin 163 := 1
+/-- Setup constant or normalization modulus. -/
+abbrev third : Fin 163 := 2
+/-- Power exponent during setup. -/
+abbrev fourth : Fin 163 := 3
+/-- Runtime source-memory base supplied by the caller. -/
+abbrev base : Fin 163 := 160
+/-- Computed source-word modulus, preserved across the translated product. -/
+abbrev modulus : Fin 163 := 161
+/-- Temporary absolute address. -/
+abbrev address : Fin 163 := 162
+/-- Source register retaining the original input span length. -/
+abbrev inputSize : Fin 163 := QueriedProduct.inputSize.castAdd 3
+/-- Source register retaining the relative answer pointer. -/
+abbrev output : Fin 163 := QueriedProduct.output.castAdd 3
+/-- Source register retaining the query occurrence count. -/
+abbrev queryCount : Fin 163 := QueriedProduct.queryCount.castAdd 3
+
+end Reg
+
+/-- The logarithm routine uses four low scratch registers. -/
+@[expose] def clogBank (i : Fin 4) : Fin 163 := i.castAdd 159
+/-- The power routine uses five low scratch registers. -/
+@[expose] def powerBank (i : Fin 5) : Fin 163 := i.castAdd 158
+/-- Array normalization uses seven low scratch registers. -/
+@[expose] def normalizeBank (i : Fin 7) : Fin 163 := i.castAdd 156
+
+/-- Read the actual row and occurrence-count headers, and form `N+Q+3`. -/
+@[expose] def readSize : Code .standard 163 := ram[
+  Reg.result ← #3; Reg.address ← Reg.base + Reg.result; Reg.result ← *Reg.address;
+  Reg.second ← #4; Reg.address ← Reg.base + Reg.second; Reg.second ← *Reg.address;
+  Reg.result ← Reg.result + Reg.second; Reg.second ← #3;
+  Reg.result ← Reg.result + Reg.second ]
+
+/-- Compute `2^(128*clog₂(N+Q+3))` with the existing logarithm and power programs. -/
+@[expose] def setup : Code .standard 163 :=
+  .seq readSize <| .seq (NatClog.program.rename clogBank) <|
+    .seq (ram[ Reg.third ← #128; Reg.fourth ← Reg.second * Reg.third; Reg.third ← #2 ]) <|
+      .seq (Power.program.rename powerBank) <|
+        .seq (.op (.copy Reg.modulus Reg.result)) (MemoryWindow.normalizeRegisters 160)
+
+/-- Normalize the restored local input, so its actual physical words equal their source words. -/
+@[expose] def restoreInput : Code .standard 163 :=
+  .seq (ram[ Reg.result ← Reg.base; Reg.second ← Reg.inputSize;
+    Reg.third ← Reg.modulus ]) (ArrayNormalize.program.rename normalizeBank)
+
+/-- Normalize the exact output span and return its absolute address. -/
+@[expose] def returnOutput : Code .standard 163 :=
+  .seq (ram[ Reg.result ← Reg.base + Reg.output;
+    Reg.second ← Reg.queryCount; Reg.third ← Reg.modulus ])
+      (ArrayNormalize.program.rename normalizeBank)
+
+/-- One fixed native raw-input product callable above an arbitrary caller-supplied base.
+Every memory translation, source instruction and normalization is part of this code. -/
+@[expose] def program : Code .standard 163 :=
+  .seq (.seq setup (MemoryWindow.compile (QueriedProduct.program true)))
+    (.seq restoreInput returnOutput)
+
+/-- Internal execution prefix through setup and the actual translated product. -/
+@[expose] def core : Code .standard 163 :=
+  .seq setup (MemoryWindow.compile (QueriedProduct.program true))
+
+/-- The derived source width is independent of the physical machine width. -/
+@[expose] def sourceWidth (N Q : ℕ) : ℕ := 128 * Nat.clog 2 (N + Q + 3)
+
+/-- Polynomially bounded virtual address-space reservation; no bulk initialization is implied. -/
+@[expose] def windowSize (N Q : ℕ) : ℕ := 2 ^ sourceWidth N Q
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Return.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Return.lean
new file mode 100644
index 0000000000..bbd2db7574
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Return.lean
@@ -0,0 +1,102 @@
+/-
+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.Callable.Program
+
+/-!
+# Exact physical input and answer words
+
+The callable compiler relates clipped memory to source memory. Two actual in-place span loops
+make the restored input and returned answers exact physical words. These are internal execution
+interfaces; both loops charge their setup, address calculations, remainders and stores.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+
+private theorem normalizeBank_injective : Function.Injective normalizeBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 163 => k.val) h)
+
+private theorem exec_normalizeBank {W b n M : ℕ} (x : Data 163)
+    (hb : x.regs Reg.result = b) (hn : x.regs Reg.second = n)
+    (hm : x.regs Reg.third = M) (hM : 0 < M) (hfit : Fits W (b + n + M + 2)) :
+    ∃ y, ExecWithin W (ArrayNormalize.program.rename normalizeBank) x y (7 * n + 4) ∧
+      y.mem = ArrayNormalize.normalizePrefix x.mem b M n ∧ y.regs Reg.result = b ∧
+      ∀ i : Fin 163, 7 ≤ i.val → y.regs i = x.regs i := by
+  obtain ⟨a, ha, am, ab, an, aM⟩ := ArrayNormalize.exec (x.comap normalizeBank) hb hn hm hM hfit
+  refine ⟨a.extend normalizeBank x, ha.rename normalizeBank_injective, am,
+    (normalizeBank_injective.extend_apply _ _ ArrayNormalize.base).trans ab, ?_⟩
+  intro i hi
+  have hnot : ¬∃ j, normalizeBank j = i := by
+    rintro ⟨j, hj⟩
+    have h := congrArg (fun k : Fin 163 => k.val) hj
+    change j.val = i.val at h
+    omega
+  exact Function.extend_apply' _ _ _ hnot
+
+/-- Normalize precisely the local original input; high product/caller registers survive. -/
+theorem exec_restoreInput {W b n M : ℕ} (x : Data 163) (hb : x.regs Reg.base = b)
+    (hn : x.regs Reg.inputSize = n) (hm : x.regs Reg.modulus = M) (hM : 0 < M)
+    (hfit : Fits W (b + n + M + 2)) :
+    ∃ y, ExecWithin W restoreInput x y (7 * n + 7) ∧
+      y.mem = ArrayNormalize.normalizePrefix x.mem b M n ∧
+      ∀ i : Fin 163, 7 ≤ i.val → y.regs i = x.regs i := by
+  let z := ((x.set Reg.result b).set Reg.second n).set Reg.third M
+  have hz : ExecWithin (B := .standard) W
+      (ram[ Reg.result ← Reg.base; Reg.second ← Reg.inputSize;
+        Reg.third ← Reg.modulus ]) x z 3 := by
+    ram_eval [z, hb, hn, hm, Reg.result, Reg.second, Reg.third, Reg.base, Reg.inputSize,
+      Reg.modulus, QueriedProduct.inputSize, Fin.mk.injEq]
+  obtain ⟨y, hy, ym, yr, yh⟩ := exec_normalizeBank (W := W) (b := b) (n := n) (M := M) z
+    (by simp [z, Reg.result, Reg.second, Reg.third])
+    (by simp [z, Reg.second, Reg.third]) (by simp [z]) hM hfit
+  refine ⟨y, (hz.seq hy).mono (by omega), ym, ?_⟩
+  intro i hi
+  rw [yh i hi]
+  have h0 : i ≠ Reg.result := by intro h; subst i; simp [Reg.result] at hi
+  have h1 : i ≠ Reg.second := by intro h; subst i; simp [Reg.second] at hi
+  have h2 : i ≠ Reg.third := by intro h; subst i; simp [Reg.third] at hi
+  simp only [z, Data.set_regs, Function.update_of_ne h0, Function.update_of_ne h1,
+    Function.update_of_ne h2]
+
+/-- Normalize the answer span, preserving all high registers, and return its absolute pointer. -/
+theorem exec_returnOutput {W b o n M : ℕ} (x : Data 163) (hb : x.regs Reg.base = b)
+    (ho : x.regs Reg.output = o) (hn : x.regs Reg.queryCount = n)
+    (hm : x.regs Reg.modulus = M) (hM : 0 < M) (hfit : Fits W (b + o + n + M + 2)) :
+    ∃ y, ExecWithin W returnOutput x y (7 * n + 7) ∧
+      y.mem = ArrayNormalize.normalizePrefix x.mem (b + o) M n ∧
+      y.regs Reg.result = b + o ∧
+      ∀ i : Fin 163, 7 ≤ i.val → y.regs i = x.regs i := by
+  have haddr : Fits W (b + o) := hfit.of_le (by omega)
+  let z := ((x.set Reg.result (b + o)).set Reg.second n).set Reg.third M
+  have hz : ExecWithin W
+      (ram[ Reg.result ← Reg.base + Reg.output;
+        Reg.second ← Reg.queryCount; Reg.third ← Reg.modulus ]) x z 3 := by
+    ram_eval [z, hb, ho, hn, hm, haddr, Reg.result, Reg.second, Reg.third, Reg.base,
+      Reg.output, Reg.queryCount, Reg.modulus, QueriedProduct.output,
+      QueriedProduct.queryCount, Fin.mk.injEq]
+  obtain ⟨y, hy, ym, yr, yh⟩ :=
+    exec_normalizeBank (W := W) (b := b + o) (n := n) (M := M) z
+    (by simp [z, Reg.result, Reg.second, Reg.third])
+    (by simp [z, Reg.second, Reg.third]) (by simp [z]) hM (by
+      simpa only [Nat.add_assoc] using hfit)
+  refine ⟨y, (hz.seq hy).mono (by omega), ym, yr, ?_⟩
+  intro i hi
+  rw [yh i hi]
+  have h0 : i ≠ Reg.result := by intro h; subst i; simp [Reg.result] at hi
+  have h1 : i ≠ Reg.second := by intro h; subst i; simp [Reg.second] at hi
+  have h2 : i ≠ Reg.third := by intro h; subst i; simp [Reg.third] at hi
+  simp only [z, Data.set_regs, Function.update_of_ne h0, Function.update_of_ne h1,
+    Function.update_of_ne h2]
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Setup.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Setup.lean
new file mode 100644
index 0000000000..1baba6d4d3
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Setup.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Program
+
+/-!
+# Computed virtual width and register normalization
+
+Setup reads the actual original headers and executes the existing ceiling-logarithm and
+natural-power programs. No logarithm, modulus, bounded initial scratch or source register
+certificate is supplied in the input.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+
+private theorem clogBank_injective : Function.Injective clogBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 163 => k.val) h)
+
+private theorem powerBank_injective : Function.Injective powerBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 163 => k.val) h)
+
+/-- The explicit physical numerical margin covers setup and the smaller native source width. -/
+theorem setup_fits {W b N Q : ℕ} (hfit : Fits W (b + 4 * windowSize N Q + 1024)) :
+    sourceWidth N Q ≤ W ∧ N + Q + 3 ≤ windowSize N Q ∧
+      sourceWidth N Q < windowSize N Q := by
+  have hlog : Nat.clog 2 (N + Q + 3) ≤ sourceWidth N Q := by unfold sourceWidth; omega
+  have hp : N + Q + 3 ≤ windowSize N Q :=
+    (Nat.le_pow_clog (by decide) _).trans (Nat.pow_le_pow_right (by decide) hlog)
+  have hwidth : sourceWidth N Q < windowSize N Q := Nat.lt_two_pow_self
+  refine ⟨?_, hp, hwidth⟩
+  by_contra h
+  have hW : W ≤ sourceWidth N Q := by omega
+  have he := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hW
+  unfold Fits windowSize at hfit
+  omega
+
+/-- Actual setup computes the modulus, normalizes the fixed source register bank and preserves
+every caller memory word. Its charge is logarithmic in original dimensions and query count. -/
+theorem exec_setup {W b N Q : ℕ} (x : Data 163) (hb : x.regs Reg.base = b)
+    (hN : x.mem (b + 3) = N) (hQ : x.mem (b + 4) = Q)
+    (hfit : Fits W (b + 4 * windowSize N Q + 1024)) :
+    ∃ y, ExecWithin W setup x y (517 * Nat.clog 2 (N + Q + 3) + 184) ∧
+      y.mem = x.mem ∧
+      MemoryWindow.Matches (sourceWidth N Q) b
+        (MemoryWindow.view (sourceWidth N Q) b y) y ∧
+      (MemoryWindow.view (sourceWidth N Q) b y).Bounded (sourceWidth N Q) := by
+  change x.regs (160 : Fin 163) = b at hb
+  obtain ⟨hw, hS, hwidth⟩ := setup_fits hfit
+  have hc : Nat.clog 2 (N + Q + 3) ≤ sourceWidth N Q := by unfold sourceWidth; omega
+  have h0 : Fits W 0 := fits_zero _
+  have h2 : Fits W 2 := hfit.of_le (by omega)
+  have h3 : Fits W 3 := hfit.of_le (by omega)
+  have h4 : Fits W 4 := hfit.of_le (by omega)
+  have h128 : Fits W 128 := hfit.of_le (by omega)
+  have hb3 : Fits W (b + 3) := hfit.of_le (by omega)
+  have hb4 : Fits W (b + 4) := hfit.of_le (by omega)
+  have hsum : Fits W (N + Q) := hfit.of_le (by omega)
+  have hsize : Fits W (N + Q + 3) := hfit.of_le (by omega)
+  have hs1 : Fits W (N + Q + 3 + 1) := hfit.of_le (by omega)
+  have hc1 : Fits W (Nat.clog 2 (N + Q + 3) + 1) := hfit.of_le (by omega)
+  have hexp : Fits W (128 * Nat.clog 2 (N + Q + 3)) := by
+    apply hfit.of_le
+    change sourceWidth N Q ≤ _
+    omega
+  have hpfit : Fits W (2 ^ (128 * Nat.clog 2 (N + Q + 3)) +
+      128 * Nat.clog 2 (N + Q + 3) + 2) := by
+    apply hfit.of_le
+    change windowSize N Q + sourceWidth N Q + 2 ≤ _
+    omega
+  obtain ⟨s, hs, ss, sm, sb⟩ :
+      ∃ s, ExecWithin W readSize x s 9 ∧ s.regs Reg.result = N + Q + 3 ∧
+        s.mem = x.mem ∧ s.regs Reg.base = b := by
+    refine ⟨?s, ?run, ?result, ?memory, ?base⟩
+    case run => ram_eval [readSize, hb, hN, hQ, h3, h4, hb3, hb4, hsum, hsize,
+        Reg.result, Reg.second, Reg.base, Reg.address, Fin.mk.injEq]
+    case result => simp +decide
+    case memory => rfl
+    case base => simpa +decide [Reg.base, Function.update_apply] using hb
+  obtain ⟨l, hl, lr, lm, lo, lt⟩ := NatClog.exec_rename clogBank clogBank_injective s h2
+    (by change Fits W (s.regs Reg.result + 1); rw [ss]; exact hs1)
+    (by change Fits W (Nat.clog 2 (s.regs Reg.result) + 1); rw [ss]; exact hc1)
+  have lc : l.regs Reg.second = Nat.clog 2 (N + Q + 3) := by
+    change l.regs Reg.second = Nat.clog 2 (s.regs Reg.result) at lr
+    simpa only [ss] using lr
+  have lb : l.regs Reg.base = b := (hl.regs_eq (by
+    simp [NatClog.program, NatClog.body, Code.rename, Code.Preserves, Op.rename, Op.dest, Op.bin,
+      clogBank, Reg.base, NatClog.result, NatClog.arg,
+      NatClog.one, NatClog.two])).trans sb
+  let p := ((l.set Reg.third 128).set Reg.fourth
+    (Nat.clog 2 (N + Q + 3) * 128)).set Reg.third 2
+  have hexp' : Fits W (Nat.clog 2 (N + Q + 3) * 128) := by
+    simpa only [Nat.mul_comm] using hexp
+  have hprep : ExecWithin W
+      (ram[ Reg.third ← #128; Reg.fourth ← Reg.second * Reg.third; Reg.third ← #2 ]) l p 3 := by
+    ram_eval [p, lc, h128, h2, hexp', Reg.third, Reg.fourth, Reg.second,
+      Fin.mk.injEq]
+  obtain ⟨a, ha, av, ac, ao, am, ab, ae⟩ := Power.exec (w := W) 2
+    (128 * Nat.clog 2 (N + Q + 3)) (by decide) (p.comap powerBank)
+    (by simp [p, powerBank, Power.base, Reg.third, Reg.fourth])
+    (by simp [p, powerBank, Power.exponent, Reg.third, Reg.fourth, Nat.mul_comm]) hpfit
+  let z := a.extend powerBank p
+  have hz : ExecWithin W (Power.program.rename powerBank) p z
+      (4 * (128 * Nat.clog 2 (N + Q + 3)) + 5) := ha.rename powerBank_injective
+  have zv : z.regs Reg.result = windowSize N Q :=
+    (powerBank_injective.extend_apply _ _ Power.value).trans av
+  have zb : z.regs Reg.base = b := by
+    have hnot : ¬∃ i, powerBank i = Reg.base := by
+      rintro ⟨i, hi⟩
+      have := congrArg (fun k : Fin 163 => k.val) hi
+      simp only [powerBank, Reg.base, Fin.val_castAdd] at this
+      omega
+    change Function.extend powerBank a.regs p.regs Reg.base = b
+    rw [Function.extend_apply' _ _ _ hnot]
+    simpa [p, Reg.base, Reg.third, Reg.fourth,
+      Function.update_apply, Fin.mk.injEq] using lb
+  let z' := z.set Reg.modulus (windowSize N Q)
+  have hcopy : ExecWithin (B := .standard) W (.op (.copy Reg.modulus Reg.result)) z z' 1 := by
+    simpa only [z', zv] using
+      (ExecWithin.copy (B := .standard) (w := W) (x := z) (d := Reg.modulus) (s := Reg.result))
+  have z'b : z'.regs Reg.base = b := by
+    simpa [z', Reg.base, Reg.modulus,
+      Function.update_apply, Fin.mk.injEq] using zb
+  have z'm : z'.regs Reg.modulus = 2 ^ sourceWidth N Q := by simp [z', windowSize]
+  obtain ⟨y, hy, ym, ymatch, ybound, yr⟩ := MemoryWindow.exec_normalizeRegisters
+    z' z'b z'm hw
+  refine ⟨y, ?_, ?_, ymatch, ybound⟩
+  · apply (hs.seq (hl.seq (hprep.seq (hz.seq (hcopy.seq hy))))).mono
+    change 9 + (5 * Nat.clog 2 (s.regs Reg.result) + 5 + _) ≤ _
+    rw [ss]
+    omega
+  · exact ym.trans (am.trans (lm.trans sm))
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Width.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Width.lean
new file mode 100644
index 0000000000..c10ab26190
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Callable/Width.lean
@@ -0,0 +1,183 @@
+/-
+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.Callable.Bounds
+
+/-!
+# Every-wide-width initialized callable product
+
+The width threshold depends only on original row/occurrence counts and the length/word bound of
+the protected caller prefix. The actual program never reads physical width. Generic execution
+does not assume query sparsity; only the final quantitative saving does.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Positive logarithmic physical width derived entirely from original input and caller data. -/
+@[expose] def admissionWidth (caller : List ℕ) (N Q P : ℕ) : ℕ :=
+  256 * Nat.clog 2 (inputBase caller + N + Q + P + 5)
+
+/-- The concrete threshold remains positive at all boundary parameters. -/
+theorem admissionWidth_pos (caller : List ℕ) (N Q P : ℕ) : 0 < admissionWidth caller N Q P :=
+  Nat.mul_pos (by decide) (Nat.clog_pos (by decide) (by omega))
+
+/-- Physical admission covers both the computed virtual window and all caller-prefix words. -/
+theorem admission_bounds {W N Q P : ℕ} (caller : List ℕ)
+    (hP : ∀ v ∈ caller, v ≤ P) (hW : admissionWidth caller N Q P ≤ W) :
+    Fits W (inputBase caller + 4 * windowSize N Q + 1024) ∧
+      ∀ v ∈ caller, Fits W v := by
+  have hc : Nat.clog 2 (inputBase caller + N + Q + P + 5) ≤ W := by
+    unfold admissionWidth at hW
+    omega
+  refine ⟨physical_fits ?_, ?_⟩
+  · have h := Nat.clog_mono_right 2 (by omega :
+      inputBase caller + N + Q + 5 ≤ inputBase caller + N + Q + P + 5)
+    unfold admissionWidth at hW
+    omega
+  · intro v hv
+    have h := hP v hv
+    have hceil := Nat.le_pow_clog (by decide : 1 < (2 : ℕ))
+      (inputBase caller + N + Q + P + 5)
+    have hpow := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hc
+    change v < 2 ^ W
+    omega
+
+private theorem context_fits {W b N Q P : ℕ}
+    (hW : 256 * Nat.clog 2 (b + N + Q + P + 5) ≤ W) : Fits W P := by
+  have hc : Nat.clog 2 (b + N + Q + P + 5) ≤ W := by omega
+  have hceil := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (b + N + Q + P + 5)
+  have hpow := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hc
+  change P < 2 ^ W
+  omega
+
+/-- Every native caller prefix is physically word-bounded, including a loaded dirty word
+before the following remainder. Here `P` bounds every initial register and memory word,
+not merely the source input or normalized values. It is an initial-data bound, not a bound
+on intermediates supplied by the caller. -/
+theorem caller_prefix_bounded {W b N Q P k : ℕ} {x : Data 163} {z : State 163}
+    (hregs : ∀ i, x.regs i ≤ P) (hmem : ∀ a, x.mem a ≤ P)
+    (hW : 256 * Nat.clog 2 (b + N + Q + P + 5) ≤ W)
+    (hr : Runs W (program.program Reg.result) ⟨0, x⟩ z k) : z.data.Bounded W :=
+  hr.bounded ⟨fun i => (context_fits hW).of_le (hregs i),
+    fun a => (context_fits hW).of_le (hmem a)⟩
+
+/-- Actual callable flat runs at every admitted physical width, with arbitrary dirty initial
+workspace bounded by `P`. This is the interface for a real producer's reachable caller state:
+`P` bounds all its initial words, including dirty pre-modulo loads. Original local input words
+derive the concrete source execution; no solver, run, time, routing or layout certificate is
+assumed. The same final `y` contains exact answers, restored input and the caller frame. -/
+theorem runs_caller {W b m N P : ℕ}
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (x : Data 163) (hb : x.regs Reg.base = b)
+    (hinput : ∀ a, a < QueriedProduct.inputEnd m N qs.length →
+      x.mem (b + a) =
+        (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hN : D m ^ 18 ≤ N) (hregs : ∀ i, x.regs i ≤ P) (hmem : ∀ a, x.mem a ≤ P)
+    (hW : 256 * Nat.clog 2 (b + N + qs.length + P + 5) ≤ W) :
+    ∃ y n, n ≤ timeBound (m := m) qs ∧
+      Runs W (program.program Reg.result) ⟨0, x⟩ ⟨program.size, y⟩ n ∧
+      Executes W (program.program Reg.result) ⟨0, x⟩
+        (b + QueriedProduct.outputBase (19 * m) m N qs.length) (n + 1) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length,
+        y.mem (b + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length → y.mem (b + a) = x.mem (b + a)) ∧
+      (∀ a, a < b ∨ b + windowSize N qs.length ≤ a → y.mem a = x.mem a) := by
+  have hfit : Fits W (b + 4 * windowSize N qs.length + 1024) := by
+    apply physical_fits
+    have h := Nat.clog_mono_right 2 (by omega :
+      b + N + qs.length + 5 ≤ b + N + qs.length + P + 5)
+    omega
+  obtain ⟨y, hy, yr, yb, yM, hv, hi, hf⟩ := exec X Y qs x hb hinput hX hY hN hfit
+  have hx : x.Bounded W := ⟨fun i => (context_fits hW).of_le (hregs i),
+    fun a => (context_fits hW).of_le (hmem a)⟩
+  have ybound := hy.bounded hx
+  obtain ⟨n, hn, hy⟩ := hy
+  refine ⟨y, n, hn, ?_, ?_, ybound, hv, hi, hf⟩
+  · simpa only [Nat.zero_add] using hy.runs (pc := 0)
+      (p := program.program Reg.result) (Program.Contains.self _).append_left
+  · simpa only [yr] using hy.executes Reg.result
+
+/-- At every admitted physical width, the initialized callable program returns all requested
+exact product words and preserves caller/local-input memory. No sparsity premise is used. -/
+theorem runs_wide {W m N P : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hP : ∀ v ∈ caller, v ≤ P) (hW : admissionWidth caller N qs.length P ≤ W) :
+    InputFits W (input caller X Y qs) ∧
+    ∃ y n, n + 1 ≤ timeBound (m := m) qs + 3 ∧
+      Runs W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        ⟨entryProgram.size, y⟩ n ∧
+      Executes W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        (inputBase caller + QueriedProduct.outputBase (19 * m) m N qs.length) (n + 1) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length,
+        y.mem (inputBase caller + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length →
+        y.mem (inputBase caller + a) =
+          (State.init (input caller X Y qs) : State 163).data.mem (inputBase caller + a)) ∧
+      (∀ a, a < inputBase caller ∨ inputBase caller + windowSize N qs.length ≤ a →
+        y.mem a = (State.init (input caller X Y qs) : State 163).data.mem a) := by
+  obtain ⟨hfit, hcaller⟩ := admission_bounds caller hP hW
+  obtain ⟨hi, y, n, hn, hr, he, hy, hv, hin, hf⟩ := runs caller X Y qs hN hX hY hcaller hfit
+  exact ⟨hi, y, n, by omega, hr, he, hy, hv, hin, hf⟩
+
+/-- Every initialized prefix, including raw dirty loads before normalization, fits the admitted
+physical width. Outside the explicit original input the initialized memory is zero. Thus `P`
+in this initialized interface need only bound the protected caller prefix. -/
+theorem bounded_reachable {W m N P k : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hP : ∀ v ∈ caller, v ≤ P) (hW : admissionWidth caller N qs.length P ≤ W)
+    {z : State 163}
+    (hz : Runs W (entryProgram.program Reg.result) (State.init (input caller X Y qs)) z k) :
+    z.data.Bounded W := by
+  obtain ⟨hfit, hcaller⟩ := admission_bounds caller hP hW
+  exact hz.bounded_init (input_fits caller X Y qs hN hX hY hcaller hfit)
+
+/-- Complete actual initialized thin saving, including base loading, all translated memory
+accesses, span normalization and halt. The occurrence bound is explicit and stronger than a
+distinct-set bound for lists containing duplicate requests. -/
+theorem runs_thin {W m N P : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (hN : D m ^ 18 ≤ N) (hQ : qs.length * 2 ^ m ≤ N ^ 2)
+    (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1)
+    (hP : ∀ v ∈ caller, v ≤ P) (hW : admissionWidth caller N qs.length P ≤ W) :
+    InputFits W (input caller X Y qs) ∧
+    ∃ y n,
+      Runs W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        ⟨entryProgram.size, y⟩ n ∧
+      Executes W (entryProgram.program Reg.result) (State.init (input caller X Y qs))
+        (inputBase caller + QueriedProduct.outputBase (19 * m) m N qs.length) (n + 1) ∧
+      ((n + 1 : ℕ) : ℝ) ≤
+        17301504 * ((19 * m + 1 : ℕ) : ℝ) * (N : ℝ) ^ 2 / (D m : ℝ) ^ (1 / 18 : ℝ) ∧
+      y.Bounded W ∧
+      (∀ i : Fin qs.length,
+        y.mem (inputBase caller + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) =
+          Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧
+      (∀ a, a < QueriedProduct.inputEnd m N qs.length →
+        y.mem (inputBase caller + a) =
+          (State.init (input caller X Y qs) : State 163).data.mem (inputBase caller + a)) ∧
+      (∀ a, a < inputBase caller ∨ inputBase caller + windowSize N qs.length ≤ a →
+        y.mem a = (State.init (input caller X Y qs) : State 163).data.mem a) := by
+  obtain ⟨hi, y, n, hn, hr, he, hy, hv, hin, hf⟩ := runs_wide caller X Y qs hN hX hY hP hW
+  have hnR : ((n + 1 : ℕ) : ℝ) ≤ (timeBound (m := m) qs + 3 : ℕ) := by exact_mod_cast hn
+  exact ⟨hi, y, n, hr, he, hnR.trans (thin_timeBound_sparse qs hN hQ), hy, hv, hin, hf⟩
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct
diff --git a/Complexity/Computability/WordRAM/ArrayNormalize.lean b/Complexity/Computability/WordRAM/ArrayNormalize.lean
new file mode 100644
index 0000000000..e0d6123bb5
--- /dev/null
+++ b/Complexity/Computability/WordRAM/ArrayNormalize.lean
@@ -0,0 +1,137 @@
+/-
+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.Computability.WordRAM.Notation
+
+/-!
+# Charged in-place normalization of an array
+
+`ArrayNormalize.program` replaces each word of a supplied interval by its remainder modulo a
+supplied positive modulus. It executes actual loads, remainders and stores; the untouched
+memory need not already be normalized. This small topic module avoids adding an application
+specific transformation to the allocation API.
+-/
+
+public section
+
+namespace Cslib.WordRAM.ArrayNormalize
+
+/-- First address to normalize. -/
+abbrev base : Fin 7 := 0
+/-- Number of words. -/
+abbrev length : Fin 7 := 1
+/-- Positive normalization modulus. -/
+abbrev modulus : Fin 7 := 2
+/-- Current index. -/
+abbrev index : Fin 7 := 3
+/-- Temporary absolute address. -/
+abbrev address : Fin 7 := 4
+/-- Loaded and normalized word. -/
+abbrev value : Fin 7 := 5
+/-- Constant one. -/
+abbrev one : Fin 7 := 6
+
+/-- Normalize one cell with five actual native instructions. -/
+@[expose] def body : Code .standard 7 := ram[
+  address ← base + index; value ← *address; value ← value % modulus;
+  *address ← value; index ← index + one ]
+
+/-- Fixed code for in-place normalization of an interval supplied in registers. -/
+@[expose] def program : Code .standard 7 :=
+  .seq (ram[ index ← #0; one ← #1 ]) (.loop (.lt index length) body)
+
+/-- Mathematical memory after normalizing a prefix; this is not a machine operation. -/
+def normalizePrefix (mem : ℕ → ℕ) (b M k : ℕ) : ℕ → ℕ :=
+  fun a => if b ≤ a ∧ a < b + k then mem a % M else mem a
+
+/-- Every cell in the normalized interval contains its original remainder. -/
+theorem normalizePrefix_read (mem : ℕ → ℕ) (b M n j : ℕ) (hj : j < n) :
+    normalizePrefix mem b M n (b + j) = mem (b + j) % M := by
+  simp [normalizePrefix, hj]
+
+/-- Normalizing an interval leaves all outside memory unchanged. -/
+theorem normalizePrefix_outside (mem : ℕ → ℕ) (b M n a : ℕ)
+    (ha : ¬(b ≤ a ∧ a < b + n)) : normalizePrefix mem b M n a = mem a := by
+  simp [normalizePrefix, ha]
+
+private theorem normalizePrefix_succ (mem : ℕ → ℕ) (b M k : ℕ) :
+    normalizePrefix mem b M (k + 1) =
+      Function.update (normalizePrefix mem b M k) (b + k) (mem (b + k) % M) := by
+  funext a
+  by_cases ha : a = b + k
+  · subst a; simp [normalizePrefix]
+  · simp only [normalizePrefix, Function.update_of_ne ha]
+    have h : (b ≤ a ∧ a < b + (k + 1)) ↔ (b ≤ a ∧ a < b + k) := by omega
+    simp only [h]
+
+private theorem normalizePrefix_zero (mem : ℕ → ℕ) (b M : ℕ) :
+    normalizePrefix mem b M 0 = mem := by
+  funext a
+  simp [normalizePrefix]
+
+/-- In-place normalization costs at most `7n+4` native instructions, including every indexed
+load/store and loop decision. The input arguments and all outside memory are preserved. -/
+theorem exec {W b M n : ℕ} (x : Data 7) (hb : x.regs base = b)
+    (hn : x.regs length = n) (hm : x.regs modulus = M) (hM : 0 < M)
+    (hfit : Fits W (b + n + M + 2)) :
+    ∃ y, ExecWithin W program x y (7 * n + 4) ∧ y.mem = normalizePrefix x.mem b M n ∧
+      y.regs base = b ∧ y.regs length = n ∧ y.regs modulus = M := by
+  have h0 : Fits W 0 := fits_zero _
+  have h1 : Fits W 1 := hfit.of_le (by omega)
+  let start := (x.set index 0).set one 1
+  have hs : ExecWithin (B := .standard) W (ram[ index ← #0; one ← #1 ]) x start 2 := by
+    ram_eval [start, h0, h1]
+  let I (y : Data 7) : Prop := y.regs base = b ∧ y.regs length = n ∧
+    y.regs modulus = M ∧ y.regs one = 1 ∧ y.regs index ≤ n ∧
+    y.mem = normalizePrefix x.mem b M (y.regs index)
+  have hi : I start := by
+    simp [I, start, normalizePrefix_zero, hb, hn, hm, base, length, modulus, index, one]
+  have step (y : Data 7) (hy : I y) (hc : (Cond.lt index length).Holds y) :
+      ∃ z, ExecWithin W body y z 5 ∧ I z ∧ n - z.regs index < n - y.regs index := by
+    obtain ⟨yb, yn, ym, yo, yi, ymem⟩ := hy
+    have hlt : y.regs index < n := by simpa only [Cond.holds_lt, yn] using hc
+    have ha : Fits W (b + y.regs index) := hfit.of_le (by omega)
+    have hv : Fits W (x.mem (b + y.regs index) % M) :=
+      hfit.of_le ((Nat.mod_lt _ hM).le.trans (by omega))
+    have hj : Fits W (y.regs index + 1) := hfit.of_le (by omega)
+    have hread : y.mem (b + y.regs index) = x.mem (b + y.regs index) := by
+      rw [ymem]
+      simp [normalizePrefix]
+    let z := ((((y.set address (b + y.regs index)).set value
+      (x.mem (b + y.regs index))).set value
+      (x.mem (b + y.regs index) % M)).write (b + y.regs index)
+        (x.mem (b + y.regs index) % M)).set index (y.regs index + 1)
+    have he : ExecWithin W body y z 5 := by
+      ram_eval [body, z, yb, ym, yo, hread, ha, hv, hj,
+        base, length, modulus, index, address, value, one, Fin.mk.injEq]
+    refine ⟨z, he, ?_, ?_⟩
+    · refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [z, Function.update_apply] using yb
+      · simpa +decide [z, Function.update_apply] using yn
+      · simpa +decide [z, Function.update_apply] using ym
+      · simpa +decide [z, Function.update_apply] using yo
+      · simpa +decide [z, Function.update_apply] using (show y.regs index + 1 ≤ n by omega)
+      · simpa +decide only [z, Data.set_regs, Data.set_mem, Data.write_regs, Data.write_mem,
+          Function.update_apply, ymem, index, address, value, one, Fin.reduceEq, ↓reduceIte] using
+          (normalizePrefix_succ x.mem b M (y.regs index)).symm
+    · simp only [z, Data.set_regs, Function.update_self]
+      omega
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I (fun y => n - y.regs index) step hi
+  have hj : y.regs index = n := by
+    have := hy.2.2.2.2.1
+    simp only [Cond.holds_lt, hy.2.1] at hc
+    omega
+  refine ⟨y, ?_, ?_, hy.1, hy.2.1, hy.2.2.1⟩
+  · apply (hs.seq he).mono
+    have hstart : start.regs index = 0 := by simp [start, index, one]
+    rw [hstart]
+    omega
+  · simpa only [hj] using hy.2.2.2.2.2
+
+end Cslib.WordRAM.ArrayNormalize
diff --git a/Complexity/Computability/WordRAM/MemoryWindow.lean b/Complexity/Computability/WordRAM/MemoryWindow.lean
new file mode 100644
index 0000000000..ee191ca498
--- /dev/null
+++ b/Complexity/Computability/WordRAM/MemoryWindow.lean
@@ -0,0 +1,400 @@
+/-
+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.Computability.WordRAM.Structured
+
+/-!
+# Native programs in a caller-owned memory window
+
+`MemoryWindow.compile` translates standard native code to use a runtime memory base. Three
+additional registers hold the base, the source word modulus and an address temporary. A load
+executes an addition, a load and a remainder; a store executes an addition and a store. Other
+instructions and all branch decisions retain the source register values.
+
+`MemoryWindow.view` clips memory words to the source width. Consequently arbitrary dirty memory
+in the caller's window is allowed: no bulk initialization or copying of that window is implicit
+in the translation. The view is only a relation between ordinary native data, not a new machine
+or execution semantics. Source executions must still be established using `WordRAM.Exec`.
+
+This compiler is original native program work. It does not supply an algorithm, an execution
+certificate or a bound for any source program.
+-/
+
+public section
+
+namespace Cslib.WordRAM.MemoryWindow
+
+variable {r : ℕ}
+
+namespace Reg
+
+/-- Runtime address of source memory cell zero. -/
+@[expose] def base : Fin (r + 3) := ⟨r, by omega⟩
+
+/-- Runtime value `2^w` for the source word width `w`. -/
+@[expose] def modulus : Fin (r + 3) := ⟨r + 1, by omega⟩
+
+/-- Temporary absolute address used by translated loads and stores. -/
+@[expose] def address : Fin (r + 3) := ⟨r + 2, by omega⟩
+
+end Reg
+
+/-- One source instruction with actual address additions and load normalization. -/
+@[expose] def compileOp : Op .standard r → Code .standard (r + 3)
+  | .load d a =>
+      .seq (.op (.bin .add Reg.address Reg.base (a.castAdd 3)))
+        (.seq (.op (.load (d.castAdd 3) Reg.address))
+          (.op (.bin .mod (d.castAdd 3) (d.castAdd 3) Reg.modulus)))
+  | .store a s =>
+      .seq (.op (.bin .add Reg.address Reg.base (a.castAdd 3)))
+        (.op (.store Reg.address (s.castAdd 3)))
+  | o => .op (o.rename (Fin.castAdd 3))
+
+/-- Rebase all memory accesses, retaining ordinary native branching and loop control. -/
+@[expose] def compile : Code .standard r → Code .standard (r + 3)
+  | .op o => compileOp o
+  | .seq a b => .seq (compile a) (compile b)
+  | .branch c a b => .branch (c.rename (Fin.castAdd 3)) (compile a) (compile b)
+  | .loop c a => .loop (c.rename (Fin.castAdd 3)) (compile a)
+  | .rand d s => .rand (d.castAdd 3) (s.castAdd 3)
+
+/-- Source data represented by a target register bank and clipped, shifted memory. -/
+@[expose] def view (w b : ℕ) (x : Data (r + 3)) : Data r :=
+  ⟨fun i => x.regs (i.castAdd 3), fun a => x.mem (b + a) % 2 ^ w⟩
+
+/-- Ordinary value equalities relating source and target native data. -/
+structure Matches (w b : ℕ) (x : Data r) (y : Data (r + 3)) : Prop where
+  /-- The source register bank and clipped memory agree. -/
+  view_eq : view w b y = x
+  /-- The base register has the chosen runtime address. -/
+  base_eq : y.regs Reg.base = b
+  /-- The modulus register has the source word modulus. -/
+  modulus_eq : y.regs Reg.modulus = 2 ^ w
+
+/-- The compiler expands a flat instruction into at most three instructions. -/
+theorem size_compileOp (o : Op .standard r) : (compileOp o).size ≤ 3 := by
+  cases o <;> simp [compileOp]
+
+/-- Branches and loop overhead also satisfy the factor-three code-size bound. -/
+theorem size_compile (c : Code .standard r) : (compile c).size ≤ 3 * c.size := by
+  induction c with
+  | op o => exact size_compileOp o
+  | seq a b ha hb | branch c a b ha hb => simp only [compile, Code.size]; omega
+  | loop c a ha => simp only [compile, Code.size]; omega
+  | rand => simp [compile]
+
+/-- Memory rebasing introduces no reads of the physical word width. -/
+theorem readsWidth_compileOp (o : Op .standard r) : (compileOp o).ReadsWidth ↔ o.ReadsWidth := by
+  cases o <;> simp [compileOp, Code.ReadsWidth, Op.rename, Op.ReadsWidth, Op.bin]
+
+/-- The compiled code reads the word width exactly when the source does. -/
+theorem readsWidth_compile (c : Code .standard r) : (compile c).ReadsWidth ↔ c.ReadsWidth := by
+  induction c <;> simp_all [compile, Code.ReadsWidth, readsWidth_compileOp]
+
+private theorem bank_ne_base (i : Fin r) : i.castAdd 3 ≠ (Reg.base : Fin (r + 3)) := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.val_castAdd, Reg.base] at this
+  omega
+
+private theorem bank_ne_modulus (i : Fin r) : i.castAdd 3 ≠ (Reg.modulus : Fin (r + 3)) := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.val_castAdd, Reg.modulus] at this
+  omega
+
+private theorem bank_ne_address (i : Fin r) : i.castAdd 3 ≠ (Reg.address : Fin (r + 3)) := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.val_castAdd, Reg.address] at this
+  omega
+
+private theorem view_set (w b : ℕ) (x : Data (r + 3)) (i : Fin r) (v : ℕ) :
+    view w b (x.set (i.castAdd 3) v) = (view w b x).set i v := by
+  ext j
+  · change Function.update x.regs (i.castAdd 3) v (j.castAdd 3) =
+      Function.update (fun k : Fin r => x.regs (k.castAdd 3)) i v j
+    by_cases h : j = i
+    · subst j; simp
+    · have h' : j.castAdd 3 ≠ i.castAdd 3 := by
+        intro he
+        apply h
+        exact Fin.ext (congrArg (fun k : Fin (r + 3) => k.val) he)
+      simp only [Function.update_of_ne h, Function.update_of_ne h']
+  · rfl
+
+private theorem view_address (w b : ℕ) (x : Data (r + 3)) (v : ℕ) :
+    view w b (x.set Reg.address v) = view w b x := by
+  ext j
+  · exact Function.update_of_ne (bank_ne_address j) _ _
+  · rfl
+
+private theorem view_write (w b : ℕ) (x : Data (r + 3)) (a v : ℕ) (hv : Fits w v) :
+    view w b (x.write (b + a) v) = (view w b x).write a v := by
+  ext j
+  · rfl
+  · change Function.update x.mem (b + a) v (b + j) % 2 ^ w =
+      Function.update (fun k => x.mem (b + k) % 2 ^ w) a v j
+    by_cases h : j = a
+    · subst j; simp [Nat.mod_eq_of_lt hv]
+    · have h' : b + j ≠ b + a := by omega
+      simp [Function.update_of_ne h, Function.update_of_ne h']
+
+/-- Matching source registers have their exact target-bank values. -/
+theorem Matches.regs {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (i : Fin r) : y.regs (i.castAdd 3) = x.regs i :=
+  congrArg (fun z : Data r => z.regs i) h.view_eq
+
+/-- Matching source memory has the clipped target word at its shifted address. -/
+theorem Matches.mem {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (a : ℕ) : y.mem (b + a) % 2 ^ w = x.mem a :=
+  congrArg (fun z : Data r => z.mem a) h.view_eq
+
+private theorem Matches.set {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (i : Fin r) (v : ℕ) :
+    Matches w b (x.set i v) (y.set (i.castAdd 3) v) := by
+  refine ⟨by rw [view_set, h.view_eq], ?_, ?_⟩
+  · simpa only [Data.set_regs, Function.update_of_ne (Ne.symm (bank_ne_base i))] using h.base_eq
+  · simpa only [Data.set_regs, Function.update_of_ne (Ne.symm (bank_ne_modulus i))] using
+      h.modulus_eq
+
+private theorem Matches.address {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (v : ℕ) : Matches w b x (y.set Reg.address v) := by
+  refine ⟨by rw [view_address, h.view_eq], ?_, ?_⟩
+  · simpa [Reg.base, Reg.address, Function.update_apply, Fin.mk.injEq] using h.base_eq
+  · simpa [Reg.modulus, Reg.address, Function.update_apply, Fin.mk.injEq] using h.modulus_eq
+
+private theorem Matches.write {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (a v : ℕ) (hv : Fits w v) :
+    Matches w b (x.write a v) (y.write (b + a) v) :=
+  ⟨by rw [view_write _ _ _ _ _ hv, h.view_eq], h.base_eq, h.modulus_eq⟩
+
+private theorem set_overwrite (x : Data r) (i : Fin r) (u v : ℕ) :
+    (x.set i u).set i v = x.set i v := by
+  ext j
+  · simp only [Data.set_regs, Function.update_idem]
+  · rfl
+
+/-- A translated source instruction has actual native execution within three instructions.
+All source addresses fit the bounded source word, so the only writes are inside the runtime
+window. Dirty words are normalized by the translated load itself. -/
+theorem exec_compileOp {w W b : ℕ} {o : Op .standard r} {x x' : Data r}
+    {y : Data (r + 3)} (ho : ¬o.ReadsWidth) (he : o.eval w x = some x')
+    (hx : x.Bounded w) (hxy : Matches w b x y) (hw : w ≤ W)
+    (hfit : Fits W (b + 2 ^ w)) :
+    ∃ y', ExecWithin W (compileOp o) y y' 3 ∧ Matches w b x' y' ∧
+      ∀ a, a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a := by
+  cases o with
+  | const d v =>
+    obtain ⟨hv, rfl⟩ := Data.put_eq_some.1 he
+    refine ⟨y.set (d.castAdd 3) v, (ExecWithin.const (hv.mono hw)).mono (by omega),
+      hxy.set d v, fun _ _ => rfl⟩
+  | copy d s =>
+    simp only [Op.eval, Option.some.injEq] at he
+    subst x'
+    refine ⟨y.set (d.castAdd 3) (x.regs s), ?_, hxy.set d _, fun _ _ => rfl⟩
+    simpa only [compileOp, Op.rename, hxy.regs s] using
+      (ExecWithin.copy (w := W) (B := .standard) (d := d.castAdd 3)
+        (s := s.castAdd 3) (x := y)).mono (by omega : 1 ≤ 3)
+  | alu f d args =>
+    obtain ⟨v, hf, hv, rfl⟩ := Op.eval_alu_eq_some.1 he
+    have hargs : y.regs ∘ (Fin.castAdd 3 ∘ args) = x.regs ∘ args := by
+      funext i
+      exact hxy.regs (args i)
+    have hf' := Basis.standard.interp_mono_of_not_readsWidth f ho hw hf hv
+    refine ⟨y.set (d.castAdd 3) v, ?_, hxy.set d v, fun _ _ => rfl⟩
+    exact (ExecWithin.alu (by rw [hargs]; exact hf') (hv.mono hw)).mono (by omega)
+  | load d a =>
+    simp only [Op.eval, Option.some.injEq] at he
+    subst x'
+    have ha : Fits W (b + x.regs a) := hfit.of_le (by have := hx.1 a; unfold Fits at this; omega)
+    let z := y.set Reg.address (b + x.regs a)
+    have hz : Matches w b x z := hxy.address _
+    have had : z.regs Reg.address = b + x.regs a := by simp [z]
+    have h1 : ExecWithin W
+        (.op (.bin .add Reg.address Reg.base (a.castAdd 3))) y z 1 := by
+      simpa only [BinOp.eval, hxy.base_eq, hxy.regs a] using
+        (ExecWithin.bin (f := .add) (d := Reg.address) (i := Reg.base)
+          (j := a.castAdd 3) (x := y) (w := W) (by simpa [hxy.base_eq, hxy.regs a] using ha))
+    let z' := z.set (d.castAdd 3) (y.mem (b + x.regs a))
+    have h2 : ExecWithin (B := .standard) W (.op (.load (d.castAdd 3) Reg.address)) z z' 1 := by
+      simpa only [had, z, Data.set_mem] using
+        (ExecWithin.load (w := W) (B := .standard) (x := z)
+          (d := d.castAdd 3) (a := Reg.address))
+    have hmod : z'.regs Reg.modulus = 2 ^ w := by
+      simpa only [z', Data.set_regs,
+        Function.update_of_ne (Ne.symm (bank_ne_modulus d))] using hz.modulus_eq
+    have hd : z'.regs (d.castAdd 3) = y.mem (b + x.regs a) := by simp [z']
+    have hm : y.mem (b + x.regs a) % 2 ^ w = x.mem (x.regs a) := hxy.mem _
+    have h3 : ExecWithin W
+        (.op (.bin .mod (d.castAdd 3) (d.castAdd 3) Reg.modulus)) z'
+        (z'.set (d.castAdd 3) (x.mem (x.regs a))) 1 := by
+      simpa only [BinOp.eval, hd, hmod, hm] using
+        (ExecWithin.bin (f := .mod) (d := d.castAdd 3) (i := d.castAdd 3)
+          (j := Reg.modulus) (x := z') (w := W)
+          (by simpa only [BinOp.eval, hd, hmod, hm] using (hx.2 (x.regs a)).mono hw))
+    refine ⟨z'.set (d.castAdd 3) (x.mem (x.regs a)), ?_, ?_, fun _ _ => rfl⟩
+    · exact h1.seq (h2.seq h3)
+    · change Matches w b (x.set d _) ((z.set (d.castAdd 3) _).set (d.castAdd 3) _)
+      rw [set_overwrite]
+      exact hz.set d _
+  | store a s =>
+    simp only [Op.eval, Option.some.injEq] at he
+    subst x'
+    have ha : Fits W (b + x.regs a) := hfit.of_le (by have := hx.1 a; unfold Fits at this; omega)
+    let z := y.set Reg.address (b + x.regs a)
+    have hz : Matches w b x z := hxy.address _
+    have had : z.regs Reg.address = b + x.regs a := by simp [z]
+    have h1 : ExecWithin W
+        (.op (.bin .add Reg.address Reg.base (a.castAdd 3))) y z 1 := by
+      simpa only [BinOp.eval, hxy.base_eq, hxy.regs a] using
+        (ExecWithin.bin (f := .add) (d := Reg.address) (i := Reg.base)
+          (j := a.castAdd 3) (x := y) (w := W) (by simpa [hxy.base_eq, hxy.regs a] using ha))
+    have h2 : ExecWithin (B := .standard) W (.op (.store Reg.address (s.castAdd 3))) z
+        (z.write (b + x.regs a) (x.regs s)) 1 := by
+      simpa only [had, hz.regs s] using
+        (ExecWithin.store (w := W) (B := .standard) (x := z)
+          (a := Reg.address) (s := s.castAdd 3))
+    refine ⟨z.write (b + x.regs a) (x.regs s), (h1.seq h2).mono (by omega),
+      hz.write _ _ (hx.1 s), ?_⟩
+    intro j hj
+    have hja : j ≠ b + x.regs a := by
+      have := hx.1 a
+      unfold Fits at this
+      omega
+    exact Function.update_of_ne hja _ _
+
+private theorem Matches.holds {w b : ℕ} {x : Data r} {y : Data (r + 3)}
+    (h : Matches w b x y) (c : Cond r) : (c.rename (Fin.castAdd 3)).Holds y ↔ c.Holds x := by
+  cases c <;> simp only [Cond.rename, Cond.Holds, h.regs]
+
+/-- Clipped memory is source-word bounded whenever the represented register bank is bounded.
+No condition is imposed on the unnormalized physical memory words. -/
+theorem view_bounded (w b : ℕ) (y : Data (r + 3))
+    (hregs : ∀ i : Fin r, Fits w (y.regs (i.castAdd 3))) : (view w b y).Bounded w :=
+  ⟨hregs, fun _ => Nat.mod_lt _ (Nat.two_pow_pos _)⟩
+
+/-- Every actual bounded deterministic source execution gives an actual target execution with
+at most three times its charged instructions. The base and modulus survive, source registers
+and clipped memory agree, and the entire caller memory outside the reserved window survives.
+This is a compiler correctness rule over the existing native `Exec`, not an assumed execution
+contract for an algorithm. -/
+theorem exec {w W b : ℕ} {c : Code .standard r} {x x' : Data r} {n : ℕ}
+    (he : Exec w c x x' n) (hc : ¬c.ReadsWidth) (hx : x.Bounded w)
+    {y : Data (r + 3)} (hxy : Matches w b x y) (hw : w ≤ W)
+    (hfit : Fits W (b + 2 ^ w)) :
+    ∃ y', ExecWithin W (compile c) y y' (3 * n) ∧ Matches w b x' y' ∧
+      ∀ a, a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a := by
+  induction he generalizing y with
+  | op ho => exact exec_compileOp hc ho hx hxy hw hfit
+  | seq h₁ h₂ ih₁ ih₂ =>
+    obtain ⟨z, hz, hzm, hzf⟩ := ih₁ (fun h => hc (Or.inl h)) hx hxy
+    obtain ⟨z', hz', hz'm, hz'f⟩ := ih₂ (fun h => hc (Or.inr h)) (h₁.bounded hx) hzm
+    refine ⟨z', (hz.seq hz').mono (by omega), hz'm, ?_⟩
+    intro a ha
+    exact (hz'f a ha).trans (hzf a ha)
+  | branch_pos hp h ih =>
+    obtain ⟨z, hz, hzm, hzf⟩ := ih (fun h => hc (Or.inl h)) hx hxy
+    refine ⟨z, ?_, hzm, hzf⟩
+    exact (ExecWithin.branch_pos ((hxy.holds _).2 hp) hz).mono (by omega)
+  | branch_neg hp h ih =>
+    obtain ⟨z, hz, hzm, hzf⟩ := ih (fun h => hc (Or.inr h)) hx hxy
+    refine ⟨z, ?_, hzm, hzf⟩
+    exact (ExecWithin.branch_neg (fun h => hp ((hxy.holds _).1 h)) hz).mono (by omega)
+  | loop_exit hp =>
+    refine ⟨y, ?_, hxy, fun _ _ => rfl⟩
+    exact (Exec.loop_exit (fun h => hp ((hxy.holds _).1 h))).within.mono (by omega)
+  | loop_iter hp h₁ h₂ ih₁ ih₂ =>
+    obtain ⟨z, hz, hzm, hzf⟩ := ih₁ hc hx hxy
+    obtain ⟨z', hz', hz'm, hz'f⟩ := ih₂ hc (h₁.bounded hx) hzm
+    refine ⟨z', ?_, hz'm, ?_⟩
+    · exact (ExecWithin.loop_iter ((hxy.holds _).2 hp) hz hz').mono (by omega)
+    · intro a ha
+      exact (hz'f a ha).trans (hzf a ha)
+
+/-- The bounded-time form of memory-window compiler correctness. -/
+theorem execWithin {w W b T : ℕ} {c : Code .standard r} {x x' : Data r}
+    (he : ExecWithin w c x x' T) (hc : ¬c.ReadsWidth) (hx : x.Bounded w)
+    {y : Data (r + 3)} (hxy : Matches w b x y) (hw : w ≤ W)
+    (hfit : Fits W (b + 2 ^ w)) :
+    ∃ y', ExecWithin W (compile c) y y' (3 * T) ∧ Matches w b x' y' ∧
+      ∀ a, a < b ∨ b + 2 ^ w ≤ a → y'.mem a = y.mem a := by
+  obtain ⟨n, hn, he⟩ := he
+  obtain ⟨z, hz, hzm, hzf⟩ := exec he hc hx hxy hw hfit
+  exact ⟨z, hz.mono (by omega), hzm, hzf⟩
+
+/-- Normalize a static list of source registers, retaining the runtime base and modulus. -/
+@[expose] def normalizeBankList : List (Fin r) → Code .standard (r + 3)
+  | [] => .op (.copy Reg.address Reg.address)
+  | i :: is => .seq (.op (.bin .mod (i.castAdd 3) (i.castAdd 3) Reg.modulus))
+      (normalizeBankList is)
+
+/-- A fixed instruction sequence normalizing each source register once. The final self-copy
+also makes the zero-register case an ordinary nonempty native program. -/
+@[expose] def normalizeRegisters (r : ℕ) : Code .standard (r + 3) :=
+  normalizeBankList (List.finRange r)
+
+private theorem exec_normalizeBankList {w W : ℕ} (is : List (Fin r)) (x : Data (r + 3))
+    (hm : x.regs Reg.modulus = 2 ^ w) (hw : w ≤ W) :
+    ∃ y, ExecWithin W (normalizeBankList is) x y (is.length + 1) ∧ y.mem = x.mem ∧
+      y.regs Reg.base = x.regs Reg.base ∧ y.regs Reg.modulus = 2 ^ w ∧
+      (∀ j : Fin r, y.regs (j.castAdd 3) =
+        if j ∈ is then x.regs (j.castAdd 3) % 2 ^ w else x.regs (j.castAdd 3)) := by
+  induction is generalizing x with
+  | nil =>
+    refine ⟨x.set Reg.address (x.regs Reg.address), ExecWithin.copy, rfl, ?_, ?_, ?_⟩
+    · simp [Reg.base, Reg.address, Fin.mk.injEq]
+    · simpa [Reg.modulus, Reg.address, Function.update_apply, Fin.mk.injEq] using hm
+    · intro j
+      simp only [List.not_mem_nil, ↓reduceIte, Data.set_regs,
+        Function.update_of_ne (bank_ne_address j)]
+  | cons i is ih =>
+    let z := x.set (i.castAdd 3) (x.regs (i.castAdd 3) % 2 ^ w)
+    have hz : z.regs Reg.modulus = 2 ^ w := by
+      simpa only [z, Data.set_regs,
+        Function.update_of_ne (Ne.symm (bank_ne_modulus i))] using hm
+    have h1 : ExecWithin W
+        (.op (.bin .mod (i.castAdd 3) (i.castAdd 3) Reg.modulus)) x z 1 := by
+      simpa only [BinOp.eval, hm] using
+        (ExecWithin.bin (f := .mod) (d := i.castAdd 3) (i := i.castAdd 3)
+          (j := Reg.modulus) (x := x) (w := W)
+          (by simpa only [BinOp.eval, hm] using
+            (show Fits w (x.regs (i.castAdd 3) % 2 ^ w) from
+              Nat.mod_lt _ (Nat.two_pow_pos _)).mono hw))
+    obtain ⟨y, he, hmem, hbase, hmod, hregs⟩ := ih z hz
+    refine ⟨y, ?_, hmem, ?_, hmod, ?_⟩
+    · simpa only [normalizeBankList, List.length_cons, Nat.add_left_comm] using h1.seq he
+    · simpa only [z, Data.set_regs,
+        Function.update_of_ne (Ne.symm (bank_ne_base i))] using hbase
+    · intro j
+      rw [hregs]
+      by_cases hji : j = i
+      · subst j
+        simp [z]
+      · have hji' : j.castAdd 3 ≠ i.castAdd 3 := by
+          intro heq
+          exact hji (Fin.ext (congrArg (fun k : Fin (r + 3) => k.val) heq))
+        simp only [z, Data.set_regs, Function.update_of_ne hji', List.mem_cons,
+          hji, false_or]
+
+/-- Actual register normalization supplies a bounded source view without clearing any memory.
+The base, modulus and every caller memory cell are preserved. -/
+theorem exec_normalizeRegisters {w W b : ℕ} (x : Data (r + 3))
+    (hb : x.regs Reg.base = b) (hm : x.regs Reg.modulus = 2 ^ w) (hw : w ≤ W) :
+    ∃ y, ExecWithin W (normalizeRegisters r) x y (r + 1) ∧ y.mem = x.mem ∧
+      Matches w b (view w b y) y ∧ (view w b y).Bounded w ∧
+      ∀ j : Fin r, y.regs (j.castAdd 3) = x.regs (j.castAdd 3) % 2 ^ w := by
+  obtain ⟨y, he, hmem, hbase, hmod, hregs⟩ := exec_normalizeBankList (List.finRange r) x hm hw
+  have hr (j : Fin r) : y.regs (j.castAdd 3) = x.regs (j.castAdd 3) % 2 ^ w := by
+    simpa only [List.mem_finRange, ↓reduceIte] using hregs j
+  refine ⟨y, ?_, hmem, ⟨rfl, hbase.trans hb, hmod⟩, ?_, hr⟩
+  · simpa only [normalizeRegisters, List.length_finRange] using he
+  · exact view_bounded w b y (fun j => by rw [hr]; exact Nat.mod_lt _ (Nat.two_pow_pos _))
+
+end Cslib.WordRAM.MemoryWindow
diff --git a/ComplexityTests/SchonhageCallable.lean b/ComplexityTests/SchonhageCallable.lean
new file mode 100644
index 0000000000..42ee7fc41d
--- /dev/null
+++ b/ComplexityTests/SchonhageCallable.lean
@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+-- upstream: local-only (tests)
+
+import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Width
+
+-- VM checks exercise actual code alongside the separate kernel-checked general execution.
+-- Complete interpreter clients use m=0,N=1: (4^m)^18 ≤ N makes larger depths impractical.
+-- Positive-depth thin bounds are established by the general execution/resource theorems.
+set_option linter.hashCommand false
+
+namespace ComplexityTests.SchonhageCallable
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+private def observe {m N : ℕ} (caller : List ℕ)
+    (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ)
+    (qs : List (Fin N × Fin N)) (dirtyWorkspace : Bool := false) : Option (List ℤ × Bool) :=
+  let original := (State.init (CallableProduct.input caller X Y qs) : State 163).data
+  let b := CallableProduct.inputBase caller
+  let sentinel := b + CallableProduct.windowSize N qs.length + 7
+  let dirty : Data 163 := ⟨original.regs, fun a =>
+    if dirtyWorkspace && decide (b + QueriedProduct.inputEnd m N qs.length ≤ a ∧
+        a < b + CallableProduct.windowSize N qs.length)
+      then 2 * CallableProduct.windowSize N qs.length + 27 else original.mem a⟩
+  let initial := dirty.write sentinel 91
+  (CallableProduct.entryProgram.eval 512 1024 initial).map fun (y, _) =>
+    ((List.range qs.length).map (fun i => Signed.decode (y.mem (y.regs 0 + i))),
+      decide ((∀ a < b, y.mem a = original.mem a) ∧
+        (∀ a < QueriedProduct.inputEnd m N qs.length, y.mem (b + a) = original.mem (b + a)) ∧
+        y.mem sentinel = 91))
+
+-- Actual raw-one multiplication and duplicate requests at a dynamic nonzero base.
+#guard observe [17, 29] (m := 0) (N := 1) (fun _ _ => 1) (fun _ _ => 1)
+    [(0, 0), (0, 0), (0, 0)] == some ([1, 1, 1], true)
+
+-- Actual empty query and zero-product cases still restore the caller and local input.
+#guard observe [23] (m := 0) (N := 1) (fun _ _ => 1) (fun _ _ => 0) [] == some ([], true)
+#guard observe [] (m := 0) (N := 1) (fun _ _ => 1) (fun _ _ => 0) [(0, 0)] == some ([0], true)
+
+-- A preexisting caller workspace can contain physical words larger than the source modulus.
+-- This is a supplied dirty caller state; the callee performs no bulk fill or clearing.
+#guard observe [17, 29] (m := 0) (N := 1) (fun _ _ => 1) (fun _ _ => 1)
+    [(0, 0), (0, 0)] true == some ([1, 1], true)
+
+private def X : Matrix (Fin 1) (Fin (D 0)) ℤ := fun _ _ => 1
+private def Y : Matrix (Fin (D 0)) (Fin 1) ℤ := fun _ _ => 1
+private def requests : List (Fin 1 × Fin 1) := [(0, 0)]
+
+-- Kernel-checked complete initialized execution. The same y is reached by charged Runs,
+-- supplies the exact physical signed answer 2, preserves the caller, and reaches halt.
+example : ∃ y n,
+    Runs 512 (CallableProduct.entryProgram.program CallableProduct.Reg.result)
+      (State.init (CallableProduct.input [17, 29] X Y requests))
+      ⟨CallableProduct.entryProgram.size, y⟩ n ∧
+    Executes 512 (CallableProduct.entryProgram.program CallableProduct.Reg.result)
+      (State.init (CallableProduct.input [17, 29] X Y requests))
+      (4 + QueriedProduct.outputBase 0 0 1 1) (n + 1) ∧
+    y.mem (4 + QueriedProduct.outputBase 0 0 1 1) = 2 ∧ y.mem 2 = 17 ∧ y.mem 3 = 29 := by
+  obtain ⟨hi, y, n, hn, hr, he, hy, hv, hin, hf⟩ := CallableProduct.runs
+    (W := 512) [17, 29] X Y requests (by decide +kernel)
+    (by intro i k; constructor <;> norm_num [X])
+    (by intro k j; constructor <;> norm_num [Y])
+    (by
+      intro v hv
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hv
+      rcases hv with rfl | rfl <;> decide +kernel)
+    (by decide +kernel)
+  refine ⟨y, n, hr, he, ?_, ?_, ?_⟩
+  · have hone : (X * Y) 0 0 = 1 := by decide +kernel
+    have h := hv (0 : Fin 1)
+    change y.mem (4 + QueriedProduct.outputBase 0 0 1 1) = Signed.encode ((X * Y) 0 0) at h
+    rw [hone] at h
+    exact h
+  · simpa [CallableProduct.input, CallableProduct.inputBase, State.init, Data.init] using
+      hf 2 (Or.inl (by decide))
+  · simpa [CallableProduct.input, CallableProduct.inputBase, State.init, Data.init] using
+      hf 3 (Or.inl (by decide))
+
+-- The numerical reservation/admission budget has a strict width boundary for this input.
+example : Fits 387 (4 + 4 * CallableProduct.windowSize 1 1 + 1024) ∧
+    ¬Fits 386 (4 + 4 * CallableProduct.windowSize 1 1 + 1024) := by decide +kernel
+
+-- Empty query lists are admitted at positive geometry; zero N fails the explicit thin premise.
+example : ¬D 0 ^ 18 ≤ 0 := by decide +kernel
+
+end ComplexityTests.SchonhageCallable
diff --git a/ComplexityTests/WordRAMMemoryWindow.lean b/ComplexityTests/WordRAMMemoryWindow.lean
new file mode 100644
index 0000000000..ae21ca8306
--- /dev/null
+++ b/ComplexityTests/WordRAMMemoryWindow.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+-- upstream: local-only (tests)
+
+import Complexity.Computability.WordRAM.MemoryWindow
+import Complexity.Computability.WordRAM.ArrayNormalize
+import Mathlib.Tactic.FinCases
+
+/-! # Dirty-memory, dynamic-base and frame clients for actual memory-window code -/
+
+open Cslib.WordRAM
+
+private def dirty : Data 6 :=
+  ⟨![2, 0, 1, 17, 8, 0], fun a => if a = 19 then 27 else if a = 16 then 99
+    else if a = 25 then 77 else 0⟩
+
+private def sourceCode : Code .standard 3 :=
+  .seq (.op (.load 1 0)) <| .seq (.op (.bin .add 1 1 2)) (.op (.store 0 1))
+
+-- The real masked load reads 27 % 8 = 3, then actual arithmetic/store writes 4.
+-- Omitting the remainder would write 28. Both adjacent caller sentinels survive.
+example : ∃ y, ExecWithin 8 (MemoryWindow.compile sourceCode) dirty y 6 ∧
+    y.mem 19 = 4 ∧ y.mem 16 = 99 ∧ y.mem 25 = 77 ∧ y.regs 3 = 17 ∧ y.regs 4 = 8 := by
+  refine ⟨?y, ?run, ?value, ?left, ?right, ?base, ?modulus⟩
+  case run =>
+    apply ExecWithin.of_eval (fuel := 0) (n := 6)
+    · rfl
+    · decide
+  all_goals decide +kernel
+
+example : Fits 5 (17 + 2 ^ 3) ∧ ¬Fits 4 (17 + 2 ^ 3) := by decide +kernel
+
+-- The source view is bounded despite dirty physical memory and caller words above 2^3.
+example : (MemoryWindow.view 3 17 dirty : Data 3).Bounded 3 := by
+  apply MemoryWindow.view_bounded
+  intro i
+  fin_cases i <;> decide +kernel
+
+-- Only the requested span is normalized, including the final cell.
+example : ∃ y, ExecWithin 8 ArrayNormalize.program
+    ⟨![10, 2, 8, 99, 99, 99, 99], fun a => if a = 10 then 27 else 19⟩ y 18 ∧
+      y.mem 9 = 19 ∧ y.mem 10 = 3 ∧ y.mem 11 = 3 ∧ y.mem 12 = 19 := by
+  refine ⟨?y, ?run, ?values⟩
+  case run => ram_eval 2 [ArrayNormalize.program, ArrayNormalize.body, ArrayNormalize.base,
+    ArrayNormalize.length, ArrayNormalize.modulus, ArrayNormalize.index, ArrayNormalize.address,
+    ArrayNormalize.value, ArrayNormalize.one, Fits, Fin.mk.injEq]
+  case values => decide +kernel
diff --git a/ROADMAP.md b/ROADMAP.md
index 08bf383697..d80448735e 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -518,6 +518,17 @@ each statement against the numbered result. Organize modules by subject, not cha
   almost-surely terminating structured loops; random-tape equivalence and BPP/RP/ZPP simulation
   bridges for the randomized word RAM ([#1124]); transfer of cell-probe lower bounds; and the
   Horn-SAT, 2SAT, matching and domino-tiling clients.
+- **Caller-safe queried thin products** ([#1618](https://github.com/cslib-community/complexitylib/issues/1618)):
+  actual memory operations are rebased above a runtime caller base, using a computed source
+  modulus and charged load normalization. The initialized 163-register program restores local
+  input, returns an absolute answer pointer and preserves the caller outside a polynomial window.
+  Setup/return adds at most `2048*(N*D+Q+1)` to three times the original product charge. At
+  `D=4^m`, `L=19m`, `D^18≤N` and `Q*2^m≤N²`, the full charge including halt is at most
+  `17301504*(19m+1)*N²/D^(1/18)`. Distinct-set sparsity retains an additive occurrence charge.
+  Every width at least `256*clog₂(base+N+Q+P+5)` suffices for initialized caller-word bound `P`.
+  The reserved window is at most `(2*(N+Q+3))^128` and is not bulk-initialized. Actual ET-record
+  reads, matrix/query placement, producer-readback composition and the full [#1394] endpoint
+  remain open.
 - **Conditional Convolution-3SUM host** ([#1524]): the charged native host initializes from the
   ordinary input and runs every generated instance, conditional on a concrete solver's execution,
   correctness and frame theorem. This completes the conditional host milestone. Integrating the
diff --git a/UPSTREAM.md b/UPSTREAM.md
index e12ceded21..e55fed516e 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -362,6 +362,29 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   proofs, not a transfer of the source Light semantics or instruction constants. Exact Triangle
   parameter/instance preparation and outer solving, full ordinary-3SUM composition, and the
   improved Section 4 route to exponent 1.9992 remain separate work under #1394.
+  Caller-safe queried products ([#1618](https://github.com/cslib-community/complexitylib/issues/1618))
+  rebase actual memory accesses above a runtime caller base. The generic `WordRAM.MemoryWindow`
+  compiler charges an addition/load/remainder for each load and an addition/store for each
+  store, reusing ordinary native `Exec` and `Code`. Its clipped-memory view permits dirty
+  workspace without bulk initialization; it is a value relation, not independent run semantics.
+  The original product program is unchanged. Existing `NatClog` (the exact module already
+  landed in #1469) and `WordRAM.Power` compute the source modulus from original counts; fixed
+  register normalization and two `WordRAM.ArrayNormalize` span loops are actual charged code.
+  The callable raw-zero/one thin-regime client uses 163 registers and at most 131072 flat
+  instructions. It restores local input, returns exact product words at an absolute pointer,
+  preserves the caller outside its window, and retains the original charged raw-to-signed
+  doubling. At `D=4^m`, `L=19m`, `D^18≤N`, its standalone charge including halt is at most
+  three times the original product charge plus `2048*(N*D+Q+1)`. Distinct-set sparsity retains
+  the additive occurrence charge; `Q*2^m≤N²` gives `17301504*(19m+1)*N²/D^(1/18)`.
+  The window is at most `(2*(N+Q+3))^128`; this deliberately large polynomial address-space
+  reservation is not a claim about a tightly packed physical allocation. Every width at least
+  `256*clog₂(base+N+Q+P+5)` suffices for initialized callers with prefix words bounded by `P`.
+  The arbitrary dirty-caller interface uses `P` to bound every initial register and memory
+  word, including words loaded before the actual remainder; native prefix bounds then follow
+  from that derived physical admission. Initialized scratch is zero, so its `P` only needs
+  to bound the protected caller prefix. The generic compiler theorem remains separate from
+  the concrete thin-geometry admission and saving.
+  The real ET-record/matrix/query adapter and whole solver remain subsequent work under #1394.
   Stage `exec_*` lemmas are internal implementation APIs exported across proof modules;
   callers use the flat initialized runs, width theorem or pointer/epoch kernel. The narrow
   `WordRAM.ArrayAppend` and `WordRAM.InputArray` topic modules keep append/input dependencies