Positive surviving copies with an explicit logarithmic rate

Proved

mme_exact_step_positive_copies_log_lower_bound

by Robertboy18 · Sep 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

regional-extractiontensor-complexity

If a real lower bound B for the selected count is at least twice the power-of-eight repair budget, the exact step has positive surviving copies. Their log count is strictly greater than log B minus the repair exponent times log 8 minus log 2. Both the positivity threshold and the rounding allowance are explicit.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Theorems.Thm_mme_recursive_profiled_CW_exact_step
import Definitions.Def_mme_recursive_profiled_CW_data
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
open MME MME.ProfiledCW
set_option autoImplicit false
universe u

Formal statement

theorem mme_exact_step_positive_copies_log_lower_bound
    {ell N : ℕ} {P : Predicate N} (E : ExactStep ell N P) {B : ℝ}
    (hB : B ≤ E.count) (hlarge : 2 * (8 : ℝ) ^ E.stage.repairExponent ≤ B) :
    0 < E.copies ∧ Real.log B -
      (E.stage.repairExponent : ℝ) * Real.log 8 - Real.log 2 < Real.log E.copies := by sorry

Source

Natural logarithm repair budgets, finite profile capacities, and exact-step copy rounding.

View graph