Level-two N=2 integer steps are impossible

Proved

mme_entropy_regional_step_L2_N2_impossible

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

matrix-multiplicationmore-asymmetryregional-entropy

At level $2$ with two elementary positions, no integer regional step exists.

The length equation is

L\,2^{2-1}=2,

so $L=1$ . But physical positions contain both halves of every parent occurrence, so one parent occurrence already supplies two distinct physical positions, which cannot inject into $\mathrm{Fin}(1)$ . Hence the type $\mathrm{IntegerStep}\,2\,2$ over any predicate is empty. This records why the fixed- $(2,2)$ step-boundary package is false and why any consistent level-two construction needs $M$ divisible by $4$ .

Formalization Note Lean uses truncated subtraction, so $2-1=1$ definitionally; the argument is by $\mathrm{Fin}.ext$ and injectivity of the position equivalence.

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
set_option autoImplicit false

Formal statement

theorem mme_entropy_regional_step_L2_N2_impossible : forall (S : MME.RegionRealization.IntegerStep 2 2 (fun _ _ => True)), False := by sorry

Source

Alman et al., More Asymmetry Yields Faster Matrix Multiplication, https://arxiv.org/html/2404.16349v2#S6, Section 6 sizing; consequence of IntegerStep length and Position fields. Follows the disproof of mme_entropy_regional_step_boundary_package.

View graph