Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 5.1: five recursive fourth-power constituent values

Open
mme_stothers_lemma51_recursive_values

by marwahaha · Aug 29, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Let KKK be an arbitrary field and let τ∈R\tau\in\mathbb Rτ∈R satisfy 2≤3τ≤32\le3\tau\le32≤3τ≤3. Put

E=(12)3τ,H=(38)3τ,L=4 63τ(63τ+2).E=(12)^{3\tau},\qquad H=(38)^{3\tau},\qquad L=4\,6^{3\tau}(6^{3\tau}+2).E=(12)3τ,H=(38)3τ,L=463τ(63τ+2).

Write

R116=4(E2+2L),R125=4(L+EH)(2H+L)/H,R134=4(E+L)(2+2E+H),R224=(2H+L)2(2+2E+H)/H,R233=4(E+L)2(2H+L)/L.\begin{aligned} R_{116}&=4(E^2+2L),\\ R_{125}&=4(L+EH)(2H+L)/H,\\ R_{134}&=4(E+L)(2+2E+H),\\ R_{224}&=(2H+L)^2(2+2E+H)/H,\\ R_{233}&=4(E+L)^2(2H+L)/L. \end{aligned}R116​R125​R134​R224​R233​​=4(E2+2L),=4(L+EH)(2H+L)/H,=4(E+L)(2+2E+H),=(2H+L)2(2+2E+H)/H,=4(E+L)2(2H+L)/L.​

For each row and every fixed real VVV with 0≤V<Rijk0\le V<R_{ijk}0≤V<Rijk​, the cyclic symmetrization of the corresponding literal constituent φijk\varphi_{ijk}φijk​ of CW6⊗4CW_6^{\otimes4}CW6⊗4​ has tau-value at least VVV.

This strict-lower-base form is the source-faithful encoding of the five limiting exponential-rate bounds in Davie--Stothers Lemma 5.1. The cyclic symmetrization represents the cube in the platform's normalization ρ=3τ\rho=3\tauρ=3τ. The strict inequality is essential: the platform predicate requires a constant-relative finite witness, whereas the paper's pruning argument may lose a subexponential factor and therefore need not attain the limiting base itself.

Preamble
import Definitions.Def_mme_stothers_fourth_data

open MME

universe u

set_option autoImplicit false
Formal statement
theorem mme_stothers_lemma51_recursive_values
    {K : Type u} [Field K] (tau : Real)
    (htauLower : 2 ≤ 3 * tau) (htauUpper : 3 * tau ≤ 3) :
    (∀ V : Real, 0 ≤ V →
      V < MME.StothersFourth.classValue 6 tau 5 →
      HasTauValueAtLeast
        (cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 1 1 6)) tau V) ∧
    (∀ V : Real, 0 ≤ V →
      V < MME.StothersFourth.classValue 6 tau 6 →
      HasTauValueAtLeast
        (cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 1 2 5)) tau V) ∧
    (∀ V : Real, 0 ≤ V →
      V < MME.StothersFourth.classValue 6 tau 7 →
      HasTauValueAtLeast
        (cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 1 3 4)) tau V) ∧
    (∀ V : Real, 0 ≤ V →
      V < MME.StothersFourth.classValue 6 tau 8 →
      HasTauValueAtLeast
        (cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 2 2 4)) tau V) ∧
    (∀ V : Real, 0 ≤ V →
      V < MME.StothersFourth.classValue 6 tau 9 →
      HasTauValueAtLeast
        (cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 2 3 3)) tau V) := by
  sorry
