Phi125 exact-edge tensor realization

Disproved

mme_stothers_phi125_edge_tensor_realization

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

algebraic-complexitycoppersmith-winograddavie-stotherslaser-methodphi-125tau-value

For an exact symmetric phi125 profile and a finite set of cyclic exact edges with mode-word injectivity, realize the retained edges as tensor blocks whose direct sum restricts the corresponding even power of the cyclic phi125 constituent. Every block has the uniform local tau-value lower bound below the supplied budget. This isolates the tensor realization and local constituent-value step of the Davie--Stothers extraction.

Preamble

import Definitions.Def_mme_stothers_fourth_data
import Definitions.Def_mme_stothers_phi125_profile_data
import Definitions.Def_mme_tau_value

open MME BigOperators Filter

universe u

set_option autoImplicit false

Formal statement

theorem mme_stothers_phi125_edge_tensor_realization
    {K : Type u} [Field K]
    (tau : ℝ) (N alpha beta gamma : ℕ)
    (hN : 0 < N) (hprofile : alpha + beta + gamma = N)
    (kept : Finset
      (MME.StothersFourth.Phi125.CyclicExactEdge N alpha beta gamma))
    (B : ℝ) (hB : 0 ≤ B)
    (hinjective :
      ∀ i : Fin 3,
        Function.Injective (fun e : kept ↦
          MME.StothersFourth.Phi125.cyclicModeWord e.1 i)) :
    ∃ (block : kept → TensorObj K 3),
      TensorObj.Restrict
        (TensorObj.bigAdd (fun j : Fin kept.card ↦
          block (kept.equivFin.symm j)))
        ((cyclicSymmetrization
          (MME.StothersFourth.cwFourthConstituent K 6 1 2 5)).kronPow
            (2 * N)) ∧
      (∀ e : kept, ∀ W : ℝ,
        0 ≤ W → W < B → HasTauValueAtLeast (block e) tau W) := by
  sorry

Source

A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication (2013), Section 5, Lemma 5.1(ii), printed pp. 364-365; https://www.maths.ed.ac.uk/~sandy/a11164.pdf.

View graph