N=2 steps have length two

Proved

mme_N2_step_L_eq_two

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer step with two elementary positions has length parameter $L=2$ .

At levels $0$ and $1$ (the only ones possible at $N=2$ ) the length equation reads $L\cdot 1 = 2$ . This pins the position skeleton both open leaves must build on.

Formalization Note Uses the level case split plus the length field.

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
set_option autoImplicit false

Formal statement

theorem mme_N2_step_L_eq_two : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)), S.L = 2 := by sorry

Source

Corollary of mme_N2_lower_zero_or_one and the IntegerStep length field.

View graph