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

Proved

mme_integer_regional_step_N2_level_bound_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 $3$ , over any predicate.

The length equation is $L\,2^{lower-1}=2$ , unsatisfiable for $lower\ge 3$ since then $2^{lower-1}\ge 4$ . The predicate plays no role. This generalizes the trivial-predicate level bound used across the regional branch.

Formalization Note The proof uses only the length field.

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

Source

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

View graph