Courtade–Kumar proof module `CKLaneM07.CE.Row4 (subtrees cells)` (transplant)

Definition

CK_CKLaneM07_CE_Row4_q00_q00_q00_q00_q00_l08

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

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneM07.CE.Row4 (subtrees cells) 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 CKLaneM07.CE.Row4 (subtrees cells) from release v1.0 (sources_v3.tar.zst).

Definition code

import Definitions.Def_CK_CKLaneM07_CE_Cells_C0256
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0257
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0258
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0259
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0260
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0261
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0262
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0263
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0264
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0265
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0266
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0267
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0268
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0269
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0270
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0271
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0272
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0273
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0274
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0275
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0276
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0277
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0278
import Definitions.Def_CK_CKLaneM07_CE_Cells_C0279

set_option autoImplicit false
set_option maxRecDepth 100000

/-! Sub-list 8 of `CKLaneM07.CE.Row4.cells` (split by split_listdef.py; elements verbatim, in order). -/

namespace CKLaneM07.CE.Row4

def cells_l08 : List CellV :=
  [CKLaneM07.CE.Cells.C0256.cl,
   CKLaneM07.CE.Cells.C0257.cl,
   CKLaneM07.CE.Cells.C0258.cl,
   CKLaneM07.CE.Cells.C0259.cl,
   CKLaneM07.CE.Cells.C0260.cl,
   CKLaneM07.CE.Cells.C0261.cl,
   CKLaneM07.CE.Cells.C0262.cl,
   CKLaneM07.CE.Cells.C0263.cl,
   CKLaneM07.CE.Cells.C0264.cl,
   CKLaneM07.CE.Cells.C0265.cl,
   CKLaneM07.CE.Cells.C0266.cl,
   CKLaneM07.CE.Cells.C0267.cl,
   CKLaneM07.CE.Cells.C0268.cl,
   CKLaneM07.CE.Cells.C0269.cl,
   CKLaneM07.CE.Cells.C0270.cl,
   CKLaneM07.CE.Cells.C0271.cl,
   CKLaneM07.CE.Cells.C0272.cl,
   CKLaneM07.CE.Cells.C0273.cl,
   CKLaneM07.CE.Cells.C0274.cl,
   CKLaneM07.CE.Cells.C0275.cl,
   CKLaneM07.CE.Cells.C0276.cl,
   CKLaneM07.CE.Cells.C0277.cl,
   CKLaneM07.CE.Cells.C0278.cl,
   CKLaneM07.CE.Cells.C0279.cl]

end CKLaneM07.CE.Row4

Source

arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneM07.CE.Row4 (subtrees cells) (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneM07/CE/Row4 (subtrees cells).lean)

View graph