theorem Hex.Matrix.toMatrix_pad_view {R : Type u} {n m : Nat} [OfNat R 0] (A : Submatrix R n m) (n' m' : Nat) (hn : n ≤ n') (hm : m ≤ m') : (A.pad n' m' hn hm).toMatrix = A.toMatrix.pad n' m'

Materializing a widened view is Matrix.pad of the materialized source.

theorem Hex.Matrix.toMatrix_toBlocks₁₁ {R : Type u} [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : A.toBlocks₁₁.toMatrix = A.toMatrix.toBlocks₁₁

Materializing the top-left quadrant view is Matrix.toBlocks₁₁ of the materialized parent.

theorem Hex.Matrix.toMatrix_toBlocks₁₂ {R : Type u} [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : A.toBlocks₁₂.toMatrix = A.toMatrix.toBlocks₁₂

Materializing the top-right quadrant view is Matrix.toBlocks₁₂ of the parent.

theorem Hex.Matrix.toMatrix_toBlocks₂₁ {R : Type u} [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : A.toBlocks₂₁.toMatrix = A.toMatrix.toBlocks₂₁

Materializing the bottom-left quadrant view is Matrix.toBlocks₂₁ of the parent.

theorem Hex.Matrix.toMatrix_toBlocks₂₂ {R : Type u} [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : A.toBlocks₂₂.toMatrix = A.toMatrix.toBlocks₂₂

Materializing the bottom-right quadrant view is Matrix.toBlocks₂₂ of the parent.

structure Hex.Matrix.StrassenConfig (R : Type u) : Type u

Configuration for mulStrassen: the recursion cutoff below which a block is handed to the base kernel, and the pluggable baseMul base kernel itself. Data only — baseMul is a bare function and the record carries no algebraic instances, so a caller can supply a hand-tuned small-matrix kernel without touching the recursion.

• cutoff : Nat

  The recursion stops splitting and calls baseMul once any of the three dimensions is below this cutoff.

• baseMul {n m k : Nat} : Matrix R n m → Matrix R m k → Matrix R n k

  The base kernel run on small blocks. Polymorphic over the dimensions because the recursion reaches its base case at a range of (possibly rectangular) shapes.

def Hex.Matrix.StrassenConfig.Valid {R : Type u} [Mul R] [Add R] [OfNat R 0] (cfg : StrassenConfig R) : Prop

A configuration is valid when its base kernel agrees with the reference mul on every input. The correctness theorem mulStrassen_eq_mul is stated under this hypothesis, keeping the proof out of the StrassenConfig data record.

Equations

• cfg.Valid = ∀ {n m k : Nat} (X : Hex.Matrix R n m) (Y : Hex.Matrix R m k), cfg.baseMul X Y = X.mul Y

def Hex.Matrix.strassenDefault {R : Type u} [Mul R] [Add R] [OfNat R 0] : StrassenConfig R

The default configuration: naive mulImpl as the base kernel and a measured cutoff of 96.

Measured by the Strassen bench driver (bench/HexMatrix/Bench.lean) on Int coefficients with GMP arithmetic, sweeping the cutoff τ against dimension n on host chungus2 (AMD EPYC 9455), Lean toolchain 4.32.0-rc1. An extra Strassen level below a 64×64 block loses to the naive base kernel, while a 128×128 block splits profitably. Any cutoff in (64, 128] therefore recurses down to a 64×64 naive leaf; that leaf class wins from the first splitting dimension (n = 128) and stays within ~4% of the 128×128-leaf class at n = 512 (which edges ahead there), so 96 is shipped as its representative, extending Strassen to non-power-of-two blocks in [96, 128) as well. The value has been re-measured twice: on the flat row-major backing with materialized quadrants and again on the Submatrix-view recursion, both within noise of the original sweep (the quadrant copies the views remove are O(n²) per level against the O(n^2.81) multiply work, so they never dominated at benched sizes) — the crossover stayed put and 96 stands.

Equations

• Hex.Matrix.strassenDefault = { cutoff := 96, baseMul := fun {n m k : Nat} => Hex.Matrix.mulImpl }

theorem Hex.Matrix.strassenDefault_valid {R : Type u} [Mul R] [Add R] [OfNat R 0] : strassenDefault.Valid

The default configuration is valid: its base kernel mulImpl equals mul by mul_eq_mulImpl.

@[irreducible]

def Hex.Matrix.mulStrassenView {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] (cfg : StrassenConfig R) {n m k : Nat} (A : Submatrix R n m) (B : Submatrix R m k) : Matrix R n k

The internal Strassen-Winograd recursion over copy-free Submatrix views. Recurses on the runtime dimensions following the Winograd schedule.

Base case: when any of n, m, k is ≤ 1 or below cfg.cutoff, materialize the current view blocks (toMatrix) and call cfg.baseMul — the only leaf allocation. The ≤ 1 disjuncts are config-independent, so cutoff = 0 cannot defeat termination.

Recursive step: widen each operand view to even dimensions (h + h, w + w, d + d with h := (n+1)/2 etc.) — a zero-fill reshape with no copy — split into 2×2 quadrant views (offset arithmetic — small view records, no buffer copies), materialize only the fifteen Sᵢ/Tᵢ/Uᵢ operand sums and the seven recursive products, assemble with fromBlocks, and crop back to n × k. Termination is well-founded on n + m + k: the recursion fires only when n, m, k ≥ 2, and each halved dimension is then strictly smaller.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Matrix.castDims {R : Type u} {n m n' m' : Nat} (hn : n = n') (hm : m = m') (A : Matrix R n m) : Matrix R n' m'

Transport both matrix dimensions along equalities.

Equations

• Hex.Matrix.castDims hn hm A = hn ▸ hm ▸ A

@[irreducible]

def Hex.Matrix.mulStrassenInto {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] (cfg : StrassenConfig R) {n N M : Nat} (A B : Submatrix R n n) (C : Matrix R N M) (D : Region N M n n) : Matrix R N M

Write a square Strassen result into a backing-free region of one owned output matrix. Even recursive nodes use the Boyer–Dumas–Pernet–Zhou schedule: X and Y are the only half-size matrix buffers, while products and Uᵢ values are written directly into the four output quadrants. Base and odd nodes retain the reference view recursion as a shape-safe fallback.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Matrix.mulStrassenInto_spec {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] (cfg : StrassenConfig R) {n N M : Nat} (A B : Submatrix R n n) (C : Matrix R N M) (D : Region N M n n) : D.toMatrix (mulStrassenInto cfg A B C D) = mulStrassenView cfg A B ∧ ∀ {rows cols : Nat} (E : Region N M rows cols), D.Disjoint E → E.toMatrix (mulStrassenInto cfg A B C D) = E.toMatrix C

The region writer returns the reference result in its destination and preserves every disjoint region.

def Hex.Matrix.mulStrassen {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] (cfg : StrassenConfig R) {n m k : Nat} (M : Matrix R n m) (N : Matrix R m k) : Matrix R n k

Strassen-Winograd multiplication. The public entry point wraps the operands as full-matrix Submatrix views and runs the view recursion mulStrassenView; the quadrant splitting inside never materializes or copies a quadrant buffer — only O(1) view records.

Equations

• Hex.Matrix.mulStrassen cfg M N = Hex.Matrix.mulStrassenView cfg (Hex.Submatrix.ofMatrix M) (Hex.Submatrix.ofMatrix N)

def Hex.Matrix.mulStrassenImpl {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] (cfg : StrassenConfig R) {n m k : Nat} (A : Matrix R n m) (B : Matrix R m k) : Matrix R n k

Storage-scheduled implementation of mulStrassen. Square inputs run the two-buffer writer; all other shapes retain the reference view recursion.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem Hex.Matrix.mulStrassen_eq_impl : @mulStrassen = @mulStrassenImpl

The storage-scheduled implementation is extensionally equal to the reference entry point. This transfers the implementation without changing mulStrassen's statement or its ring-level correctness theorem.

theorem Hex.Matrix.mulStrassenView_eq_mul {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] (cfg : StrassenConfig R) (hcfg : cfg.Valid) (A : Submatrix R n m) (B : Submatrix R m k) : mulStrassenView cfg A B = A.toMatrix.mul B.toMatrix

The view recursion computes the same matrix as the reference mul of the materialized operands, for every valid configuration. Proved by functional induction over mulStrassenView, reducing each quadrant view to its toBlocks materialization (toMatrix_toBlocks…, toMatrix_pad_view) and composing the three wave-1 lemmas exactly as the Matrix-level recursion did.

theorem Hex.Matrix.mulStrassen_eq_mul {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] (cfg : StrassenConfig R) (hcfg : cfg.Valid) (M : Matrix R n m) (N : Matrix R m k) : mulStrassen cfg M N = M.mul N

Correctness of Strassen-Winograd multiplication. For every valid configuration, mulStrassen computes the same matrix as the reference mul.