Uniformly small repair loss per fine coordinate

Proved

mme_profile_repair_scale_exists_uniform_coordinate_loss

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

regional-extractiontensor-complexity

For every positive eta, one repair scale greater than one makes the logarithmic repair budget at most log 8 plus eta times the number of fine coordinates, uniformly over all levels, finite position types, cell assignments, shapes and complete-word profiles.

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
import Definitions.Def_mme_recursive_yz_CW_cells
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.Positivity
open BigOperators MME MME.RecursiveYZ MME.RecursiveYZ.CWCells MME.CompleteSplit
open scoped Classical
set_option autoImplicit false
universe u

Formal statement

theorem mme_profile_repair_scale_exists_uniform_coordinate_loss
    (eta : ℝ) (heta : 0 < eta) :
    ∃ d : ℕ, 1 < d ∧ ∀ (ell : ℕ) (P C : Type*) [Fintype P]
      (cell : P → C) (shape : C → Fin 3 → ℕ)
      (mu : Fin 3 → C → CompleteWord ell → ℕ),
      Real.log ((8 : ℝ) ^ (Nat.log d
        (∏ i : Fin 3, Nat.card (Block ell cell shape mu i)) + 1)) ≤
        Real.log 8 + eta * (Fintype.card P * 2 ^ (ell - 1) : ℕ) := by sorry

Source

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

View graph