feat(WordRAM): compile memory windows for callable thin products

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

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.
+-/

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

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