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

Definition

CK_CKLaneC_RSC2_S03_0109

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

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneC.RSC2.S03_0109 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.S03_0109 from release v1.0 (sources_v3.tar.zst).

Definition code

import Definitions.Def_CK_CKLaneC_RSC2_S03_0109_part01

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

namespace CKLaneC.RSC2.S03_0109
open CKLaneC.TM3 CKLaneC.RSCell

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 6755399441055744 7881299347898368 0 4611686018427387904 6917529027641081856 9223372036854775808 :=
  (RegionPosI.split_s 8070450532247928832 (RegionPosI.split_b 7318349394477056 (RegionPosI.split_s 7493989779944505344 (RegionPosI.of_check c0 q0 ok_0 6755399441055744 7318349394477056 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 6755399441055744 7318349394477056 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel))) (RegionPosI.split_s 7493989779944505344 (RegionPosI.of_check c2 q2 ok_2 7318349394477056 7881299347898368 0 4611686018427387904 6917529027641081856 7493989779944505344 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 7318349394477056 7881299347898368 0 4611686018427387904 7493989779944505344 8070450532247928832 (by decide +kernel)))) (RegionPosI.split_b 7318349394477056 (RegionPosI.split_s 8646911284551352320 (RegionPosI.of_check c4 q4 ok_4 6755399441055744 7318349394477056 0 4611686018427387904 8070450532247928832 8646911284551352320 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 6755399441055744 7318349394477056 0 4611686018427387904 8646911284551352320 9223372036854775808 (by decide +kernel))) (RegionPosI.split_s 8646911284551352320 (RegionPosI.of_check c6 q6 ok_6 7318349394477056 7881299347898368 0 4611686018427387904 8070450532247928832 8646911284551352320 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 7318349394477056 7881299347898368 0 4611686018427387904 8646911284551352320 9223372036854775808 (by decide +kernel)))))

end CKLaneC.RSC2.S03_0109

Source

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

View graph