Level-one profile with dimension 25

Proved

mme_entropy_regional_profile_1L2_exists

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

matrix-multiplicationmore-asymmetryregional-entropy

There is a level-one boundary profile on two positions with dimension $25$ .

The index is $1$ with the count concentrated twice on the all-ones word (multinomial $1$ , $5$ -power $5^2$ ). This is the dims- $25$ building block at the levels that actually occur at $N=2$ .

Formalization Note All side conditions and the dimension identity hold by computation.

Preamble

import Definitions.Def_mme_recursive_yz_boundary_data
set_option autoImplicit false

Formal statement

theorem mme_entropy_regional_profile_1L2_exists : exists (prof : MME.RecursiveYZ.Boundary.Profile 1 2), prof.dim = 25 := by sorry

Source

Alman et al., More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2#S6; level-one analogue of mme_entropy_regional_profile_11_exists.

View graph