mme_omega_le_of_subrank_capacity
DisprovedThe abstract ω-bound from subrank capacity (Strassen–Schönhage / Wigderson–Zuiddam).
For any order-3 tensor T : TensorObj K 3, real upper bound R ≥ 1 on the asymptotic rank, and real lower bound V > 1 on the subrank capacity,
Proof sketch (Hölder + Schönhage's τ + asymptotic limit; deferred to a sub-decomposition):
-
From , for each extract infinitely many with and , where the number of summands is subexponential in .
-
Apply
mme_asymptotic_sum_inequality(Schönhage's τ-theorem, already Proved) to get . -
Use Hölder's inequality with conjugate exponents :
- Taking -th roots and using (subexponential growth), the limit gives , i.e. .
Reusability — first-class principle. This theorem carries zero content specific to any particular tensor or paper. Every subsequent ω-bound improvement instantiates this exact bridge with its own tensor's pair; only the lower bound on subrank capacity differs paper-to-paper. The abstract framework here is the load-bearing piece of the entire matrix-multiplication-exponent program.
import Mathlib.Analysis.SpecialFunctions.Log.Basic import Definitions.Def_mme_subrank_capacity import Definitions.Def_mme_omega_strassen open MME universe u
theorem mme_omega_le_of_subrank_capacity {K : Type u} [Field K] {T : TensorObj K 3} {R V : ℝ} (hR : tensorAsymptoticRank T ≤ R) (hRpos : 1 ≤ R) (hV : 1 < V) (hsub : V ≤ subrankCapacity T) : matMulExp_strassen K ≤ Real.log R / Real.log V := by sorry