Exact rational expressions and floor comparisons for global Y/Z
Provedmme_released_global_yz_expression_dataentropymatrix-multiplicationmore-asymmetrynumerical-certificate
The 3822 signed log terms equal the pruned rational mass-entropy expressions, and both branch bounds exceed the existing six floors.
Preamble
import Definitions.Def_mme_released_global_yz_certificate 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.ReleasedGlobalNumeric MME.ReleasedGlobalYZ MME.MoreAsymmetryExactSeed MME.RegionRate MME.RecursiveThinSplit MME.GlobalCW MME.RecursiveYZ open scoped Classical set_option autoImplicit false set_option maxRecDepth 3000 universe u
Formal statement
theorem mme_released_global_yz_expression_data :
(∀ o i, (entries o i).map Prod.fst = prune (rawTerms o i)) ∧
(∀ o i, rateFloor o ≤ totalBound o i) := by
sorry
Source
Numerical global rate of the exact published More Asymmetry candidate. This closes the Y/Z branches and full global rate; whole-interface recursive continuation and the final finite witness remain separate.