Exact Z entropy arithmetic in orientation 0
Provedmme_released_global_yz_expression_data_0_1entropymatrix-multiplicationmore-asymmetrynumerical-certificate
The exact signed-log expression and rational floor inequality for branch 1 in orientation 0.
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_0_1 :
((entries (0 : Fin 6) (1 : Fin 2)).map Prod.fst = prune (rawTerms (0 : Fin 6) (1 : Fin 2))) ∧
(rateFloor (0 : Fin 6) ≤ totalBound (0 : Fin 6) (1 : Fin 2)) := 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.