N=2 steps have one parent occurrence

Proved

mme_N2_total_occurrences_eq_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 has exactly one parent occurrence in total.

Since $L=2$ and positions pair each occurrence, $2 = 2\sum_r n_r$ forces $\sum_r n_r = 1$ .

Formalization Note Combines the length-two and census lemmas through the position equivalence.

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
open scoped BigOperators
set_option autoImplicit false

Formal statement

theorem mme_N2_total_occurrences_eq_one : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)), ∑ r, S.n r = 1 := by sorry

Source

Corollary of mme_N2_step_L_eq_two and mme_position_card_eq.

View graph