A compatible fine fourth-power block restricts from its coarse block

Proved

mme_CW_fourth_fine_block_restrict_coarse_block

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

algebraic-complexitycoppersmith-winogradgraded-tensorlaser-methodtensor-restriction

Let a fine block of the fourth Coppersmith--Winograd power be specified by two square-block grades $(I_1,J_1,L_1)$ and $(I_2,J_2,L_2)$ . Suppose their modewise sums equal a coarse fourth-power grade $\kappa$ :

I_1+I_2=\kappa_0,\qquad J_1+J_2=\kappa_1,\qquad L_1+L_2=\kappa_2.

Then the literal fine product-grading block is a tensor restriction of the coarse $\kappa$ block. This is the general source-faithful bridge needed to place the fine constituent decompositions for $\varphi_{125},\varphi_{134},\varphi_{224}$ , and $\varphi_{233}$ inside their actual coarse fourth-power constituents.

Preamble

import Mathlib.Tactic
import Definitions.Def_mme_stothers_phi116_fine_blocks

open MME TensorProduct Module

universe u

set_option autoImplicit false

Formal statement

theorem mme_CW_fourth_fine_block_restrict_coarse_block
    {K : Type u} [Field K] (q : ℕ)
    (I₁ J₁ L₁ I₂ J₂ L₂ : Fin 5)
    (coarse : Fin 3 → Fin 9)
    (hsum : ∀ s,
      (cwSquareBlockType I₁ J₁ L₁ s).val +
          (cwSquareBlockType I₂ J₂ L₂ s).val =
        (coarse s).val) :
    TensorObj.Restrict
      (MME.StothersFourth.Phi116.cwFourthFineBlockObj
        K q I₁ J₁ L₁ I₂ J₂ L₂)
      ((MME.StothersFourth.cwFourthCanonicalGrading K q).blockSubtensor
        coarse) := by
  sorry

Source

The canonical fine-to-coarse grading relation used throughout A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication (2013), Section 5 and Table 1, pp. 365--368, https://www.maths.ed.ac.uk/~sandy/a11164.pdf; formalized for the literal fourth Coppersmith--Winograd power.

View graph