Level-two step-boundary package with five copies and dimensions 25

Disproved

mme_entropy_regional_step_boundary_package

by Tamas Fulop · Sep 15, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

matrix-multiplicationmore-asymmetryregional-entropy

Level-two regional package for the More Asymmetry entropy route at $N=2$ . There is an integer entropy step $S$ at level $2$ over the trivial predicate, together with a level-two boundary profile $prof$ of dimension $25$ , such that three things hold: the profile dimension is $25$ ; the step guarantees at least five entropy copies,

5 \le \mathrm{copies}(S);

and the profile grade and usefulness conditions imply the step output predicate, so the boundary data built from $prof$ aligns with $S$ . This packages the Section 6 regional data (the level-two profile on the word $(1,1)$ contributes $5^2=25$ dimensions; one descend level contributes the five copies) into a single checkable node, separating the analytic copy bound and the profile alignment (proved elsewhere) from the recipe assembly (which consumes this package). Formalization Note Lean uses canonical single-cell conventions ( $L=1$ , profile mode $0$ ) for the alignment implication.

Retired: disproved - no N=2 step yields five entropy copies; small-N surplus is impossible. Replaced by mme_entropy_regional_smallN_no_surplus (delimitation to N>=3) and mme_entropy_regional_largeN_surplus_witness (remaining existence).

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
import Definitions.Def_mme_regional_entropy_copy_bound
import Definitions.Def_mme_recursive_profiled_CW_data
import Definitions.Def_mme_recursive_yz_boundary_data
import Definitions.Def_mme_recursive_yz_CW_cells
import Definitions.Def_mme_recursive_yz_compatibility

set_option autoImplicit false

Formal statement

theorem mme_entropy_regional_step_boundary_package :
    exists (S : MME.RegionRealization.IntegerStep 2 2 (fun _ _ => True))
      (prof : MME.RecursiveYZ.Boundary.Profile 2 1),
      prof.dim = 25 /\
      Nat.le 5 (MME.RegionRealization.IntegerStep.entropyCopies S) /\
      (forall (i : Fin 3) (x : MME.ProfiledCW.FineWord 2),
        ((forall _p : Fin 1,
            MME.RecursiveYZ.CWCells.grade
              (@MME.ProfiledCW.split (Fin 1) 2 1 2 (Equiv.refl (Fin 1))
                (by decide : 1 * 2 ^ (2 - 1) = 2) x _p) =
              (prof.shape 0) i) /\
          MME.RecursiveYZ.Useful (fun _ : Fin 1 => (0 : Fin 1))
            (fun _ : Fin 1 => prof.mu 0 i)
            (@MME.ProfiledCW.split (Fin 1) 2 1 2 (Equiv.refl (Fin 1))
              (by decide : 1 * 2 ^ (2 - 1) = 2) x)) ->
        S.output i x) := by sorry

Source

Alman et al., More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2#S6, Section 6 regional entropy construction with the level-two profile on the word (1,1) giving 5^2=25 dimensions

View graph