Correction matrix positivity on the first RB2 cell

Proved

GeneralCK.Certificates.LaneCB.RB2Cell000000.actual_minors_positive

by marwahaha · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

general-courtade-kumarinterval-arithmeticrb2soundness

For $1/10\le u\le257/2560$ and $1/10\le\rho\le53/512$ , with $\rho<1$ , put $w=u+\rho(1/2-u)$ . The correction matrix at entropy coordinates $(H(u),H(w))$ has strictly positive first diagonal entry $M_{\rm left}$ and determinant $M_{\rm det}$ .

Preamble

import Definitions.Def_GeneralCK_correction_minors
import Definitions.Def_GeneralCK_statement

open Set
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxRecDepth 10000
set_option maxHeartbeats 4000000

Formal statement

theorem GeneralCK.Certificates.LaneCB.RB2Cell000000.actual_minors_positive {u rho : ℝ} (hu : u∈Icc (1/10:ℝ) (257/2560))
    (hr : rho∈Icc (1/10:ℝ) (53/512)) (hr1 : rho < 1) :
    0 < _root_.GeneralCK.Correction.Mleft (_root_.GeneralCK.H u) (_root_.GeneralCK.H (u+rho*(1/2-u))) ∧
    0 < _root_.GeneralCK.Correction.Mdet (_root_.GeneralCK.H u) (_root_.GeneralCK.H (u+rho*(1/2-u))) := by sorry

Source

https://github.com/dpwoodru/general-courtade-kumar-lean/releases/tag/v1.0

View graph