Courtade–Kumar proof module `CKLaneC.RSC2.S09_0027` (transplant)
DefinitionCK_CKLaneC_RSC2_S09_0027Verbatim transplant of the Lean module CKLaneC.RSC2.S09_0027 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.S09_0027 from release v1.0 (sources_v3.tar.zst).
import Definitions.Def_CK_CKLaneC_RSC2_S09_0027_part02 /-! RA-stat cover batch S09_0027 (generated by tools/emit_cover2.py; compact format). -/ namespace CKLaneC.RSC2.S09_0027 open CKLaneC.TM3 CKLaneC.RSCell theorem s0_7 : stageC0 w7 q7 = true := by decide +kernel theorem s1_7 : stageC1 w7 q7 = true := by decide +kernel theorem s2_7 : stageC2 w7 q7 = true := by decide +kernel theorem s3_7 : stageC3 w7 q7 = true := by decide +kernel theorem sE_7 : stageE w7 q7 = true := by decide +kernel theorem sF_7 : stageF w7 = true := by decide +kernel theorem ok_7 : (domOK c7 && cellCheck c7 q7) = true := staged_check c7 q7 w7 (by decide +kernel) sB_7 s0_7 s1_7 s2_7 s3_7 sE_7 sF_7 theorem region : RegionPosI 288230376151711744 360287970189639680 9223372036854775808 13835058055282163712 4611686018427387904 6917529027641081856 := (RegionPosI.split_s 5764607523034234880 (RegionPosI.split_b 324259173170675712 (RegionPosI.split_s 5188146770730811392 (RegionPosI.of_check c0 q0 ok_0 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 4611686018427387904 5188146770730811392 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 5188146770730811392 5764607523034234880 (by decide +kernel))) (RegionPosI.split_s 5188146770730811392 (RegionPosI.of_check c2 q2 ok_2 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 4611686018427387904 5188146770730811392 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 5188146770730811392 5764607523034234880 (by decide +kernel)))) (RegionPosI.split_b 324259173170675712 (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c4 q4 ok_4 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel))) (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c6 q6 ok_6 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel))))) end CKLaneC.RSC2.S09_0027