Level-two N=2 integer steps are impossible over any predicate

Proved

mme_entropy_regional_step_L2_anyP_impossible

by Tamas Fulop · Sep 18, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

matrix-multiplicationmore-asymmetryregional-entropy

At level $2$ with two elementary positions, no integer regional step exists over any predicate.

The length equation gives $L=1$ while one parent occurrence supplies two distinct physical positions, so the position equivalence cannot exist. The predicate plays no role. This generalizes the trivial-predicate impossibility and closes the level-two case for every $P$ at $N=2$ .

Formalization Note The proof uses only the length and position fields.

Preamble

import Definitions.Def_mme_integer_regional_CW_recipe
import Definitions.Def_mme_recursive_profiled_CW_data
set_option autoImplicit false

Formal statement

theorem mme_entropy_regional_step_L2_anyP_impossible : forall (P : MME.ProfiledCW.Predicate 2) (S : MME.RegionRealization.IntegerStep 2 2 P), False := by sorry

Source

Generalization of mme_entropy_regional_step_L2_N2_impossible; sizing for Alman et al., More Asymmetry, https://arxiv.org/html/2404.16349v2#S6, Section 6.

View graph