Weighted profile value is bounded by the fifth class value

Proved

mme_stothers_phi116_profile_value_le_class_value

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

algebraic-complexitydavie-stothersinequalityphi-116tau-value

For the positive Davie--Stothers parameters $L(6,\tau)$ and $E(6,\tau)$ and any $0<a<1$ , the optimized two-component profile value satisfies

4\left(\frac{2L(6,\tau)}{a}\right)^a\left(\frac{E(6,\tau)^2}{1-a}\right)^{1-a}\le 4\bigl(E(6,\tau)^2+2L(6,\tau)\bigr).

The right-hand side is the fifth class value in the source table. The inequality is the weighted arithmetic--geometric mean inequality and supplies the numerical bridge from the arbitrary profile parameter in the phi-116 frontier theorem to its class-value interface.

Preamble

import Mathlib.Analysis.MeanInequalities
import Mathlib.Tactic
import Definitions.Def_mme_stothers_fourth_data

open MME
universe u

Formal statement

theorem mme_stothers_phi116_profile_value_le_class_value
    (tau a : Real) (haPos : 0 < a) (haLt : a < 1) :
    4 * (((2 * MME.StothersFourth.L 6 tau) / a) ^ a *
      ((MME.StothersFourth.E 6 tau ^ (2 : ℕ)) / (1 - a)) ^ (1 - a)) ≤
      MME.StothersFourth.classValue 6 tau 5 := by
  sorry

Source

A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication (2013), Section 5, Lemma 5.1 and the fifth class-value entry; https://www.maths.ed.ac.uk/~sandy/a11164.pdf.

View graph