p2m_matMulExp_lt
Openalgebraic-complexityasymptotic-spectraborder-rankcomputational-complexitymatrix-multiplicationomega-exponentready-to-formalizerepresentation-theoryring-theoryschonhagestrassentensors
Schönhage's bound (ω < 2.55). The matrix-multiplication exponent ω, defined as inf_n log(rank(MM n n n)) / log n with respect to the canonical restriction-based Strassen preorder on the order-3 tensor semiring Tensor ℚ 3, satisfies ω < 51/20 = 2.55. Schönhage (1981) proved this via a direct-sum construction MM(n,1,m) ⊕ MM(1,(n-1)(m-1),1) of border rank ≤ nm+1, combined with the asymptotic sum inequality (recovered here from Strassen's duality on the asymptotic spectrum). The supporting definitions are uploaded as p2m_* platform definitions; this problem asks for the proof.
Formal statement
import Definitions.Def_p2m_Tensor_matMulExp
universe u
/-- **Schönhage's bound (ω < 2.55).** The matrix-multiplication exponent
satisfies `ω < 51/20`. This is the prove2me mission target; the proof in
the upstream project (`AsymptoticSpectra.Tensor.Schonhage.matMulExp_lt`)
goes via the direct-sum construction `MM(n,1,m) ⊕ MM(1,(n-1)(m-1),1)` and
the asymptotic sum inequality. -/
theorem p2m_matMulExp_lt {K : Type u} [Field K] : Tensor.matMulExp (K := K) < 51 / 20 := by sorry
Source
Schönhage, A. (1981). Partial and total matrix multiplication. SIAM J. Comput. 10(3), 434–455. Formalised in the AsymptoticSpectra Lean 4 project (Tensor.matMulExp_lt in AsymptoticSpectra/Tensor/Schonhage.lean).