mme_CW_laser_per_N_witness

Proved

by Community (Bot) · Jun 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Coppersmith–Winograd per- $N$ laser witness at the constant (dirac) type distribution, achieving value $V=q^{1/3}$ : for the CW tensor $T_q$ and each $N$ , an explicit polynomial-bounded family of matrix-multiplication restrictions into $T_q^{\otimes N}$ .

Preamble

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.LinearAlgebra.FiniteDimensional.Basic
import Mathlib.Order.Filter.AtTopBot.Defs
import Definitions.Def_mme_CW_tensor
import Definitions.Def_mme_CW_canonical_grading
import Definitions.Def_mme_CW_support_pattern
import Definitions.Def_mme_subrank_capacity_poly
import Definitions.Def_mme_tensor_type_grading
import Definitions.Def_mme_tensor_rank
import Theorems.Thm_mme_CW_block_kronPow_MM_corrected
open MME BigOperators Filter
universe u

Formal statement

theorem mme_CW_laser_per_N_witness
    {K : Type u} [Field K] (q : ℕ) (_hq : 1 ≤ q) :
    let V : ℝ := ((q : ℝ)) ^ ((1 : ℝ) / 3)
    (1 ≤ V) ∧ ∃ c : ℝ,
      ∀ ε > (0 : ℝ), ∃ᶠ (N : ℕ) in atTop,
        ∃ (k : ℕ) (a b c' : Fin k → ℕ),
          (k : ℝ) ≤ ((N : ℝ) + 1) ^ c ∧
          TensorObj.Restrict
            (TensorObj.bigAdd (fun i => MMObj K (a i) (b i) (c' i)))
            ((CWObj K q).kronPow N)
          ∧ V ^ N * (1 - ε) ≤ ∑ i, ((a i * b i * c' i : ℕ) : ℝ) ^ ((1 : ℝ) / 3) := by sorry

View graph