N=2 integer steps live below level 2
Provedmme_entropy_regional_step_N2_lt_twomatrix-multiplicationmore-asymmetryregional-entropy
Every integer regional step with two elementary positions lives below level .
The length equation already forces , and level itself is impossible: at level the length equation gives while physical positions contain both halves of every parent occurrence. Hence only levels and carry content at .
Formalization Note This combines the level bound with the level-two impossibility, both already proved nodes in the same environment.
Preamble
import Definitions.Def_mme_integer_regional_CW_recipe set_option autoImplicit false
Formal statement
theorem mme_entropy_regional_step_N2_lt_two : forall (lower : Nat) (S : MME.RegionRealization.IntegerStep lower 2 (fun _ _ => True)), lower < 2 := by sorry
Source
Consequence of mme_integer_regional_step_N2_level_bound and mme_entropy_regional_step_L2_N2_impossible; sizing for Alman et al., More Asymmetry, https://arxiv.org/html/2404.16349v2#S6, Section 6.