Choose a uniformly small logarithmic repair loss

Proved

mme_repair_scale_exists_uniform_log_loss

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

regional-extractiontensor-complexity

For every positive delta there exists one natural repair scale greater than one such that, uniformly over all natural capacities C, the logarithmic repair budget is at most log 8 plus delta times log C.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
set_option autoImplicit false
universe u

Formal statement

theorem mme_repair_scale_exists_uniform_log_loss (delta : ℝ) (hdelta : 0 < delta) :
    ∃ d : ℕ, 1 < d ∧ ∀ C : ℕ,
      Real.log ((8 : ℝ) ^ (Nat.log d C + 1)) ≤ Real.log 8 + delta * Real.log C := by sorry

Source

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

View graph