N=2 integer steps live below level 2 over any predicate

Proved

mme_entropy_regional_step_N2_lt_two_anyP

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer regional step with two elementary positions lives below level $2$ , over any predicate.

The length equation forces $lower < 3$ , and level $2$ itself is empty at $N=2$ . Hence only levels $0$ and $1$ carry content, uniformly in the predicate.

Formalization Note This combines the arbitrary-predicate level bound with the arbitrary-predicate level-two impossibility.

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_N2_lt_two_anyP : forall (lower : Nat) (P : MME.ProfiledCW.Predicate 2) (S : MME.RegionRealization.IntegerStep lower 2 P), lower < 2 := by sorry

Source

Consequence of mme_integer_regional_step_N2_level_bound_anyP and mme_entropy_regional_step_L2_anyP_impossible.

View graph