Level-one N=2 steps exist
Provedmme_N2_step_inhabited_L1matrix-multiplicationmore-asymmetryregional-entropy
There exists an integer regional step at level with two elementary positions.
The skeleton is forced (, , , , parent ) and completed with a delta mass at one split, grade-matching delta profiles, and a large tolerance. This is the base point every copy-bound argument at must start from.
Formalization Note Explicit instance; the predicate is trivial so the source obligation is immediate.
Preamble
import Definitions.Def_mme_integer_regional_CW_recipe set_option autoImplicit false
Formal statement
theorem mme_N2_step_inhabited_L1 : exists (S : MME.RegionRealization.IntegerStep 1 2 (fun _ _ => True)), True := by sorry
Source
Explicit instance for Alman et al., More Asymmetry, https://arxiv.org/html/2404.16349v2#S6, Section 6 skeleton at N=2.