Compute concrete global marginals directly from the sparse supported table
Provedmme_released_global_sparse_marginalsmatrix-multiplicationmore-asymmetryquantitative-realization
Every marginal word count equals its coarse alpha weight times the sparse joint table summed only over atoms with the requested mode word. This exact Lean identity avoids enumerating the full 81 cubed joint-word alphabet when certifying the numerical profile.
Preamble
import Definitions.Def_mme_released_global_profile_data open BigOperators MME MME.ReleasedGlobal open scoped Classical set_option autoImplicit false set_option maxHeartbeats 1000000 set_option maxRecDepth 3000 set_option backward.isDefEq.respectTransparency false
Formal statement
theorem mme_released_global_sparse_marginals (owner : Fin 6) (c : Shape) (i : Fin 3) (w : Word) :
wordCounts owner i c w = alpha owner (shapeEquiv.symm c) *
((jointRows owner (shapeEquiv.symm c)).map
(fun a ↦ if atom a.1 i = w then a.2 else 0)).sum := 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.