A hash log gap guarantees positive repaired copies

Proved

mme_exact_step_hash_log_gap_positive_copies

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

regional-extractiontensor-complexity

For an exact step whose selected count dominates A exp(-4 sqrt(log Q))/(32 Q), an explicit logarithmic gap covering the repair cost and log 32 plus log 2 guarantees positive repaired copies and a strict lower bound on their logarithm. Positivity of A and Q and the log-gap hypothesis are required.

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.Ring
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_hash_log_gap_positive_copies
    {ell N : ℕ} {P : Predicate N} (E : ExactStep ell N P)
    (A Q : ℝ) (hA : 0 < A) (hQ : 0 < Q)
    (hcount : A * Real.exp (-4 * Real.sqrt (Real.log Q)) / (32 * Q) ≤ E.count)
    (hgap : Real.log 32 + Real.log 2 +
      (E.stage.repairExponent : ℝ) * Real.log 8 ≤
      Real.log A - Real.log Q - 4 * Real.sqrt (Real.log Q)) :
    0 < E.copies ∧ Real.log A - Real.log Q - 4 * Real.sqrt (Real.log Q) -
      (E.stage.repairExponent : ℝ) * Real.log 8 - Real.log 32 - Real.log 2 <
        Real.log E.copies := by sorry

Source

Selected-count logarithms and uniformly controlled repair for the concrete released regional extraction.

View graph