The 45 fourth-power blocks and ten Table-1 classes

Proved

mme_stothers_fourth_table1_classification

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

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Among ordered triples $(i,j,k)\in\{0,\ldots,8\}^3$ , exactly 45 satisfy $i+j+k=8$ . Every such triple belongs to a unique coordinate-permutation orbit represented by one of

008,017,026,035,044,116,125,134,224,233.

The orbit of representative $r$ has cardinality $3n_r$ , where the Table-1 multiplicities are $n=(1,2,2,2,1,1,2,2,1,1)$ . This is the finite classification used to group the 45 fourth-power constituents into ten cyclic symmetry classes.

Preamble

import Definitions.Def_mme_stothers_fourth_data

open MME BigOperators

set_option autoImplicit false

Formal statement

theorem mme_stothers_fourth_table1_classification :
    Fintype.card
        {sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8} = 45 ∧
    (∀ sigma : {sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8},
      ∃! r : Fin 10,
        MME.StothersFourth.sameOrbit sigma.1
          (MME.StothersFourth.classRep r)) ∧
    (∀ r : Fin 10,
      Fintype.card
          {sigma : {sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8} //
            MME.StothersFourth.sameOrbit sigma.1
              (MME.StothersFourth.classRep r)} =
        3 * MME.StothersFourth.classMultiplicity r) := by
  sorry

Source

Davie and Stothers (2013), Section 5 and Table 1, printed pp. 363 and 367, https://www.maths.ed.ac.uk/~sandy/a11164.pdf.

View graph