The copy-count divisor is at least eight

Proved

mme_integer_step_eight_pow_repairExponent_ge

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer step's copy-count divisor is at least eight.

Since the repair exponent is at least one, $8^{exponent} \ge 8^1 = 8$ by power monotonicity. This makes the factor- $8$ loss in every copy estimate explicit.

Formalization Note This imports the proved positivity of the repair exponent.

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

Source

Consequence of mme_integer_step_repairExponent_pos.

View graph