Normalize the concrete global candidate at every integer scale

Proved

mme_released_global_profile_normalization

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

matrix-multiplicationmore-asymmetryquantitative-realization

The concrete real profile has nonnegative normalized coarse masses and consistent nonnegative cell-word marginals. Scaling integer counts by any natural k agrees exactly with scaling the real profile by 10^60 k.

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_profile_normalization (owner : Fin 6) :
    (∀ r c, 0 ≤ (profile owner).1 r c) ∧
    (∀ r, ∑ c, (profile owner).1 r c = 1) ∧
    (∀ i c w, 0 ≤ (profile owner).2 i c w) ∧
    (∀ i c, ∑ w, (profile owner).2 i c w = (profile owner).1 c.1 c.2) ∧
    (∀ (k : ℕ) (r : Fin 1) (c : Shape),
      (counts owner k r c : ℝ) = (blocks k : ℝ)*(profile owner).1 r c) ∧
    (∀ (k : ℕ) (i : Fin 3) (c : Cell 8 1 (fun _ _ ↦ 8)) (w : Word),
      (scaledWords owner k i c w : ℝ) = (blocks k : ℝ)*(profile owner).2 i c w) := 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.

View graph