All finite global extraction losses fit any positive entropy gap

Proved

mme_global_CW_canonical_cofinal_entropy_bound

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

matrix-multiplicationmore-asymmetryquantitative-realization

Fix bounds on elementary size, degree and histogram dimensions, and an upper bound B k^2 for the entropy exponent. If the pooled global entropy is at least E k^2, then for every rho<E all sufficiently large k make the canonical stage certify at least rho k^2 logarithmic copies. All polynomial, square-root, hash and repair costs are included.

Preamble

import Definitions.Def_mme_global_CW_histogram_frame
import Definitions.Def_mme_global_CW_entropy_data
import Definitions.Def_mme_global_CW_joint_start_data
open BigOperators MME MME.TensorObj MME.ProfiledCW MME.RegionRate MME.RecursiveYZ MME.GlobalCW MME.CompleteSplit
open scoped Classical
set_option autoImplicit false
universe u

Formal statement

theorem mme_global_CW_canonical_cofinal_entropy_bound (C H d : ℕ) (B E rho : ℝ)
    (hB : 0 ≤ B) (hgap : rho < E) :
    ∃ k0 : ℕ, ∀ k : ℕ, k0 ≤ k → ∃ hk : 1 < k,
      ∀ {ell M : ℕ} (D : HistogramFrame ell M) (mu : D.AdmissibleProfile),
      M ≤ C * k ^ 2 → D.degree ≤ H →
      Fintype.card (Cell D.degree D.R D.bounds) ≤ d →
      D.R * (D.degree+1) ≤ d →
      D.R * (D.degree+1) * Fintype.card (CompleteSplit.CompleteWord ell) ≤ d →
      E * (k : ℝ) ^ 2 ≤ (D.stage mu k hk).entropyRate →
      (D.stage mu k hk).entropyExponent ≤ B * (k : ℝ) ^ 2 →
      rho * (k : ℝ) ^ 2 ≤ (D.stage mu k hk).certifiedLogCopies := by
  sorry

Source

Finite global realization for More Asymmetry Theorem 5.3, https://arxiv.org/html/2404.16349v2#S5 . This constructs the global window extraction needed by the joint finite-witness architecture; released profile and numerical instantiation remain open.

View graph