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

Definition

CK_CKLaneC_RSC2_S04_0113

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

general-courtade-kumartransplant

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

Definition code

import Definitions.Def_CK_CKLaneC_RSC2_S04_0113_part00

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

namespace CKLaneC.RSC2.S04_0113
open CKLaneC.TM3 CKLaneC.RSCell

theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

theorem region : RegionPosI 9007199254740992 10133099161583616 4611686018427387904 9223372036854775808 9223372036854775808 11529215046068469760 :=
  (RegionPosI.split_s 10376293541461622784 (RegionPosI.split_b 9570149208162304 (RegionPosI.split_s 9799832789158199296 (RegionPosI.of_check c0 q0 ok_0 9007199254740992 9570149208162304 4611686018427387904 9223372036854775808 9223372036854775808 9799832789158199296 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 9007199254740992 9570149208162304 4611686018427387904 9223372036854775808 9799832789158199296 10376293541461622784 (by decide +kernel))) (RegionPosI.split_s 9799832789158199296 (RegionPosI.of_check c2 q2 ok_2 9570149208162304 10133099161583616 4611686018427387904 9223372036854775808 9223372036854775808 9799832789158199296 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 9570149208162304 10133099161583616 4611686018427387904 9223372036854775808 9799832789158199296 10376293541461622784 (by decide +kernel)))) (RegionPosI.split_b 9570149208162304 (RegionPosI.of_check c4 q4 ok_4 9007199254740992 9570149208162304 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 9570149208162304 10133099161583616 4611686018427387904 9223372036854775808 10376293541461622784 11529215046068469760 (by decide +kernel))))

end CKLaneC.RSC2.S04_0113

Source

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

View graph