Repair exponents are positive

Proved

mme_integer_step_repairExponent_pos

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer regional step has repair exponent at least one.

The exponent is defined as $\log_{repairScale}(capacity)+1$ , so positivity is immediate. This records the denominator $8^{exponent}\ge 8$ used by every copy-count estimate.

Formalization Note The proof unfolds the definition and closes by arithmetic.

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_step_repairExponent_pos : forall {ell M : Nat} {P : MME.ProfiledCW.Predicate M} (S : MME.RegionRealization.IntegerStep ell M P), 1 ≤ S.repairExponent := by sorry

Source

Definition of IntegerStep.repairExponent; supporting lemma for regional copy bounds, Alman et al., More Asymmetry, https://arxiv.org/html/2404.16349v2#S6.

View graph