N=2 steps have one region
Provedmme_N2_region_eq_onematrix-multiplicationmore-asymmetryregional-entropy
Every integer step with two elementary positions has exactly one region.
Each region carries at least one occurrence (via the minimum), and there is one occurrence in total, so there is exactly one region.
Formalization Note Combines the occurrence census with the parent-size fields.
Preamble
import Definitions.Def_mme_integer_regional_CW_recipe open scoped BigOperators set_option autoImplicit false
Formal statement
theorem mme_N2_region_eq_one : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)), S.R = 1 := by sorry
Source
Corollary of mme_N2_total_occurrences_eq_one with IntegerStep parent fields.