Courtade–Kumar proof module `CKLaneC.RSC2.S05_0004` (transplant)

Definition

CK_CKLaneC_RSC2_S05_0004

by tianyipeng · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneC.RSC2.S05_0004 of the machine-checked proof of the general Courtade–Kumar theorem (the most informative Boolean function conjecture), so that the complete proof can be verified on this platform.

It is the original source with only two mechanical changes. Imports of project modules are redirected to their transplanted bundles Definitions.Def_CK_*. Declarations that already exist in earlier platform definition bundles of this mission are removed, and those bundles are imported instead, so every constant keeps a single platform identity.

The module contains both definitions and the lemmas proved alongside them in the source. They are kept together so the transplant stays faithful and every proof is re-checked by the server.

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). Lean development: https://github.com/dpwoodru/general-courtade-kumar-lean (Apache-2.0), module CKLaneC.RSC2.S05_0004 from release v1.0 (sources_v3.tar.zst).

Definition code

import Definitions.Def_CK_CKLaneC_RSC2_S05_0004_part02

/-! RA-stat cover batch S05_0004 (generated by tools/emit_cover2.py; compact format). -/

namespace CKLaneC.RSC2.S05_0004
open CKLaneC.TM3 CKLaneC.RSCell

theorem region : RegionPosI 27021597764222976 36028797018963968 0 4611686018427387904 2882303761517117440 3458764513820540928 :=
  (RegionPosI.split_b 31525197391593472 (RegionPosI.split_s 3170534137668829184 (RegionPosI.split_b 29273397577908224 (RegionPosI.of_check c0 q0 ok_0 27021597764222976 29273397577908224 0 4611686018427387904 2882303761517117440 3170534137668829184 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 29273397577908224 31525197391593472 0 4611686018427387904 2882303761517117440 3170534137668829184 (by decide +kernel))) (RegionPosI.split_b 29273397577908224 (RegionPosI.of_check c2 q2 ok_2 27021597764222976 29273397577908224 0 4611686018427387904 3170534137668829184 3458764513820540928 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 29273397577908224 31525197391593472 0 4611686018427387904 3170534137668829184 3458764513820540928 (by decide +kernel)))) (RegionPosI.split_s 3170534137668829184 (RegionPosI.of_check c4 q4 ok_4 31525197391593472 36028797018963968 0 4611686018427387904 2882303761517117440 3170534137668829184 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 31525197391593472 36028797018963968 0 4611686018427387904 3170534137668829184 3458764513820540928 (by decide +kernel))))

end CKLaneC.RSC2.S05_0004

Source

arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneC.RSC2.S05_0004 (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneC/RSC2/S05_0004.lean)

View graph