feat(Schonhage): compute native shared box tables

Complexity.lean

@@ -325,6 +325,30 @@ 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.BoxTable
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Bounds
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueLoop
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueState
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueWrite
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Children
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Constructor
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.DigitScan
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Digits
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Flat
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Geometry
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Index
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Initialize
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Input
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.InputLayout
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Lookup
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupDigits
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupLoop
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupStep
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Program
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Tile
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileChildren
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileKernels
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Values
 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
@@ -3489,6 +3513,7 @@ public import Complexity.Foundations.Data.Finset.Finpartition
 public import Complexity.Foundations.Data.Finset.KthLargest
 public import Complexity.Foundations.Data.Finset.KthLargest.Truncation
 public import Complexity.Foundations.Data.Finset.Lowest
+public import Complexity.Foundations.Data.Finset.LowestMax
 public import Complexity.Foundations.Data.Finset.Markov
 public import Complexity.Foundations.Data.Finset.OrderGlue
 public import Complexity.Foundations.Data.Finset.OrderedFilter
@@ -3582,6 +3607,7 @@ public import Complexity.Foundations.Data.Nat.Prime
 public import Complexity.Foundations.Data.Nat.Primrec
 public import Complexity.Foundations.Data.Nat.Radix
 public import Complexity.Foundations.Data.Nat.Radix.Measurement
+public import Complexity.Foundations.Data.Nat.RadixUpdate
 public import Complexity.Foundations.Data.Nat.RecursionTree
 public import Complexity.Foundations.Data.Nat.ResidueSum
 public import Complexity.Foundations.Data.Nat.SqrtLog

Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable.lean

