Courtade–Kumar proof module `CKLaneC.RSC2.BA_0094` (transplant)
DefinitionCK_CKLaneC_RSC2_BA_0094Verbatim transplant of the Lean module CKLaneC.RSC2.BA_0094 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.BA_0094 from release v1.0 (sources_v3.tar.zst).
import Definitions.Def_CK_CKLaneC_RSC2_BA_0094_part00 /-! RA-stat cover batch BA_0094 (generated by tools/emit_cover2.py; compact format). -/ namespace CKLaneC.RSC2.BA_0094 open CKLaneC.TM3 CKLaneC.RSCell theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel theorem sE_4 : stageE w4 q4 = true := by decide +kernel theorem sF_4 : stageF w4 = true := by decide +kernel theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true := staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4 theorem region : RegionPosI 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 2305843009213693952 4323455642275676160 := (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.split_s 2558044588346441728 (RegionPosI.of_check c0 q0 ok_0 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 2305843009213693952 2558044588346441728 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 2558044588346441728 2810246167479189504 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.split_s 3819052484010180608 (RegionPosI.of_check c3 q3 ok_3 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 3314649325744685056 3819052484010180608 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 2594073385365405696 2882303761517117440 9223372036854775808 10376293541461622784 3819052484010180608 4323455642275676160 (by decide +kernel)))) end CKLaneC.RSC2.BA_0094