Each N=2 region carries one occurrence
Provedmme_N2_occ_eq_onematrix-multiplicationmore-asymmetryregional-entropy
In every integer step with two elementary positions, each region carries exactly one occurrence.
Each region has at least one occurrence while the total is one, so every region has exactly one.
Formalization Note Single-element bound against the total census.
Preamble
import Definitions.Def_mme_integer_regional_CW_recipe open scoped BigOperators set_option autoImplicit false
Formal statement
theorem mme_N2_occ_eq_one : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)) (r : Fin S.R), S.n r = 1 := by sorry
Source
Corollary of mme_N2_total_occurrences_eq_one with IntegerStep parent fields.