Kernel-checked intervals for all 594 concrete global X-rate logarithms
Provedmme_released_global_x_log_intervalsentropymatrix-multiplicationmore-asymmetrynumerical-certificate
For every one of six orientations and 99 explicit positive rational inputs, the stored rational lower and upper endpoints bound the real logarithm of that input.
Preamble
import Definitions.Def_mme_released_global_x_certificate open BigOperators MME MME.ReleasedGlobal MME.ReleasedGlobalNumeric MME.MoreAsymmetryExactSeed MME.RegionRate MME.RecursiveThinSplit MME.GlobalCW open scoped Classical set_option autoImplicit false set_option maxRecDepth 3000
Formal statement
theorem mme_released_global_x_log_intervals (o : Fin 6) (j : Fin 99) :
(xLogLower o j : ℝ) ≤ Real.log (xInputs o j : ℝ) ∧
Real.log (xInputs o j : ℝ) ≤ (xLogUpper o j : ℝ) := by
sorry
Source
Numerical global X-rate certification for the exact ReleasedGlobal candidate from More Asymmetry, https://arxiv.org/html/2404.16349v2#S5 . Y/Z numerical rates and whole-interface recursive continuation remain separate.