@@ -0,0 +1,46 @@
+/-
+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.BoxTable.Constructor
+public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Flat
+
+/-!
+# Native shared geometry and compact signed box tables
+
+The existing finite boxes are now computed as a shared native directory and compact
+catalogue. Each tile fills one value per actual box from the two canonical signed
+leaf arrays, and lookup reads the actual stored signed word for a valid raw cube.
+The caller routines permit dirty scratch and preserve the original arrays and outside memory.
+
+## Main definitions
+
+* `BoxTable.geometry`: compute the shared directory and descriptor catalogue once.
+* `BoxTable.tile`: reuse that geometry to fill one compact value table.
+* `BoxTable.lookup`: read a valid raw cube's actual stored value.
+* `BoxTable.program`: complete initialized-input constructor with a fixed 64-register bank.
+
+## Main results
+
+* `BoxTable.runs_wide`: original-input admission, actual initialized prefix and charged halt,
+  with the same final witness for the computed ranks, values and frame.
+* `BoxTable.exec_lookup`: actual valid-box lookup, within `18*L+32` native instructions.
+* `BoxTable.geometryTime_le`: shared geometry within `64*(L+1)^2*10^L` when `m ≤ L`.
+* `BoxTable.tileTime_le`: per-tile work bounded using the existing finite box-count law.
+
+## References
+
+The finite boxes and recurrence are adapted from [AlmanWilliams2026, Section 4.2].
+The shared directory and compact native representation are original alternatives to the
+per-tile trie in the primary formal source at
+[anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30).
+Both use the existing tensor terms and signed leaf-product sum, but the memory layout,
+digit order and charged costs differ. Shared setup and retained tile storage remain explicit;
+no global all-tile amortization, wanted-query program, Corollary 26 or tuned 1.9992 bound
+is claimed.
+-/

Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Bounds.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.BoxTable.InputLayout
+import Mathlib.Data.Nat.Log
+
+/-!
+# Original-input bounds for native compact box tables
+
+The actual shared geometry and one tile have separate charged terms. A positive
+logarithmic width threshold follows from the original depth, scalar headers, and
+leaf magnitude envelopes. Neither the program nor its input reads a width certificate.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable
+
+open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Shared scalar/directory/descriptor setup; this cost is paid once across tiles. -/
+@[expose] def geometryTime (L m t : ℕ) : ℕ :=
+  4 * L + 20 + (11 * L + 28) * ((m - t + 1) * 10 ^ L)
+
+/-- One compact value-table construction, with dirty-memory-safe scalar setup. -/
+@[expose] def tileTime (L m t : ℕ) : ℕ := 328 * (boxes L m t).card + 8
+
+/-- Original input adaptation, shared setup, one tile, and the final halt are charged. -/
+@[expose] def timeBound (L m t : ℕ) : ℕ := 4 * L + 19 + geometryTime L m t + tileTime L m t + 1
+
+/-- The physical width threshold uses only original scalar and magnitude parameters. -/
+@[expose] def admissionWidth (L m t A B : ℕ) : ℕ :=
+  Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) + 3
+
+/-- Width admission remains positive at zero depth and zero operands. -/
+theorem admissionWidth_pos (L m t A B : ℕ) : 0 < admissionWidth L m t A B := by
+  unfold admissionWidth
+  omega
+
+/-- The same original-input threshold derives unsigned addresses and signed operand bounds. -/
+theorem admission_bounds {W L m t A B : ℕ} (hW : admissionWidth L m t A B ≤ W) :
+    0 < W - 2 ∧ Fits W (addressBound L m t) ∧
+      GenericRAM.Signed.Fits (W - 2) (magnitudeBound L A B : ℕ) := by
+  have hlog := Nat.le_pow_clog (by decide : 1 < (2 : ℕ))
+    (magnitudeBound L A B + addressBound L m t + 1)
+  have hs : Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) ≤ (W - 2) - 1 := by
+    unfold admissionWidth at hW
+    omega
+  have hp := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hs
+  have hmag : magnitudeBound L A B < 2 ^ ((W - 2) - 1) := by omega
+  have hw : 0 < W - 2 := by unfold admissionWidth at hW; omega
+  refine ⟨hw, ?_, hw, ?_, ?_⟩
+  · change addressBound L m t < 2 ^ W
+    have hp' := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) (by omega :
+      Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) ≤ W)
+    omega
+  · have hnonneg : 0 ≤ (magnitudeBound L A B : ℤ) := Int.natCast_nonneg _
+    have hpow : 0 ≤ (2 : ℤ) ^ ((W - 2) - 1) := by positivity
+    omega
+  · exact_mod_cast hmag
+
+/-- The existing finite cardinality law controls the per-tile memoization cost. -/
+theorem tileTime_le (L m t : ℕ) (hm : m ≤ L) (ht : t ≤ m) :
+    tileTime L m t ≤ 328 * (m + 1) * ∑ d ∈ Finset.Icc t m, beta L m d + 8 := by
+  have hb := card_boxes_le L m t hm ht
+  unfold tileTime
+  nlinarith only [hb]
+
+/-- Under the usual depth bound, shared geometry is polynomial-depth times the existing
+encoding-array length. This setup is independent of the number of tiles. -/
+theorem geometryTime_le (L m t : ℕ) (hm : m ≤ L) :
+    geometryTime L m t ≤ 64 * (L + 1) ^ 2 * 10 ^ L := by
+  have hp : 1 ≤ 10 ^ L := Nat.one_le_pow L _ (by decide)
+  have hh : m - t + 1 ≤ L + 1 := by omega
+  have hs := Nat.mul_le_mul_right (10 ^ L) hh
+  have hc := Nat.mul_le_mul_left (11 * L + 28) hs
+  have hsmall : 4 * L + 20 ≤ (4 * L + 20) * 10 ^ L := by
+    simpa only [Nat.mul_one] using Nat.mul_le_mul_left (4 * L + 20) hp
+  calc
+    geometryTime L m t ≤ (4 * L + 20) * 10 ^ L +
+        (11 * L + 28) * ((L + 1) * 10 ^ L) := Nat.add_le_add hsmall hc
+    _ = (4 * L + 20 + (11 * L + 28) * (L + 1)) * 10 ^ L := by ring
+    _ ≤ 64 * (L + 1) ^ 2 * 10 ^ L := Nat.mul_le_mul_right _ (by nlinarith)
+
+/-- The directory and descriptors are shared; a retained tile adds exactly one word per box. -/
+theorem allocation_le (L m t : ℕ) :
+    memoryEnd L m t - directoryBase L ≤ 5 * ((m - t + 1) * 10 ^ L) := by
+  have hk := Nat.count_le (Eligible L (m - t)) (n := (m - t + 1) * 10 ^ L)
+  rw [count_eligible_eq_card_boxes] at hk
+  unfold memoryEnd valueBase recordBase
+  omega
+
+/-- A fixed constructor bank and constant flat code bound, including its final halt. -/
+theorem program_size_le : program.size + 1 ≤ 1024 := by decide
+
+/-- Lookup uses the same fixed bank and bounded code, independently of the depth. -/
+theorem lookup_size_le : lookup.size + 1 ≤ 256 := by decide
+
+/-- Construction never inspects the physical width. -/
+theorem not_readsWidth : ¬program.ReadsWidth := by decide
+
+/-- Lookup never inspects the physical width. -/
+theorem lookup_not_readsWidth : ¬lookup.ReadsWidth := by decide
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable

Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueLoop.lean

