Courtade–Kumar proof module `CKLaneC.RSC2.S04_Top (subtrees t_053)` (transplant)
DefinitionCK_CKLaneC_RSC2_S04_Top_q00_t053Verbatim transplant of the Lean module CKLaneC.RSC2.S04_Top (subtrees t_053) 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_Top (subtrees t_053) from release v1.0 (sources_v3.tar.zst).
import Definitions.Def_CK_CKLaneC_RSCell_RegionI import Definitions.Def_CK_CKLaneC_RSC2_S04_Top_q00_t033 import Definitions.Def_CK_CKLaneC_RSC2_S04_Top_q00_t052 /-! RA-stat cover: subtree of the root assembly of CKLaneC.RSC2.S04_Top (split by rsc2tree.py; term verbatim). -/ namespace CKLaneC.RSC2.S04_Top open CKLaneC.RSCell theorem t_053 : RegionPosI 9007199254740992 18014398509481984 0 18446744073709551616 6917529027641081856 18446744073709551616 := (RegionPosI.split_s 9223372036854775808 CKLaneC.RSC2.S04_Top.t_033 CKLaneC.RSC2.S04_Top.t_052) end CKLaneC.RSC2.S04_Top