Courtade–Kumar proof module `CKLaneM07.FleetT.T0030 (+2 modules: CKLaneM07.FleetT.T0031, CKLaneM07.FleetT.T0032)` (transplant)
DefinitionCK_CKLaneM07_FleetT_T0030__3general-courtade-kumartransplant
Verbatim transplant of the Lean module CKLaneM07.FleetT.T0030 (+2 modules: CKLaneM07.FleetT.T0031, CKLaneM07.FleetT.T0032) 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.FleetT.T0030 (+2 modules: CKLaneM07.FleetT.T0031, CKLaneM07.FleetT.T0032) from release v1.0 (sources_v3.tar.zst).
Definition code
import Definitions.Def_CK_CKLaneM07_Checker -- ===== source module CKLaneM07.FleetT.T0030 ===== section /-! M07 derivative leaves (archived same-side owner `derivative`), shard `FleetT.T0030`. Witnesses only propose rationals; `checkLeaf` recomputes every enclosure. -/ set_option maxRecDepth 100000 namespace CKLaneM07.FleetT.T0030 open CKLaneM07 def L : List (List ℕ × Wit) := [ ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,0,3,4,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (28053356072523435) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,0,3,5,0], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (941197730216235) 51⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,0,3,5,1], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (30039254035252185) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (28255971822369703) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (28173467939121941) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (28215303733544865) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (28131317627718993) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,5,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (30167002884961185) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,5,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (7525224640412793) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (30084541694276059) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,2,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (7504089765953213) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (14046364036742407) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (28013672905388713) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (28049085920340157) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27968529346312351) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,5,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (30036050024455731) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,5,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (29972399189594457) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (14974715170047825) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,2,5,1,3,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29883697180822135) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,0,2], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (25020140374080863) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,0,3], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (24923731802957181) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,2,4,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (25057825053793401) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,2,4,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (3132595066796311) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,2,5,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (3214260780177969) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,2,5,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (25712858232265969) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,3,4,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (24961122367567919) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,3,4,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (24963616616987123) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,3,5,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (25622510809159077) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,4,1,3,5,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (25620793628859515) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,5,0,2], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (13196787604528117) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,5,0,3], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (26307912476721525) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,5,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (13191827205573659) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,2,5,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (13148455651959845) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,0,2], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (12414724975982167) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,0,3], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (24737210906344651) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,2,4,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (24866529283895971) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,2,4,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (12434286926383447) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,2,5,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (12766454279674125) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,2,5,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (25530694284927227) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,3,4,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (12386981180498373) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,3,4,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (12387774479362691) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,3,5,0], ⟨dy (763946912295928047) 60, dy (780675171398325421) 60, dy (58488257235927637) 58, dy (25445201273269861) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,4,1,3,5,1], ⟨dy (373788552645478855) 59, dy (47746682018495503) 56, dy (245898772200819105) 60, dy (25442482113060555) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,5,0,2], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (26224090907967397) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,5,0,3], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (13071018749686829) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,5,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (26211994112214569) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,0,3,5,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (13064415023820905) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,4,0,2], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (25116516119474425) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,4,0,3], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (25066880086773111) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,4,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (25117476228344857) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,4,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (12533803702443611) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,5,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (12855135465196887) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,2,5,1], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (6426593337803027) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,4,0,2], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (12508894972194955) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,4,0,3], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (3121154297035841) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,4,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (6254570625453673) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,4,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (12484745110923197) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,5,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (25617702757396231) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,5,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (6416192150990211) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,0,3,5,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (12809223861504411) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,2,4,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (25117221696747075) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,2,4,0,3], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (1566694626548569) 52⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,3,4,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (12508774187592893) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,3,4,0,3], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (12484256734242165) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,3,5,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (12829881695283639) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,4,1,3,5,0,3], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (12806587263780049) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,2,4,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (26404411627084415) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,2,4,1], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (412431768491119) 50⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,2,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (27116142418823619) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,3,4,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (26317226803246921) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,3,4,1], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (3288484025756565) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,0,3,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (27034001547258377) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,2,4,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (26385557398939505) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,2,5,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (13562606182789833) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,2,5,1], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (13554026670624225) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,3,4,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (6574301748679387) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,3,5,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (13521260398930179) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,2,5,1,3,5,1], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (6756171724025253) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,4,0,2], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (12460601222612879) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,4,0,3], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (6218420893854425) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,4,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (24921219645656281) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,4,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (12436730107279697) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,5,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (6381773049705803) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,5,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (12786307440074595) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,2,5,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (25527260168753785) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,4,0,2], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (1551666721010687) 52⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,4,0,3], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (24780144426474167) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,4,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (24826201714199183) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,4,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (24779434259163607) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,5,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (12719180645872689) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,5,1,2], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (25482374004908037) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,0,3,5,1,3], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (25437947112991107) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,2,4,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (24919998402331311) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,2,5,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (199742749833993) 49⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,2,5,0,3], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (25521445850195133) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,2,5,1,2], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (12780153620500761) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,2,5,1,3], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (3189300499088399) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,3,5,0,2], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (25476286570040929) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,3,5,0,3], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (12715792437069921) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,3,5,1,2], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (25468965964104001) 56⟩) ] theorem L_check : (L.all fun x => checkLeaf x.1 x.2) = true := by decide +kernel theorem L_sound : ∀ x ∈ L, SemSBox (ssBox x.1) := checkLeaves_sound L L_check end CKLaneM07.FleetT.T0030 end -- ===== source module CKLaneM07.FleetT.T0031 ===== section /-! M07 derivative leaves (archived same-side owner `derivative`), shard `FleetT.T0031`. Witnesses only propose rationals; `checkLeaf` recomputes every enclosure. -/ set_option maxRecDepth 100000 namespace CKLaneM07.FleetT.T0031 open CKLaneM07 def L : List (List ℕ × Wit) := [ ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,4,1,3,5,1,3], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (6355995975433153) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,2,4,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (6557963477807647) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,2,4,1], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (26221916411923661) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,2,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (26953513969581283) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,3,4,0], ⟨dy (731558069494126209) 60, dy (747577105290957711) 60, dy (64447364178546111) 58, dy (13074110258320855) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,3,4,1], ⟨dy (357941144300882061) 59, dy (365779034747063105) 59, dy (67405673126292001) 58, dy (26137693454388271) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,0,3,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (3359326631679073) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,2,4,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (13105327659254585) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,2,5,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (26961470794286681) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,2,5,1], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (26942956616461121) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,3,4,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (26125830104810101) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,3,5,0], ⟨dy (700542407369090387) 60, dy (715882288601764123) 60, dy (70349034862515925) 58, dy (3360249500154347) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,4,1,3,5,1,3,5,1], ⟨dy (342765614079526219) 59, dy (175135601842272597) 58, dy (73276877228996737) 58, dy (26862796189523635) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,2,4,0], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (13964790181816637) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,2,4,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (13988681983377435) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,2,4,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (6975731221203911) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,2,5,0], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (30002728982947343) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,2,5,1], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (14959897831001233) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,3,4,0], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (3473518056430965) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,3,4,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (27829974559415007) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,3,4,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (6939613218733833) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,3,5,0], ⟨dy (195168792849581355) 58, dy (815238614083298889) 60, dy (221954665051359627) 60, dy (29891335256510397) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,0,3,5,1], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (29804510386485111) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (6984057163154523) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (27860326546168649) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27889574165866275) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27812151641396957) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,5,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (29909891991351187) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,5,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (29848478002229973) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (14909552635805103) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,2,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29755603945640789) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (1736618897961759) 52⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (27712896038260263) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (6934049393967709) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (13830825952098155) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,5,0], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (29710753837122523) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29693145847896643) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,0,3,5,1,3,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (3703960829723297) 53⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,2,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (29997364566049871) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,2,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (29927061668771561) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,2,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30975370112727359) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,3,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (29858012683856933) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,3,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14895079487470447) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,3,5,1,2,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30912233647561279) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,2,5,0,3,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (15424995368391457) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,2,4,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (27885485471210775) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,2,4,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (27858771131110909) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,3,4,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (27807383680932037) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,3,4,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (27779881003558163) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,3,5,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (28699813085873861) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,4,0,3,5,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (28662995244540069) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14861722973251097) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14828911331365981) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,5,1,2,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30788598945546149) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,2,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (15364009321233677) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,2,4,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (6932685297808965) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,2,4,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (27702446411167091) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,2,5,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (14314729037013439) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,2,5,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (14295866101024983) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,3,4,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (27655498134158431) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,3,4,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (6906601868795163) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,3,5,0], ⟨dy (335420853782558795) 59, dy (685531228159052439) 60, dy (152377282652828035) 59, dy (14280157939597081) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,4,0,3,5,1], ⟨dy (656466953106431027) 60, dy (670841707565117591) 60, dy (316335127509405831) 60, dy (7130419883277109) 54⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14796620755518763) 55⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (29529657903972261) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,5,1,2,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30668212743797689) 56⟩), ([5,0,2,0,2,0,3,0,0,5,3,1,5,1,3,5,0,3,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30609146486564685) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,0,2,5,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (6511837732057379) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,0,2,5,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (12983746391566695) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,1,2,5,0,2,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (26797236367533651) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,1,2,5,0,3,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (3340165665150339) 53⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,1,3,5,0,2,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (6661706210598483) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,4,1,3,5,0,3,5], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (26573683089359405) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,0,2,4,1,2], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (1730518968905895) 52⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,0,2,4,1,3], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (27619473574932893) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,0,2,5,1], ⟨dy (373788552645478855) 59, dy (780675171398325421) 60, dy (245898772200819105) 60, dy (7423265420538677) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (13820625628790745) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (13785457588459339) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (13794229165168503) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27516564004079929) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,5,0], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (7398814902068463) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (1848199045308669) 52⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,2,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (7377900258441825) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,4,0,2], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (1718864881948309) 52⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,4,0,3], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (27433973279350239) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27445919232301869) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27376477220352217) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,5,0], ⟨dy (357941144300882061) 59, dy (747577105290957711) 60, dy (67405673126292001) 58, dy (3685409843812797) 53⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29452898793077285) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,2,5,1,3,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29395043347542667) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,3,5,1,2,4,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (27308193839808963) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,3,5,1,2,4,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (6810256854850685) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,3,5,1,2,5,1,2], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29338001988344789) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,0,3,5,1,2,5,1,3], ⟨dy (342765614079526219) 59, dy (715882288601764123) 60, dy (73276877228996737) 58, dy (29281743800650105) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,2,5,0,2,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14733515007188491) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,2,5,0,2,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (3675664817416513) 53⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,2,5,0,3,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (7336121622297775) 54⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,2,5,0,3,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (915140593703813) 51⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,3,5,0,2,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14612661578123011) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,3,5,0,2,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (29166927852648787) 56⟩) ] theorem L_check : (L.all fun x => checkLeaf x.1 x.2) = true := by decide +kernel theorem L_sound : ∀ x ∈ L, SemSBox (ssBox x.1) := checkLeaves_sound L L_check end CKLaneM07.FleetT.T0031 end -- ===== source module CKLaneM07.FleetT.T0032 ===== section /-! M07 derivative leaves (archived same-side owner `derivative`), shard `FleetT.T0032`. Witnesses only propose rationals; `checkLeaf` recomputes every enclosure. -/ set_option maxRecDepth 100000 namespace CKLaneM07.FleetT.T0032 open CKLaneM07 def L : List (List ℕ × Wit) := [ ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,3,5,0,3,5,0,2], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (1819330227579079) 52⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,3,5,0,3,5,0,3], ⟨dy (656466953106431027) 60, dy (685531228159052439) 60, dy (316335127509405831) 60, dy (14526181306955939) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,2,5,1,3,5,0,3,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (15079848049683813) 55⟩), ([5,0,2,0,3,0,0,0,5,2,1,3,5,1,2,5,0,2,5,1,2,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (30106020282153643) 56⟩), ([5,0,2,0,3,0,0,0,5,2,1,3,5,1,2,5,0,2,5,1,3,5], ⟨dy (314317453982457527) 59, dy (164116738276607757) 58, dy (339288325410392369) 60, dy (1878301788940621) 52⟩) ] theorem L_check : (L.all fun x => checkLeaf x.1 x.2) = true := by decide +kernel theorem L_sound : ∀ x ∈ L, SemSBox (ssBox x.1) := checkLeaves_sound L L_check end CKLaneM07.FleetT.T0032 end
Source
arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneM07.FleetT.T0030 (+2 modules: CKLaneM07.FleetT.T0031, CKLaneM07.FleetT.T0032) (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneM07/FleetT/T0030 (+2 modules: CKLaneM07/FleetT/T0031, CKLaneM07/FleetT/T0032).lean)