@@ -0,0 +1,153 @@
+/-
+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.BoxTable.CatalogueWrite
+
+/-!
+# Complete native shared-catalogue scan
+
+The actual outer loop visits every directory slot once. Its digit scans and all
+directory/record stores are charged; the compact count is Mathlib's count of the
+computed eligibility predicate. Dirty memory outside the written prefixes survives.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable
+
+open Cslib.WordRAM
+
+/-- Persistent scalar contents used by the native catalogue loop, with no run or cost fields. -/
+structure CatalogueParameters (L H D R : ℕ) (x : Data registers) : Prop where
+  /-- Original depth. -/
+  levels : x.regs Reg.levels = L
+  /-- Computed P0/star limit. -/
+  height : x.regs Reg.height = H
+  /-- Computed decimal capacity. -/
+  span : x.regs Reg.span = 10 ^ L
+  /-- Caller directory base. -/
+  directory : x.regs Reg.directory = D
+  /-- Computed compact-record base. -/
+  records : x.regs Reg.records = R
+  /-- Computed complete slot count. -/
+  slots : x.regs Reg.slots = (H + 1) * 10 ^ L
+  /-- Scalar one. -/
+  one : x.regs Reg.one = 1
+  /-- Scalar radix. -/
+  ten : x.regs Reg.ten = 10
+  /-- Scalar P0 digit. -/
+  nine : x.regs Reg.nine = 9
+  /-- Scalar record width. -/
+  three : x.regs Reg.three = 3
+  /-- Scalar zero outside signed arithmetic. -/
+  nil : x.regs Reg.nil = 0
+
+private def parameterRegisters : Finset (Fin registers) :=
+  {Reg.levels, Reg.height, Reg.span, Reg.directory, Reg.records, Reg.slots,
+    Reg.one, Reg.ten, Reg.nine, Reg.three, Reg.nil}
+
+private theorem CatalogueParameters.of_eq {L H D R : ℕ} {x y : Data registers}
+    (hx : CatalogueParameters L H D R x)
+    (h : ∀ i ∈ parameterRegisters, y.regs i = x.regs i) :
+    CatalogueParameters L H D R y :=
+  ⟨(h _ (by decide)).trans hx.levels, (h _ (by decide)).trans hx.height,
+    (h _ (by decide)).trans hx.span, (h _ (by decide)).trans hx.directory,
+    (h _ (by decide)).trans hx.records, (h _ (by decide)).trans hx.slots,
+    (h _ (by decide)).trans hx.one, (h _ (by decide)).trans hx.ten,
+    (h _ (by decide)).trans hx.nine, (h _ (by decide)).trans hx.three,
+    (h _ (by decide)).trans hx.nil⟩
+
+/-- Scalar registers changed by a complete catalogue iteration. -/
+@[expose] def CatalogueLocal (i : Fin registers) : Prop := InspectLocal i ∨ WriteLocal i
+
+instance (i : Fin registers) : Decidable (CatalogueLocal i) :=
+  inferInstanceAs (Decidable (InspectLocal i ∨ WriteLocal i))
+
+private theorem catalogueStep_preserves (i : Fin registers) :
+    ¬CatalogueLocal i → catalogueStep.Preserves i := by decide +revert
+
+private theorem parameter_not_local :
+    ∀ i ∈ parameterRegisters, ¬CatalogueLocal i := by decide
+
+/-- Compose the complete native digit scan with the real compact stores. -/
+theorem exec_catalogueStep {w L H D R s : ℕ} (x : Data registers)
+    (hx : CatalogueParameters L H D R x) (hs : x.regs Reg.slot = s)
+    (hc : x.regs Reg.count = Nat.count (Eligible L H) s)
+    (hslt : s < (H + 1) * 10 ^ L)
+    (hfit : Fits w (D + R + 6 * ((H + 1) * 10 ^ L) + 10 ^ L + L + 12)) :
+    ∃ y, ExecWithin w catalogueStep x y (11 * L + 26) ∧
+      y.mem = catalogueWrite L H D R s x.mem ∧ y.regs Reg.slot = s + 1 ∧
+      y.regs Reg.count = Nat.count (Eligible L H) (s + 1) ∧
+      CatalogueParameters L H D R y ∧
+      (∀ i, ¬CatalogueLocal i → y.regs i = x.regs i) := by
+  have hscan : Fits w (s + 10 ^ L + L + 12) := hfit.of_le (by omega)
+  have hwrite : Fits w (D + R + 6 * (s + 1) + 12) := hfit.of_le
+    (Nat.add_le_add_right ((Nat.add_le_add_left
+      (Nat.mul_le_mul_left 6 (Nat.succ_le_of_lt hslt)) (D + R)).trans
+        ((Nat.le_add_right _ (10 ^ L)).trans (Nat.le_add_right _ L))) 12)
+  obtain ⟨u, hu, he, hcode, hpop, hstride, hmem, hframe⟩ :=
+    exec_inspect x hx.levels hx.span hs hx.one hx.ten hx.nine hscan
+  have hf (i : Fin registers) (hi : ¬InspectLocal i) : u.regs i = x.regs i := hframe i hi
+  obtain ⟨y, hy, hym, hys, hyc, _⟩ := exec_writeSlot u
+    ((hf _ (by decide)).trans hx.directory) ((hf _ (by decide)).trans hx.records)
+    ((hf _ (by decide)).trans hs) ((hf _ (by decide)).trans hx.height)
+    ((hf _ (by decide)).trans hc) hcode he hpop hstride
+    ((hf _ (by decide)).trans hx.one) ((hf _ (by decide)).trans hx.three)
+    ((hf _ (by decide)).trans hx.nil) hwrite
+  have hwhole : ExecWithin w catalogueStep x y (11 * L + 26) :=
+    (hu.seq hy).mono (by omega)
+  have hregs (i : Fin registers) (hi : ¬CatalogueLocal i) : y.regs i = x.regs i :=
+    hwhole.regs_eq (catalogueStep_preserves i hi)
+  refine ⟨y, hwhole, ?_, hys, hyc, hx.of_eq (fun i hi =>
+    hregs i (parameter_not_local i hi)), hregs⟩
+  simpa only [hmem] using hym
+
+/-- The actual scan fills every directory word and emits every eligible compact record once. -/
+theorem exec_catalogueLoop {w L H D R : ℕ} (x : Data registers)
+    (hx : CatalogueParameters L H D R x)
+    (hslot : x.regs Reg.slot = 0) (hcount : x.regs Reg.count = 0)
+    (hsep : D + (H + 1) * 10 ^ L ≤ R)
+    (hfit : Fits w (D + R + 6 * ((H + 1) * 10 ^ L) + 10 ^ L + L + 12)) :
+    ∃ y, ExecWithin w (.loop (.lt Reg.slot Reg.slots) catalogueStep) x y
+        ((11 * L + 28) * ((H + 1) * 10 ^ L) + 2) ∧
+      CatalogueParameters L H D R y ∧ y.regs Reg.slot = (H + 1) * 10 ^ L ∧
+      y.regs Reg.count = Nat.count (Eligible L H) ((H + 1) * 10 ^ L) ∧
+      CataloguePrefix L H D R ((H + 1) * 10 ^ L) x.mem y.mem := by
+  let S := (H + 1) * 10 ^ L
+  let I (y : Data registers) : Prop :=
+    CatalogueParameters L H D R y ∧ y.regs Reg.slot ≤ S ∧
+      y.regs Reg.count = Nat.count (Eligible L H) (y.regs Reg.slot) ∧
+      CataloguePrefix L H D R (y.regs Reg.slot) x.mem y.mem
+  have hi : I x := by
+    refine ⟨hx, by simp [hslot, S], by simp [hslot, hcount], ?_⟩
+    simpa only [hslot] using CataloguePrefix.zero L H D R x.mem
+  have hb (y : Data registers) (hy : I y) (hg : (Cond.lt Reg.slot Reg.slots).Holds y) :
+      ∃ z, ExecWithin w catalogueStep y z (11 * L + 26) ∧ I z ∧
+        S - z.regs Reg.slot < S - y.regs Reg.slot := by
+    obtain ⟨hp, hle, hc, hprefix⟩ := hy
+    have hlt : y.regs Reg.slot < S := by
+      simpa only [Cond.holds_lt, hp.slots, S] using hg
+    obtain ⟨z, hz, hzm, hzs, hzc, hzp, _⟩ :=
+      exec_catalogueStep y hp rfl hc hlt hfit
+    refine ⟨z, hz, ⟨hzp, by omega, ?_, ?_⟩, by omega⟩
+    · simpa only [hzs] using hzc
+    · rw [hzs, hzm]
+      exact hprefix.step hlt hsep
+  obtain ⟨y, hy, hIy, hstop⟩ := ExecWithin.loop_invariant I
+    (fun y => S - y.regs Reg.slot) hb hi
+  obtain ⟨hp, hle, hc, hprefix⟩ := hIy
+  have hdone : y.regs Reg.slot = S := by
+    simp only [Cond.holds_lt, hp.slots, not_lt] at hstop
+    exact Nat.le_antisymm hle hstop
+  refine ⟨y, ?_, hp, hdone, ?_, ?_⟩
+  · simpa only [hslot, Nat.sub_zero, S, Nat.mul_comm, Nat.add_assoc] using hy
+  · simpa only [hdone] using hc
+  · simpa only [hdone] using hprefix
+
+end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable