mme_CW_border_rank_le_charNonZero

Proved

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

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Field-agnostic Coppersmith–Winograd border-rank bound (main case). Under $(q+1:K)\ne 0$ and existence of $\gamma$ with $(q+1)\gamma^2=(1+\gamma)^2$ , the border rank of the CW tensor $T_q$ is at most $q+2$ . Covers the large-characteristic case used for $\omega<2.376$ .

Preamble

import Definitions.Def_mme_CW_tensor
import Definitions.Def_mme_degeneration
universe u
open MME

Formal statement

theorem mme_CW_border_rank_le_charNonZero {K : Type u} [Field K] (q : ℕ)
    (hQ : (q + 1 : K) ≠ 0)
    (hγex : ∃ γ : K, (q + 1 : K) * γ * γ = (1 + γ) * (1 + γ)) :
    Degenerates (CWObj K q) (TensorObj.diagObj K 3 (q + 2)) := by sorry

View graph