Recursive (fuel-driven) Strassen block multiplication

Strassen.lean proves the one-level 2×2 Strassen identity over a commutative ring. This file lifts it to a recursive Strassen multiply on block matrices: a matrix on a doubled index type B ⊕ B is split into four B-indexed blocks, the seven Strassen products are computed by recursive sub-multiplications (one fuel level down), and the four result blocks are recombined via Matrix.fromBlocks.

Design

• Block index family. dim fuel m₀ doubles the base index type m₀ once per fuel level: dim 0 m₀ = m₀, dim (k+1) m₀ = dim k m₀ ⊕ dim k m₀. This sidesteps the dependent Fin (2*n) reindexing (finSumFinEquiv / reindex) that fights the recursion — the recursion is on the type-level doubling directly, exactly the shape Matrix.fromBlocks consumes.
• Recursion. strassenRec fuel multiplies two dim fuel m₀-indexed matrices. At fuel 0 it is the ordinary product *; at fuel k+1 it splits both operands into four blocks (toBlocks₁₁ …), forms the seven Strassen block products with seven recursive strassenRec k calls, and recombines.
• Correctness. strassenRec_eq : strassenRec fuel A B = A * B, by induction on fuel. The step rewrites the seven recursive products to * (IH), folds the blocks back with Matrix.fromBlocks_toBlocks, and discharges the algebraic Strassen identity with Matrix.fromBlocks_multiply + noncomm_ring (the blocks form a non-commutative matrix ring, and the Strassen recombination is order-preserving, so it holds over that ring).

Scope

The recursion performs actual sub-multiplications at every fuel level. The complexity accounting (that fuel k uses 7^k base multiplications, the O(n^log₂7) bound) and the Fin (2*n) data layout are outside the scope of this file.

API

• dim — the fuel-indexed doubled block index type.
• strassenRec — fuel-recursive Strassen multiply.
• strassen_blocks_eq — the non-commutative block Strassen recombination identity (the algebraic heart).
• strassenRec_eq — strassenRec fuel A B = A * B.

def Transfer.Examples.CoqEAL.StrassenRec.dim (m₀ : Type u_2) : ℕ → Type u_2

The fuel-indexed doubled block index type: doubles the base index m₀ once per fuel level.

Equations

• Transfer.Examples.CoqEAL.StrassenRec.dim m₀ 0 = m₀
• Transfer.Examples.CoqEAL.StrassenRec.dim m₀ k.succ = (Transfer.Examples.CoqEAL.StrassenRec.dim m₀ k ⊕ Transfer.Examples.CoqEAL.StrassenRec.dim m₀ k)

@[instance_reducible]

instance Transfer.Examples.CoqEAL.StrassenRec.dimFintype (m₀ : Type u_2) [Fintype m₀] (fuel : ℕ) : Fintype (dim m₀ fuel)

Equations

• Transfer.Examples.CoqEAL.StrassenRec.dimFintype m₀ 0 = Transfer.Examples.CoqEAL.StrassenRec.dimFintype._aux_1 m₀
• Transfer.Examples.CoqEAL.StrassenRec.dimFintype m₀ k.succ = instFintypeSum (Transfer.Examples.CoqEAL.StrassenRec.dim m₀ k) (Transfer.Examples.CoqEAL.StrassenRec.dim m₀ k)

@[instance_reducible]

instance Transfer.Examples.CoqEAL.StrassenRec.dimDecEq (m₀ : Type u_2) [DecidableEq m₀] (fuel : ℕ) : DecidableEq (dim m₀ fuel)

Equations

• Transfer.Examples.CoqEAL.StrassenRec.dimDecEq m₀ 0 = Transfer.Examples.CoqEAL.StrassenRec.dimDecEq._aux_1 m₀
• Transfer.Examples.CoqEAL.StrassenRec.dimDecEq m₀ k.succ = instDecidableEqSum

theorem Transfer.Examples.CoqEAL.StrassenRec.strassen_blocks_eq {R : Type u_1} [CommRing R] {m : Type u_2} [Fintype m] [DecidableEq m] (A11 A12 A21 A22 B11 B12 B21 B22 : Matrix m m R) : Matrix.fromBlocks ((A11 + A22) * (B11 + B22) + A22 * (B21 - B11) - (A11 + A12) * B22 + (A12 - A22) * (B21 + B22)) (A11 * (B12 - B22) + (A11 + A12) * B22) ((A21 + A22) * B11 + A22 * (B21 - B11)) ((A11 + A22) * (B11 + B22) - (A21 + A22) * B11 + A11 * (B12 - B22) + (A21 - A11) * (B11 + B12)) = Matrix.fromBlocks A11 A12 A21 A22 * Matrix.fromBlocks B11 B12 B21 B22

The non-commutative block Strassen recombination identity. For four blocks of each operand (over any matrix ring Matrix m m R, which is not commutative), the Strassen seven-product recombination of the blocks equals the block product fromBlocks … * fromBlocks …. The seven products appear in operand order, so the identity holds over the non-commutative block ring.

def Transfer.Examples.CoqEAL.StrassenRec.strassenRec {R : Type u_1} [CommRing R] (m₀ : Type u_2) [Fintype m₀] [DecidableEq m₀] (fuel : ℕ) : Matrix (dim m₀ fuel) (dim m₀ fuel) R → Matrix (dim m₀ fuel) (dim m₀ fuel) R → Matrix (dim m₀ fuel) (dim m₀ fuel) R

Fuel-recursive Strassen multiply on the doubled block index dim m₀ fuel. Fuel 0 is the ordinary product; each fuel step splits into four blocks, forms seven Strassen products with recursive calls, and recombines.

Equations

• One or more equations did not get rendered due to their size.
• Transfer.Examples.CoqEAL.StrassenRec.strassenRec m₀ 0 A B = A * B

theorem Transfer.Examples.CoqEAL.StrassenRec.strassenRec_eq {R : Type u_1} [CommRing R] (m₀ : Type u_2) [Fintype m₀] [DecidableEq m₀] (fuel : ℕ) (A B : Matrix (dim m₀ fuel) (dim m₀ fuel) R) : strassenRec m₀ fuel A B = A * B

Recursive Strassen correctness. The fuel-recursive Strassen multiply equals the ordinary matrix product, for any fuel. Induction on fuel: the base is *; the step rewrites the seven recursive products to * via the IH, reassembles via Matrix.fromBlocks_toBlocks, and closes with the non-commutative block Strassen identity strassen_blocks_eq.