Motivation

The matrix-multiplication exponent $\omega$ measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.

Coppersmith and Winograd's 1990 analysis of the square of their tensor established $\omega<2.375477$. That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give $\omega<2.373689703$; see Davie--Stothers, printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the $2.375477$ bound.

This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint $2.3737$. It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.

Setting

For a field $K$, an order-three tensor represents a bilinear map. The matrix-multiplication tensor

$$\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{k<c} x_{ij}\otimes y_{jk}\otimes z_{ki}$$

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.

The Coppersmith--Winograd tensor $CW_q$ has border rank at most $q+2$ and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents $\varphi_{ijk}$ with $i+j+k=4$. Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by

$$\varphi_{008},\ \varphi_{017},\ \varphi_{026},\ \varphi_{035},\ \varphi_{044}, \ \varphi_{116},\ \varphi_{125},\ \varphi_{134},\ \varphi_{224},\ \varphi_{233}.$$

The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With $\rho\in[2,3]$, the paper writes

$$E=(2q)^\rho,\qquad H=(q^2+2)^\rho,\qquad L=4q^\rho(q^\rho+2),$$

and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the $9\times10$ matrix $Q$ in Equation (5.2); its kernel is the two-dimensional space $Y$ displayed immediately after that equation.

The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's HasTauValueAtLeast predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.

Formalization targets

Goal: the Davie--Stothers fourth-power bound

For every field $K$,

$$\operatorname{matMulExp}(K)<\frac{23737}{10000}=2.3737.$$

The source's computed endpoint $2.373689703$ is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and matMulExp definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.

Source-level milestones

The mission records the canonical nine-grading of $CW_6^{\otimes4}$ and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for $\varphi_{116}$, $\varphi_{125}$, $\varphi_{134}$, $\varphi_{224}$, and $\varphi_{233}$ in every-strict-lower-base form; Equation (5.2) and the stated basis of $\ker Q$; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to matMulExp.

Significance

Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.

For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.

The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the $\varphi_{116}$ profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.

Difficulty

The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of $CW_q^{\otimes4}$ and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.

The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The $\varphi_{233}$ class already has a nontrivial same-marginal family. At the global level the map $Q$ has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.

Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at $23737/10000$.

Formalization scope

The development uses environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and the existing TensorObj, MMObj, restriction, degeneration, HasTauValueAtLeast, tensorAsymptoticRank, matMulExp_strassen, and matMulExp declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.

The capstone specializes to $q=6$ and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.

Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.

Selected references

• A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication, Proceedings of the Royal Society of Edinburgh Section A: Mathematics 143(2), 2013, pp. 351--369. Author PDF and DOI 10.1017/S0308210511001646.
• A. J. Stothers, On the Complexity of Matrix Multiplication, PhD thesis, University of Edinburgh, 2010. Edinburgh Research Archive.
• Don Coppersmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. DOI 10.1016/S0747-7171(08)80013-2.
• Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.