Exact Y entropy arithmetic in orientation 5

Proved

mme_released_global_yz_expression_data_5_0

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

entropymatrix-multiplicationmore-asymmetrynumerical-certificate

The exact signed-log expression and rational floor inequality for branch 0 in orientation 5.

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_5_0 :
    ((entries (5 : Fin 6) (0 : Fin 2)).map Prod.fst = prune (rawTerms (5 : Fin 6) (0 : Fin 2))) ∧
    (rateFloor (5 : Fin 6) ≤ totalBound (5 : Fin 6) (0 : 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.

View graph