Source
Davie and Stothers (2013), Lemma 5.1(i)-(v), printed pp. 363-366, https://www.maths.ed.ac.uk/~sandy/a11164.pdf; Stothers thesis (2010), Chapter 4.3, Lemmas 21-25.
Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every universe level uuu, every type K:Type uK : \mathrm{Type}\,uK:Typeu equipped with a field structure (with no further restriction on the field), and every real number τ\tauτ such that 2≤3τ≤32 \le 3\tau \le 32≤3τ≤3, the following five assertions hold simultaneously. Put E=123τE=12^{3\tau}E=123τ, H=383τH=38^{3\tau}H=383τ, and Λ=4⋅63τ(63τ+2)\Lambda=4\cdot 6^{3\tau}(6^{3\tau}+2)Λ=4⋅63τ(63τ+2), where these are real powers, and put v5=4(E2+2Λ)v_5=4(E^2+2\Lambda)v5​=4(E2+2Λ), v6=4(Λ+EH)(2H+Λ)/Hv_6=4(\Lambda+EH)(2H+\Lambda)/Hv6​=4(Λ+EH)(2H+Λ)/H, v7=4(E+Λ)(2+2E+H)v_7=4(E+\Lambda)(2+2E+H)v7​=4(E+Λ)(2+2E+H), v8=(2H+Λ)2(2+2E+H)/Hv_8=(2H+\Lambda)^2(2+2E+H)/Hv8​=(2H+Λ)2(2+2E+H)/H, and v9=4(E+Λ)2(2H+Λ)/Λv_9=4(E+\Lambda)^2(2H+\Lambda)/\Lambdav9​=4(E+Λ)2(2H+Λ)/Λ; these are exactly the five threshold entries at zero-based indices 5,…,95,\ldots,95,…,9, and the hypotheses on τ\tauτ make HHH and Λ\LambdaΛ positive, so the displayed denominators are nonzero. To define the tensors occurring in the assertions, let e0,…,e7e_0,\ldots,e_7e0​,…,e7​ be the standard basis of K8K^8K8, let W=∑r=16(e0⊗er⊗er+er⊗e0⊗er+er⊗er⊗e0)+e0⊗e0⊗e7+e0⊗e7⊗e0+e7⊗e0⊗e0W=\sum_{r=1}^{6}(e_0\otimes e_r\otimes e_r+e_r\otimes e_0\otimes e_r+e_r\otimes e_r\otimes e_0)+e_0\otimes e_0\otimes e_7+e_0\otimes e_7\otimes e_0+e_7\otimes e_0\otimes e_0W=∑r=16​(e0​⊗er​⊗er​+er​⊗e0​⊗er​+er​⊗er​⊗e0​)+e0​⊗e0​⊗e7​+e0​⊗e7​⊗e0​+e7​⊗e0​⊗e0​, and form the modewise Kronecker product F=(W⊠W)⊠(W⊠W)F=(W\boxtimes W)\boxtimes(W\boxtimes W)F=(W⊠W)⊠(W⊠W), with exactly these parentheses. Give a standard-basis coordinate r∈{0,…,7}r\in\{0,\ldots,7\}r∈{0,…,7} grade g(r)=0g(r)=0g(r)=0 when r=0r=0r=0, grade g(r)=2g(r)=2g(r)=2 when r=7r=7r=7, and grade g(r)=1g(r)=1g(r)=1 otherwise. In each of the three mode spaces of FFF, the tensor-product basis is indexed by ((r1,r2),(r3,r4))((r_1,r_2),(r_3,r_4))((r1​,r2​),(r3​,r4​)), and that basis vector has grade g(r1)+g(r2)+g(r3)+g(r4)∈{0,…,8}g(r_1)+g(r_2)+g(r_3)+g(r_4)\in\{0,\ldots,8\}g(r1​)+g(r2​)+g(r3​)+g(r4​)∈{0,…,8}. For I,J,L∈{0,…,8}I,J,L\in\{0,\ldots,8\}I,J,L∈{0,…,8}, let CI,J,LC_{I,J,L}CI,J,L​ be the tensor obtained from FFF by projecting mode 000 onto the span of its grade-III basis vectors, mode 111 onto the span of its grade-JJJ basis vectors, and mode 222 onto the span of its grade-LLL basis vectors, with those three spans themselves serving as the new mode spaces. If P(C)P(C)P(C) denotes the mode reindexing whose new mode order is (2,0,1)(2,0,1)(2,0,1), then define Cyc⁡(C)=C⊠(P(C)⊠P2(C))\operatorname{Cyc}(C)=C\boxtimes(P(C)\boxtimes P^2(C))Cyc(C)=C⊠(P(C)⊠P2(C)), where P2(C)P^2(C)P2(C) has new mode order (1,2,0)(1,2,0)(1,2,0). Now, for each real VVV, (i) 0≤V<v50\le V<v_50≤V<v5​ implies H(Cyc⁡(C1,1,6),τ,V)\mathcal H(\operatorname{Cyc}(C_{1,1,6}),\tau,V)H(Cyc(C1,1,6​),τ,V); (ii) 0≤V<v60\le V<v_60≤V<v6​ implies H(Cyc⁡(C1,2,5),τ,V)\mathcal H(\operatorname{Cyc}(C_{1,2,5}),\tau,V)H(Cyc(C1,2,5​),τ,V); (iii) 0≤V<v70\le V<v_70≤V<v7​ implies H(Cyc⁡(C1,3,4),τ,V)\mathcal H(\operatorname{Cyc}(C_{1,3,4}),\tau,V)H(Cyc(C1,3,4​),τ,V); (iv) 0≤V<v80\le V<v_80≤V<v8​ implies H(Cyc⁡(C2,2,4),τ,V)\mathcal H(\operatorname{Cyc}(C_{2,2,4}),\tau,V)H(Cyc(C2,2,4​),τ,V); and (v) 0≤V<v90\le V<v_90≤V<v9​ implies H(Cyc⁡(C2,3,3),τ,V)\mathcal H(\operatorname{Cyc}(C_{2,3,3}),\tau,V)H(Cyc(C2,3,3​),τ,V). Here H(T,τ,V)\mathcal H(T,\tau,V)H(T,τ,V) literally means the conjunction of 0≤V0\le V0≤V (so the conclusion repeats the nonnegativity already assumed in each implication) with the following condition: for every real ε>0\varepsilon>0ε>0, there are arbitrarily large natural numbers NNN for which there exist a natural number kkk and natural-number families ai,bi,cia_i,b_i,c_iai​,bi​,ci​ indexed by i∈{0,…,k−1}i\in\{0,\ldots,k-1\}i∈{0,…,k−1} such that the recursively formed modewise direct sum of the matrix-multiplication tensors MMai,bi,ci=∑x<ai∑y<bi∑z<ciex,y⊗ey,z⊗ez,x\mathrm{MM}_{a_i,b_i,c_i}=\sum_{x<a_i}\sum_{y<b_i}\sum_{z<c_i} e_{x,y}\otimes e_{y,z}\otimes e_{z,x}MMai​,bi​,ci​​=∑x<ai​​∑y<bi​​∑z<ci​​ex,y​⊗ey,z​⊗ez,x​ is a restriction of the NNN-fold modewise Kronecker power T⊠NT^{\boxtimes N}T⊠N—that is, there are three KKK-linear maps from the respective mode spaces of T⊠NT^{\boxtimes N}T⊠N to those of that direct sum whose tensor-product map sends the tensor of T⊠NT^{\boxtimes N}T⊠N exactly to the direct-sum tensor—and VN(1−ε)≤∑i=0k−1(aibici)τV^N(1-\varepsilon)\le\sum_{i=0}^{k-1}(a_i b_i c_i)^{\tau}VN(1−ε)≤∑i=0k−1​(ai​bi​ci​)τ, with each natural product cast to a real number before taking the real power. “Arbitrarily large” is the literal meaning of the filter-frequently quantifier here: for every natural lower bound, at least one such NNN at or above it exists; it does not say that every sufficiently large NNN works. The definition allows N=0N=0N=0, whose tensor power is the unit tensor object, allows k=0k=0k=0, whose direct sum is the zero tensor object and whose numerical sum is empty, allows every dimension ai,bi,cia_i,b_i,c_iai​,bi​,ci​ to be zero, and places no upper bound on ε\varepsilonε. In particular, all five outer quantifiers include V=0V=0V=0 (each vjv_jvj​ above is positive under the stated hypotheses), and for positive NNN the V=0, k=0V=0,\ k=0V=0, k=0 case is permitted by the literal definition.

Human review
  • Endorsed by Shuze Chen · Aug 30, 2026

  • Endorsed by marwahaha · Aug 30, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me