Exact Y/Z entropy expression data in orientation 4
Provedmme_released_global_yz_expression_data_4entropymatrix-multiplicationmore-asymmetrynumerical-certificate
For orientation 4, the certificate terms equal the actual rational mass-entropy expressions and their rational bounds exceed the existing numerical floor.
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_4 :
(∀ i, (entries (4 : Fin 6) i).map Prod.fst = prune (rawTerms (4 : Fin 6) i)) ∧
(∀ i, rateFloor (4 : Fin 6) ≤ totalBound (4 : Fin 6) 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.