Joint copy-count bounds package

Proved

mme_integer_step_copy_bounds_package

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

matrix-multiplicationmore-asymmetryregional-entropy

Every integer step satisfies both copy-count bounds jointly.

The guaranteed copies are bounded above by the floored lower estimate, while the divisor is bounded below by eight. Together they fix the two-sided scaffolding every numeric copy lower bound must use.

Formalization Note This conjoins the two already proved bounds.

Preamble

import Definitions.Def_mme_regional_entropy_copy_bound
import Definitions.Def_mme_recursive_profiled_CW_data
set_option autoImplicit false

Formal statement

theorem mme_integer_step_copy_bounds_package : forall {ell M : Nat} {P : MME.ProfiledCW.Predicate M} (S : MME.RegionRealization.IntegerStep ell M P), S.entropyCopies ≤ ⌊S.entropyLower⌋₊ ∧ 8 ≤ 8 ^ S.repairExponent := by sorry

Source

Conjunction of mme_integer_step_entropyCopies_le_floor and mme_integer_step_eight_pow_repairExponent_ge.

View graph