Uniform repair loss for replicated released profiles

Proved

mme_released_116_uniform_repair_coordinate_loss

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

regional-extractiontensor-complexity

For every positive eta there is one repair scale greater than one for which every replication size and every reference address of the released (1,1,6) integer profiles has log repair budget at most log 8 plus eta times its exact physical fine-coordinate count.

Preamble

import Theorems.Thm_mme_released_116_regional_total
import Definitions.Def_mme_released_116_integer_profiles
import Mathlib.Data.Fintype.Sigma
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
open MME.Released116 MME.MoreAsymmetryExactSeed
set_option autoImplicit false
universe u

Formal statement

theorem mme_released_116_uniform_repair_coordinate_loss (eta : ℝ) (heta : 0 < eta) :
    ∃ d : ℕ, 1 < d ∧ ∀ (k : ℕ)
      (reference : MME.RecursiveXHash.Address 4 6 parent
        (fun r => k * regionalSize r)),
      Real.log ((8 : ℝ) ^ (Nat.log d
        (∏ i : Fin 3, Nat.card (Block 2 (fullCell parent_total reference)
          (fun c i => (c.2.val i).val) (fun i c w => k * integerProfile i c w) i)) + 1)) ≤
        Real.log 8 + eta * (4 * (k * denominator ^ 4) : ℕ) := by sorry

Source

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

View graph