Table 2: exact q=6 fixed-tau surplus at 2.3737

Open

mme_stothers_fourth_fixed_tau_value_23737

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

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Let $K$ be an arbitrary field. At

\tau=\frac{23737}{30000},

the tensor $CW_6\otimes CW_6$ has tau-value at least

\frac{640000001}{10000000}=64.0000001>64.

This is an exact-rational fixed-tau certificate extracted from the Davie--Stothers fourth-power calculation and Table 2. The fourth-power value has been square-rooted back to the square tensor so that the result interfaces directly with the established asymptotic-rank bound $\widetilde R(CW_6^{\otimes2})\le64$ .

Preamble

import Definitions.Def_mme_stothers_fourth_data

open MME

universe u

set_option autoImplicit false

Formal statement

theorem mme_stothers_fourth_fixed_tau_value_23737
    {K : Type u} [Field K] :
    HasTauValueAtLeast
      (TensorObj.kron (CWObj K 6) (CWObj K 6))
      (23737 / 30000) (640000001 / 10000000) := by
  sorry

Source

Davie and Stothers (2013), Theorem 5.3 and Table 2, printed p. 368, reporting omega < 2.373689703, https://www.maths.ed.ac.uk/~sandy/a11164.pdf; Stothers thesis (2010), Chapter 4.2, printed pp. 80-81.

Read-back

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

Blind read-back of Milestone5.lean

mme_stothers_fourth_fixed_tau_value_23737

For every universe level $u$ and every type $K : \mathrm{Type}\,u$ equipped with a field structure, the theorem asserts the imported predicate $\mathrm{HasTauValueAtLeast}$ for the twofold Kronecker tensor object $\operatorname{kron}(\mathrm{CWObj}(K,6),\mathrm{CWObj}(K,6))$ , at the exact real parameter $\tau=\frac{23737}{30000}$ , with the exact lower value $\frac{640000001}{10000000}=64.0000001$ . The tensor is exactly one Kronecker product of two copies of $\mathrm{CWObj}(K,6)$ , not the fourfold object defined in Definition.lean; there is no interval hypothesis on $\tau$ , no auxiliary vector, positivity, normalization, or polynomial hypothesis, and no restriction on $K$ beyond being a field. The conclusion is an “at least” predicate rather than equality, and the imported notions $\mathrm{CWObj}$ , Kronecker product, and $\mathrm{HasTauValueAtLeast}$ are not further defined in the audited code.

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