One fixed tolerance controls the concrete global candidate at every scale
Provedmme_released_global_uniform_window_boundsmatrix-multiplicationmore-asymmetryquantitative-realization
For every positive entropy loss delta, choose one positive tolerance before choosing any scale. Every admissible profile in that window, at every positive integer scale and every valid repair scale, has entropy rate at least blocks times the exact central rate minus delta. Its entropy exponent is bounded by blocks times an explicit constant depending only on the central profile and delta.
Preamble
import Definitions.Def_mme_released_global_frame_data import Definitions.Def_mme_global_CW_joint_start_data open BigOperators MME MME.TensorObj MME.ProfiledCW MME.ReleasedGlobal MME.MoreAsymmetryExactSeed MME.GlobalCW MME.RegionRate MME.RecursiveYZ open scoped Classical set_option autoImplicit false set_option maxRecDepth 3000 universe u
Formal statement
theorem mme_released_global_uniform_window_bounds (owner : Fin 6) (delta : ℝ) (hdelta : 0 < delta) :
∃ eps : ℝ, 0 < eps ∧ ∀ (k : ℕ) (hk : 0 < k) (a : Reference owner k)
(d : ℕ) (hd : 1 < d) (mu : (frame owner k hk a).AdmissibleProfile),
(∀ i, windowGood owner k eps i (mu.val i)) →
(blocks k : ℝ)*((profile owner).rate (fun _ ↦ 1)-delta) ≤
((frame owner k hk a).stage mu d hd).entropyRate ∧
((frame owner k hk a).stage mu d hd).entropyExponent ≤
(blocks k : ℝ)*(massEntropy ((profile owner).1 0) -
(profile owner).rate (fun _ ↦ 1)+delta) := by
sorry
Source
Concrete global profile obligations for More Asymmetry Theorem 5.3, https://arxiv.org/html/2404.16349v2#S5 . This is an explicit rational candidate reconstructed from the released primitive seed; the numerical rate inequalities and whole-interface continuation remain separate obligations.