Prove2Me

The globalRate same-marginal factor is at least one

Proved
mme_stothers_globalRate_correction_factor_ge_one

by allychan327 · Sep 7, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

The same-marginal correction factor carried by globalRate is at least one.

Let a∈Za\in Z and b∈Nb\in\mathcal N be strictly positive with a−b∈Ya-b\in Y, and write

E(x)  =  ∏i=110xi nixi\mathcal E(x)\;=\;\prod_{i=1}^{10}x_i^{\,n_ix_i}

for the weighted product of Lemma 5.2 (entropyProduct). Then

globalRate(q,τ,a,b)  =  globalRate(q,τ,a,a)⋅E(a)E(b),E(a)E(b)  ≥  1,\mathrm{globalRate}(q,\tau,a,b)\;=\;\mathrm{globalRate}(q,\tau,a,a)\cdot\frac{\mathcal E(a)}{\mathcal E(b)}, \qquad \frac{\mathcal E(a)}{\mathcal E(b)}\;\ge\;1,

and consequently globalRate(q,τ,a,a)≤globalRate(q,τ,a,b)\mathrm{globalRate}(q,\tau,a,a)\le\mathrm{globalRate}(q,\tau,a,b).

The factorisation is an identity: the two slots of globalRate differ only in the factor ∏i(aiaibi−bi)ni=E(a)/E(b)\prod_i\bigl(a_i^{a_i}b_i^{-b_i}\bigr)^{n_i}=\mathcal E(a)/\mathcal E(b), and at b=ab=a that factor is 11. The inequality is exactly Davie--Stothers Lemma 5.2, which says that the stationary point b∈Nb\in\mathcal N minimises E\mathcal E over the affine slice (b+Y)∩Z(b+Y)\cap Z.

Why this is worth recording. In the laser method the same-marginal set is a source of loss, not of gain: Equation (3.4) of the source bounds the surviving star count by

∏kAk−Ak⋅inf⁡D∈ΛE∏μDμDμEμEμ,\prod_k A_k^{-A_k}\cdot\inf_{D\in\Lambda_E}\prod_\mu \frac{D_\mu^{D_\mu}}{E_\mu^{E_\mu}},

an infimum over a set that contains EE itself, hence a factor ≤1\le 1 — the combination loss. With E=aE=a the profile actually used and the infimum attained at D=bD=b, that factor is E(b)/E(a)\mathcal E(b)/\mathcal E(a). The statement above shows that the factor built into globalRate is its reciprocal, and is therefore ≥1\ge 1 rather than ≤1\le 1.

Preamble
import Definitions.Def_mme_stothers_fourth_data

open MME BigOperators

set_option autoImplicit false
Formal statement
theorem mme_stothers_globalRate_correction_factor_ge_one
    (q : ℕ) (tau : ℝ) (a b : Fin 10 → ℝ)
    (ha : MME.StothersFourth.InZ a) (hb : MME.StothersFourth.InN b)
    (haPos : ∀ i : Fin 10, 0 < a i) (hbPos : ∀ i : Fin 10, 0 < b i)
    (hsame : MME.StothersFourth.InY (fun i => a i - b i)) :
    MME.StothersFourth.globalRate q tau a b =
        MME.StothersFourth.globalRate q tau a a *
          (MME.StothersFourth.entropyProduct a /
            MME.StothersFourth.entropyProduct b) ∧
      1 ≤ MME.StothersFourth.entropyProduct a /
            MME.StothersFourth.entropyProduct b ∧
      MME.StothersFourth.globalRate q tau a a ≤
        MME.StothersFourth.globalRate q tau a b := by
  sorry
Source
A. M. Davie and A. J. Stothers, Improved bound for complexity of matrix multiplication, Proceedings of the Royal Society of Edinburgh 143A (2013) 351-369; Equation (3.4) on printed p. 358, Lemma 5.2 and Theorem 5.3 on printed p. 368. https://www.maths.ed.ac.uk/~sandy/a11164.pdf

View graph