Prove2Me

Correction minors positive on u∈[11/40,3/10]u\in[11/40,3/10], ρ∈[3/20,23/40]\rho\in[3/20,23/40] (directC3)

Proved
GeneralCK.CKFast.Band.minors_pos_u230686720_251658240_r125829120_482344960

by tianyipeng · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

certificatescorrection-bandgeneral-courtade-kumar

Positivity of both correction-Hessian minors on the parameter box

u∈[11/40,3/10],ρ∈[3/20,23/40],ρ<1,u\in[11/40,3/10],\qquad \rho\in[3/20,23/40],\qquad \rho<1,

namely, with w=u+ρ(1/2−u)w=u+\rho(1/2-u) and HH the binary entropy in bits,

0<Mleft(H(u),H(w))and0<Mdet⁡(H(u),H(w)).0<M_{\mathrm{left}}\big(H(u),H(w)\big)\quad\text{and}\quad 0<M_{\det}\big(H(u),H(w)\big).

This box is one piece of the correction band directC3 of the general Courtade–Kumar proof, the input directC3, which is ActualRatioFamilyOn (1/5) (3/10) (3/20) 1. The band pieces assemble into that input.

The statement has exactly the shape of the source's per-cell certificates actual_minors_positive (Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff, A Proof of the Most Informative Boolean Function Conjecture, arXiv:2609.24931, 2026; https://github.com/dpwoodru/general-courtade-kumar-lean). It is proved here by the computing checker GeneralCK.CKFast.tree_sound, over 4683 kernel-checked cells.

Preamble
import Definitions.Def_GeneralCK_CKFast_eval
import Definitions.Def_GeneralCK_correction_minors
Formal statement
theorem GeneralCK.CKFast.Band.minors_pos_u230686720_251658240_r125829120_482344960 : ∀ u rho : ℝ, u ∈ Set.Icc (11/40 : ℝ) (3/10 : ℝ) →
    rho ∈ Set.Icc (3/20 : ℝ) (23/40 : ℝ) → rho < 1 →
      0 < GeneralCK.Correction.Mleft (GeneralCK.H u) (GeneralCK.H (u + rho * (1 / 2 - u))) ∧
      0 < GeneralCK.Correction.Mdet (GeneralCK.H u) (GeneralCK.H (u + rho * (1 / 2 - u))) := by sorry
Source
Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff, A Proof of the Most Informative Boolean Function Conjecture, arXiv:2609.24931 (2026); band statement: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneA5/Bands.lean

View graph