Strassen one-level 2×2 block multiplication identity

This file states and proves the classic Strassen fast-matrix-multiply identity at one level over a CommRing R: the product of two 2×2 matrices can be computed with seven scalar multiplications (M1 … M7) and a handful of additions, rather than the naive eight. The result entries are recombinations of the seven products, and they reproduce the ordinary matrix product A * B (Mathlib Matrix.mul, i.e. *).

This is the matrix-multiplication-tail companion to the CoqEAL seqmatrix multiply refinement of SeqMatrixMul.lean: that file establishes the naive row-col multiply refinement square; here we record the fast (Strassen) recombination identity for the base 2×2 case.

Scope

This file proves only the one-level 2×2 block identity. Recursive Strassen — recursing on 2×2 block matrices down to a base case — is in StrassenRec.lean. The one-level identity is the algebraic step of the recursion (at the leaf the blocks are scalars).

API

• Strassen.M1 … M7 — the seven Strassen products of the 2×2 entries.
• Strassen.result — the 2×2 matrix recombined from M1 … M7.
• Strassen.result_eq_mul — result A B = A * B (the verified identity).

def Transfer.Examples.CoqEAL.Strassen.M1 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

The seven Strassen products, computed from the entries of A and B (2×2 matrices over a commutative ring). With A = [[a11,a12],[a21,a22]] and B = [[b11,b12],[b21,b22]] (0/1-indexed via Fin 2):

• M1 = (a11 + a22)(b11 + b22)
• M2 = (a21 + a22) b11
• M3 = a11 (b12 - b22)
• M4 = a22 (b21 - b11)
• M5 = (a11 + a12) b22
• M6 = (a21 - a11)(b11 + b12)
• M7 = (a12 - a22)(b21 + b22)

Equations

• Transfer.Examples.CoqEAL.Strassen.M1 A B = (A 0 0 + A 1 1) * (B 0 0 + B 1 1)

def Transfer.Examples.CoqEAL.Strassen.M2 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M2 = (a21 + a22) b11.

Equations

• Transfer.Examples.CoqEAL.Strassen.M2 A B = (A 1 0 + A 1 1) * B 0 0

def Transfer.Examples.CoqEAL.Strassen.M3 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M3 = a11 (b12 - b22).

Equations

• Transfer.Examples.CoqEAL.Strassen.M3 A B = A 0 0 * (B 0 1 - B 1 1)

def Transfer.Examples.CoqEAL.Strassen.M4 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M4 = a22 (b21 - b11).

Equations

• Transfer.Examples.CoqEAL.Strassen.M4 A B = A 1 1 * (B 1 0 - B 0 0)

def Transfer.Examples.CoqEAL.Strassen.M5 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M5 = (a11 + a12) b22.

Equations

• Transfer.Examples.CoqEAL.Strassen.M5 A B = (A 0 0 + A 0 1) * B 1 1

def Transfer.Examples.CoqEAL.Strassen.M6 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M6 = (a21 - a11)(b11 + b12).

Equations

• Transfer.Examples.CoqEAL.Strassen.M6 A B = (A 1 0 - A 0 0) * (B 0 0 + B 0 1)

def Transfer.Examples.CoqEAL.Strassen.M7 {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : R

Strassen product M7 = (a12 - a22)(b21 + b22).

Equations

• Transfer.Examples.CoqEAL.Strassen.M7 A B = (A 0 1 - A 1 1) * (B 1 0 + B 1 1)

def Transfer.Examples.CoqEAL.Strassen.result {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : Matrix (Fin 2) (Fin 2) R

The 2×2 result matrix recombined from the seven Strassen products:

• c11 = M1 + M4 - M5 + M7
• c12 = M3 + M5
• c21 = M2 + M4
• c22 = M1 - M2 + M3 + M6

Equations

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

theorem Transfer.Examples.CoqEAL.Strassen.result_eq_mul {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : result A B = A * B

Strassen one-level identity. The seven-multiplication recombination result A B equals the ordinary matrix product A * B for 2×2 matrices over a commutative ring.