# Matrix multiplication with exponent at most 9/4

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Complex Matrix Multiplication Below 2.258 and Rectangular Bounds](../../preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026.pdf)
- [Staggered extraction for exact matrix multiplication over every field](../../preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026.pdf)

## Scope

The formalized results bound the complex matrix-multiplication exponent by $\omega(\mathbb C)\le9/4$, the dual exponent by $\alpha>0.465$, and the rectangular exponent at aspect ratio $0.709$ by $\omega(\mathbb C;1,0.709,1)<2.092$. The dual exponent is the supremum of rectangular aspect ratios attainable with exponent $2$. The arithmetic model counts additions, subtractions, and multiplications in finite division-free programs, with arbitrary positive exponent slack. The square bound implies the paper's weaker $2.258$ headline bound.

The formalized result gives the unconditional bound $\omega(F)<2.371054886006746$ for every field $F$, including finite fields and fields of positive characteristic. The exponent counts additions, subtractions, and multiplications in finite division-free arithmetic programs, with arbitrary positive exponent slack. No numerical inequalities remain as hypotheses. The result concerns arithmetic complexity, rather than bit complexity or practical crossover sizes.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Complex square, dual, and rectangular exponent bounds | [MatrixMultiplication.lean](../ComparatorChallenges/MatrixMultiplication.lean) |
| Matrix-multiplication exponent over every field | [MatrixFields.lean](../ComparatorChallenges/MatrixFields.lean) |