Exact terms certificate for orientation 0, branch 0

Proved

mme_released_global_yz_expression_terms_0_0

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

entropymatrix-multiplicationmore-asymmetrynumerical-certificate

The stored signed logarithm terms equal the pruned exact rational entropy expression.

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_terms_0_0 :
    (entries (0 : Fin 6) (0 : Fin 2)).map Prod.fst =
      prune (rawTerms (0 : 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