N=2 steps are at level 0 or 1

Proved

mme_N2_lower_zero_or_one

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer step with two elementary positions is at level $0$ or level $1$ .

This is the case-split form of the level bound $lower < 2$ : whoever proves the five-copy or boundary-match leaves only needs the two small cases.

Formalization Note Direct corollary of the proved level bound.

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
set_option autoImplicit false

Formal statement

theorem mme_N2_lower_zero_or_one : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)), lower = 0 ∨ lower = 1 := by sorry

Source

Corollary of mme_entropy_regional_step_N2_lt_two; case split for the regional leaves.

View graph