Prove2Me

Courtade–Kumar proof module `CKLaneM06.CapSS.C030 (+8 modules: CKLaneM06.CapSS.C031, CKLaneM06.CapSS.C032, CKLaneM06.CapSS.C033, CKLaneM06.CapSS.C034, CKLaneM06.CapSS.C035, CKLaneM06.CapS…

Definition
CK_CKLaneM06_CapSS_C030__9

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

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneM06.CapSS.C030 (+8 modules: CKLaneM06.CapSS.C031, CKLaneM06.CapSS.C032, CKLaneM06.CapSS.C033, CKLaneM06.CapSS.C034, CKLaneM06.CapSS.C035, CKLaneM06.CapSS.C036, CKLaneM06.CapSS.C037, CKLaneM06.CapSS.C038) 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 CKLaneM06.CapSS.C030 (+8 modules: CKLaneM06.CapSS.C031, CKLaneM06.CapSS.C032, CKLaneM06.CapSS.C033, CKLaneM06.CapSS.C034, CKLaneM06.CapSS.C035, CKLaneM06.CapSS.C036, CKLaneM06.CapSS.C037, CKLaneM06.CapSS.C038) from release v1.0 (sources_v3.tar.zst).

Definition code
import Definitions.Def_CK_CKLaneM06_CapTree

-- ===== source module CKLaneM06.CapSS.C030 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303030`: 47 archived leaves,
47 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C030

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 0, 3, 0]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (311889828083 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (78139442807 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (310841531803 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (311512532249 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (313222066347 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (156941361967 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (312179920109 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (312843705923 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (154894133807 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155231128777 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (38518138845 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (311132670005 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155899757777 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (77374482981 / 274877906944 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314539754073 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (19699572903 / 68719476736 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (313503899821 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (157080255767 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (78960742587 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (9909322669 / 34359738368 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (316581129123 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314813550399 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315463025371 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (78115701095 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (78280636565 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155708270689 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39009918155 / 137438953472 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (313778750583 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314431426353 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (156369323249 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (4896788347 / 17179869184 : ℚ), true, (0 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (153545668191 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (306032710283 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (308449915411 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (307396917413 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (304969296649 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (151950578869 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (306339003967 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (152638119575 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (77448642979 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (308747337807 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (311125386769 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155042026373 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (307695059007 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (153318900709 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (309037543463 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (153992963327 / 549755813888 : ℚ), true, (0 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C030

end

-- ===== source module CKLaneM06.CapSS.C031 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303031`: 60 archived leaves,
60 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C031

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 0, 3, 1]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317739568357 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317224032669 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318377210239 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (158931676591 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (2469601133 / 8589934592 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (158375658783 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (319011258813 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318499098447 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39955215185 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79782818973 / 274877906944 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39673768855 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318025452335 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315080582197 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315726226373 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314046777049 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314695623335 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (316368366779 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317007010957 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315341001017 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315982917691 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160134302647 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79939973149 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320891916965 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320384955295 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39832153649 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (319285488207 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160755831433 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (321006470387 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322127849041 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40203055493 / 137438953472 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (80124950495 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79997917063 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160559772299 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320613161735 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79410541525 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79568459765 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (316621380609 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79314099169 / 274877906944 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159451018177 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159763382085 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317887972469 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159258057115 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (4881913041 / 17179869184 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155703568655 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39218223019 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (156358330307 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (310366532851 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (154660345407 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (155841048369 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (310642163927 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (157797475999 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39529155163 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (157006343017 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (39608515675 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317499610591 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315295271415 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (312984298969 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (38993801289 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314273197871 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (156622744395 / 549755813888 : ℚ), true, (0 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C031

end

-- ===== source module CKLaneM06.CapSS.C032 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303120`: 90 archived leaves,
90 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C032

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 1, 2, 0]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329874749747 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330453576667 / 1099511627776 : ℚ), false, (151839881 / 134217728 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41116468841 / 137438953472 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164757414209 / 549755813888 : ℚ), false, (151839881 / 134217728 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331028577901 / 1099511627776 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (10362492437 / 34359738368 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41261764875 / 137438953472 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82667406757 / 274877906944 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327981890139 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328569137479 / 1099511627776 : ℚ), false, (151839881 / 134217728 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81756318169 / 274877906944 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81904152393 / 274877906944 : ℚ), false,
    (151839881 / 134217728 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329152636017 / 1099511627776 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82433097583 / 274877906944 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328204235693 / 1099511627776 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328788155649 / 1099511627776 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41520890145 / 137438953472 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332730671383 / 1099511627776 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82810339191 / 274877906944 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331809312179 / 1099511627776 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83322603081 / 274877906944 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83461586845 / 274877906944 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (2596667945 / 8589934592 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41616739315 /
    137438953472 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330308404709 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165440341571 / 549755813888 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329368373753 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82486223507 / 274877906944 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331449229341 / 1099511627776 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332014046737 / 1099511627776 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330517720209 / 1099511627776 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331086855753 / 1099511627776 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326697470037 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326208380409 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81822820599 / 274877906944 : ℚ), false, (151839881 / 134217728 : ℚ)⟩)
    (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40850521127 / 137438953472 : ℚ), false, (151839881 / 134217728 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325717685911 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325225398603 / 1099511627776 : ℚ), false, (151673249 / 134217728 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326315431267 / 1099511627776 : ℚ), false, (151839881 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325825081337 / 1099511627776 : ℚ), false, (151839881 / 134217728 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327249022223 / 1099511627776 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163918514091 / 549755813888 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163454760929 / 549755813888 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163210564021 / 549755813888 : ℚ), false, (304013943 / 268435456 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327499962331 / 1099511627776 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327013543383 / 1099511627776 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324731530387 / 1099511627776 : ℚ), false,
    (151673249 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324236093015 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325333131259 / 1099511627776 : ℚ), false, (151839881 / 134217728 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20302474557 / 68719476736 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323739098087 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (80885749477 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161923340833 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324344478023 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81037368001 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40556421193 / 137438953472 : ℚ), true, (0 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40741389345 / 137438953472 : ℚ), false, (304013943 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325439494019 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326525485577 / 1099511627776 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326035801047 / 1099511627776 : ℚ), false, (1217396201 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701
    / 1099511627776 : ℚ), (324946277673 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324451477425 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325544501771 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81262899895 / 274877906944 : ℚ), true, (0 : ℚ)⟩)))))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82105342525 / 274877906944 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (5140657063 / 17179869184 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328086757031 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327602331729 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328669910013 / 1099511627776 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (5127929643 / 17179869184 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329579077747 / 1099511627776 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330152450731 / 1099511627776 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328633407611 / 1099511627776 : ℚ),
    false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329210938301 / 1099511627776 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327116248101 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326628518407 / 1099511627776 : ℚ), false, (1218740373 / 1073741824 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327703406425 / 1099511627776 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40902206277 / 137438953472 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326139154753 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162824084547 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326730240759 / 1099511627776 : ℚ), false, (1220088327 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326241190131 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328286964357 / 1099511627776 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327803200305 / 1099511627776 : ℚ), false, (610720049 / 536870912 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164433462711 / 549755813888 : ℚ), false, (1222795725 /
    1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82096293055 / 274877906944 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163658881821 / 549755813888 : ℚ), false, (610720049 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40853833321 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163950863485 / 549755813888 : ℚ), false, (1222795725 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327416601997 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C032

end

-- ===== source module CKLaneM06.CapSS.C033 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303121`: 59 archived leaves,
59 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C033

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 1, 2, 1]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166870537721 / 549755813888 : ℚ), false, (75938367 / 67108864 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83372641999 / 274877906944 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334043460263 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334837375747 / 1099511627776 : ℚ), false, (1217822309 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333948787519 / 1099511627776 : ℚ), false, (1217822309 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166287569243 / 549755813888 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41641563435 / 137438953472 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165826151921 / 549755813888 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332214067389 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333686156347 / 1099511627776 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334236087459 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83193037261 / 274877906944 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333326551197 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335918578623 / 1099511627776 : ℚ), false, (610322229 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (5234988955 / 17179869184 : ℚ), false, (610322229 / 536870912 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (84246175055 / 274877906944 : ℚ), false, (1223480691 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (168057435607 / 549755813888 : ℚ), false, (1223480691 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167076039209 / 549755813888 : ℚ), false, (610322229 / 536870912 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333877275989 / 1099511627776 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83606081327 / 274877906944 : ℚ), false, (307753129 / 268435456 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167618473033 / 549755813888 : ℚ), false, (1223480691 / 1073741824 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167483850401 / 549755813888 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335507403881 / 1099511627776 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330722174195 / 1099511627776 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331288251081 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164892428573 / 549755813888 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330355167119 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165925342033 / 549755813888 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332409475567 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330921870929 / 1099511627776 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331484971025 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329443292867 / 1099511627776 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328963569229 / 1099511627776 : ℚ), false, (306038811 / 268435456 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164707460781 / 549755813888 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164241067017 / 549755813888 : ℚ), false, (306038811 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327998999733 / 1099511627776 : ℚ), false, (306038811 / 268435456 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329058987853 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328577862817 / 1099511627776 : ℚ), false, (1225518693 / 1073741824 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82496454161 / 274877906944 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165276572763 / 549755813888 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164816145589 / 549755813888 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329153194021 / 1099511627776 : ℚ), false, (306721527 / 268435456 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329614104553 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332964627745 / 1099511627776 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333516142515 / 1099511627776 : ℚ), false, (307753129 / 268435456 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166022234799 / 549755813888 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332600368589 / 1099511627776 : ℚ), false, (307753129 / 268435456 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41758002693 / 137438953472 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167304133131 / 549755813888 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333152669695 / 1099511627776 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333701374367 / 1099511627776 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82779227609 / 274877906944 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331677113347 / 1099511627776 : ℚ), false, (307753129 / 268435456 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82545514169 / 274877906944 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330746484131 / 1099511627776 : ℚ), false, (307753129 / 268435456 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332233755987 / 1099511627776 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166393419921 / 549755813888 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82826847171 / 274877906944 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331864771855 / 1099511627776 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C033

end

-- ===== source module CKLaneM06.CapSS.C034 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303130`: 72 archived leaves,
72 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C034

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 1, 3, 0]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322740481209 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322238881711 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161674782387 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161424894559 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160867884781 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (80307788905 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40293560291 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (321845655389 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161977552413 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20216073205 / 68719476736 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162278553075 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162030516505 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322957688041 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40307083277 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161781695769 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323064192965 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320148028371 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320765834507 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79785206971 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159881059517 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (80345046953 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160995546609 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320379992975 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40124306837 / 137438953472 : ℚ), true, (0 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325155573231 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162330689409 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325750510259 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40657276615 / 137438953472 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81041399339 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161834120101 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81191077435 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81067203049 / 274877906944 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326341921135 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325851539243 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81732452369 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163220680715 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325359532641 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162432956465 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162975634865 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162729773049 / 549755813888 : ℚ), true, (0 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322598555353 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323202578555 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (321605508885 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314661289 / 1073741824 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324370691561 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161936939921 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324966202109 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162235624595 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322817411953 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323418268755 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318127702859 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (79688101967 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (316564469269 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159686865487 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (319991677227 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (158910163483 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (78887211613 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (314527452875 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (316811292587 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (315796350961 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160303125687 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160608728935 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159800433765 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160107779005 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (321825300881 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (161214892143 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (80206730061 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (10044842443 / 34359738368 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318060579197 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (317052226493 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (159648372207 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (318295118139 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C034

end

-- ===== source module CKLaneM06.CapSS.C035 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031303131`: 78 archived leaves,
78 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C035

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 0, 3, 1, 3, 1]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163757089311 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81756920711 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328095031635 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20475656661 / 68719476736 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326539524395 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163024857559 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163562149877 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326636423133 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328672371315 / 1099511627776 : ℚ), false, (306721527 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328189835447 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329246200193 / 1099511627776 : ℚ), false, (1228257525 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328765672013 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81926399663 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ),
    (40902459127 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41035427959 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327799467375 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325558266709 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162532595357 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163073444265 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81413926903 / 274877906944 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40501966735 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324609810595 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163366035237 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163121401407 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40914226897 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163413239491 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162600250947 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325787810505 / 1099511627776 : ℚ), true, (0 :
    ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329816520543 / 1099511627776 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329338018573 / 1099511627776 : ℚ), false, (1229632983 / 1073741824 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165191667193 / 549755813888 : ℚ), false, (307753129 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164953438585 / 549755813888 : ℚ), false, (307753129 / 268435456 : ℚ)⟩))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328857777137 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328375808559 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164714330557 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82237174665 / 274877906944 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330373673599 / 1099511627776 : ℚ), false, (616198081 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330935277133 / 1099511627776 : ℚ), false, (616891979 / 536870912 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164998038711 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329518139523 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165280013815 / 549755813888 :
    ℚ), false, (616891979 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330084132741 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327892125011 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327406738519 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328467002099 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163991791787 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (326371738897 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163476144641 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329038448309 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41069627005 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164803232631 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329127037567 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81882365905 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164051631811 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ),
    (323030911685 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323628686405 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322039675469 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (40330134439 / 137438953472 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162111555749 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81203547439 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20202447589 / 68719476736 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323833936055 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320519821745 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (319525059945 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (321729840221 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (320742081487 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325401923705 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (10187072363 / 34359738368 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324425401997 / 1099511627776 : ℚ), true,
    (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325013561583 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81641841877 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327145081151 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (325598416893 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163089984879 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (322926824547 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (160973104007 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324110795239 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (323137460587 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C035

end

-- ===== source module CKLaneM06.CapSS.C036 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031312`: 23 archived leaves,
27 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C036

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 1, 2]

def tree : CTree :=
  (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (172158064661 / 549755813888 : ℚ), false, (302240797 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (346076904381 / 1099511627776 : ℚ), false, (1214968127 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (85438286733 / 274877906944 : ℚ), false, (302240797 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (42951403401 / 137438953472 : ℚ), false, (1214968127 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (172440187013 / 549755813888 : ℚ), false, (297107241 / 268435456 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (172702327333 / 549755813888 : ℚ), false, (305255143 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (21695842489 / 68719476736 : ℚ), false, (1227124249 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (170881505331 / 549755813888 : ℚ), false, (302240797 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (340257837755 / 1099511627776 : ℚ), false, (302240797 / 268435456 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (340972432575 / 1099511627776 : ℚ), false, (1214968127 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (169357472797 / 549755813888 : ℚ), false, (302240797 / 268435456 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (169210725173 / 549755813888 : ℚ), false, (613165689 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (339444979005 / 1099511627776 : ℚ), false, (1229196881 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (85180148993 / 274877906944 : ℚ), false, (1214968127 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (339182532005 / 1099511627776 : ℚ), false, (1214968127 / 1073741824 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (342860010005 / 1099511627776 : ℚ), false, (305255143 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (344685284343 / 1099511627776 : ℚ), false, (1227124249 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (340145856443 / 1099511627776 : ℚ), false, (305255143 / 268435456 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (342062241959 / 1099511627776 : ℚ), false, (1227124249 / 1073741824 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (43517585839 / 137438953472 : ℚ), false, (1201507311 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (86533600469 / 274877906944 : ℚ), false, (1201507311 / 1073741824 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (172982161355 / 549755813888 : ℚ), false, (607365687 / 536870912 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (343937124263 / 1099511627776 : ℚ), false, (1201507311 / 1073741824 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (343918609681 / 1099511627776 : ℚ), false, (1233282767 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (172857437173 / 549755813888 : ℚ), false, (1239499637 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (43418765613 / 137438953472 : ℚ), false, (607365687 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (345162518093 / 1099511627776 : ℚ), false, (607365687 / 536870912 : ℚ)⟩)))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C036

end

-- ===== source module CKLaneM06.CapSS.C037 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `03131302`: 50 archived leaves,
50 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C037

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 1, 3, 0, 2]

def tree : CTree :=
  (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336766662849 / 1099511627776 : ℚ), false, (613165689 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (337810170973 / 1099511627776 : ℚ), false, (1229196881 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336307051599 / 1099511627776 : ℚ), false, (613165689 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83857606203 / 274877906944 : ℚ), false, (613165689 / 536870912 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (337362403717 / 1099511627776 : ℚ), false, (1229196881 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336495205911 / 1099511627776 : ℚ), false, (1229196881 / 1073741824 : ℚ)⟩)))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (338838789341 / 1099511627776 : ℚ), false, (616038781 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (339852520323 / 1099511627776 : ℚ), false, (1234973777 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (42148601069 / 137438953472 : ℚ), false, (616038781 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (338222454937 / 1099511627776 : ℚ), false, (1234973777 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335148877861 / 1099511627776 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335685857305 / 1099511627776 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334246483825 / 1099511627776 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83696999763 / 274877906944 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335619815987 / 1099511627776 : ℚ), false, (1229196881 / 1073741824 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335325920807 / 1099511627776 : ℚ), false, (1237972601 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41982531203 / 137438953472 : ℚ), false, (309844339 / 268435456 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83334091539 / 274877906944 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41735291993 / 137438953472 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166209317463 / 549755813888 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166484489471 / 549755813888 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83606187497 / 274877906944 : ℚ), false, (1237972601 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20935225553 / 68719476736 : ℚ), false, (309844339 / 268435456 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333515804719 / 1099511627776 : ℚ), false, (1237972601 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167029556423 / 549755813888 : ℚ), false, (309844339 / 268435456 : ℚ)⟩))))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (168339708433 / 549755813888 : ℚ), false, (616038781 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167902601389 / 549755813888 : ℚ), false, (616038781 / 536870912 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (42215571919 / 137438953472 : ℚ), false, (1234973777 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336859763901 / 1099511627776 : ℚ), false, (1234973777 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167749456431 / 549755813888 : ℚ), false, (620393221 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336030662153 / 1099511627776 : ℚ), false, (621099947 / 536870912 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167299451845 / 549755813888 : ℚ), false, (620393221 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335135177401 / 1099511627776 : ℚ), false, (621099947 / 536870912 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335986665067 / 1099511627776 : ℚ), false, (1234973777 / 1073741824 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (335667933913 / 1099511627776 : ℚ), false, (621808875 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336197172953 / 1099511627776 : ℚ), false, (1245040045 / 1073741824 : ℚ)⟩))))))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (169817936167 / 549755813888 : ℚ), false, (305255143 / 268435456 : ℚ)⟩) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (339241515471 / 1099511627776 : ℚ), false, (1237885879 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (340245985949 / 1099511627776 : ℚ), false, (1240814219 / 1073741824 : ℚ)⟩))) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (170802670631 / 549755813888 : ℚ), false, (1227124249 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (85018889965 / 274877906944 : ℚ), false, (1227124249 / 1073741824 : ℚ)⟩))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (337595867809 / 1099511627776 : ℚ), false, (1237885879 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (338620192831 / 1099511627776 : ℚ), false, (1240814219 / 1073741824 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (84259080827 / 274877906944 : ℚ), false, (1237885879 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336164279571 / 1099511627776 : ℚ), false, (1237885879 / 1073741824 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (336958913465 / 1099511627776 : ℚ), false, (1240814219 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (42453777599 / 137438953472 : ℚ), false, (1243759145 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (170312970685 / 549755813888 : ℚ), false, (311680251 / 268435456 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (168994219999 / 549755813888 : ℚ), false, (1243759145 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (169501978735 / 549755813888 : ℚ), false, (311680251 / 268435456 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C037

end

-- ===== source module CKLaneM06.CapSS.C038 =====
section

/-! Cap cover `same` (root `ssRoot`), archived node `031313030`: 66 archived leaves,
66 refined checker leaves, depth `S = 3/40`.  Generated by M06/work/gen_cap_fleet.py. -/

set_option autoImplicit false

namespace CKLaneM06.Cap.CapSS.C038

open CKLaneM06.Cap

def path : List ℕ := [0, 3, 1, 3, 1, 3, 0, 3, 0]

def tree : CTree :=
  (.node 1 (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331493397761 / 1099511627776 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332048036567 / 1099511627776 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330560759867 / 1099511627776 : ℚ), false, (617587969 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41389951865 / 137438953472 : ℚ), false, (1236572141 / 1073741824 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332599194405 / 1099511627776 : ℚ), false, (1237972601 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333146871899 / 1099511627776 : ℚ), false, (309844339 / 268435456 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331675026033 / 1099511627776 : ℚ), false, (1237972601 / 1073741824 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332226993869 / 1099511627776 : ℚ), false, (309844339 / 268435456 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330171054337 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41211706195 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330732216675 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330256853185 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328673690757 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164889851707 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329300779669 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331289953183 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330816649375 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331299584229 / 1099511627776 : ℚ), false, (309844339 / 268435456 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165170770019 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164932318797 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165449994141 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20651570339 / 68719476736 : ℚ), true, (0 : ℚ)⟩)))))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333691069449 / 1099511627776 : ℚ), false, (620393221 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334231787239 / 1099511627776 : ℚ), false, (621099947 / 536870912 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41596939859 / 137438953472 : ℚ), false, (620393221 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333320601259 / 1099511627776 : ℚ), false, (621099947 / 536870912 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167384512617 / 549755813888 : ℚ), false, (621808875 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (167651391595 / 549755813888 : ℚ), false, (1245040045 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (333862241035 / 1099511627776 : ℚ), false, (621808875 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (334400437989 / 1099511627776 : ℚ), false, (1245040045 / 1073741824 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331852358299 / 1099511627776 : ℚ), false, (620393221 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (332401726665 / 1099511627776 : ℚ), false, (621099947 / 536870912 : ℚ)⟩)) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331455048645 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330982243689 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331475268291 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83236922343 / 274877906944 : ℚ), false, (621808875 / 536870912 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (83372561563 / 274877906944 : ℚ), false, (1245040045 / 1073741824 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (10375796123 / 34359738368 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (166286157257 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))))) (.node 0 (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327719458071 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (10259078111 / 34359738368 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163379110883 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327333174263 / 1099511627776 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328858206645 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329422580167 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (81976207089 / 274877906944 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164236592461 / 549755813888 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (162640884379 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (324315856209 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (5108506117 / 17179869184 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (327516656471 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (20342587997 / 68719476736 : ℚ), true, (0 : ℚ)⟩)))) (.node 1 (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164991810353 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (330541328627 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329038244609 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (164800003919 / 549755813888 : ℚ), true, (0 : ℚ)⟩))) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (165547852037 / 549755813888 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (331646746973 / 1099511627776 : ℚ), true, (0 : ℚ)⟩)) (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41269809351 / 137438953472 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82678411375 / 274877906944 : ℚ), true, (0 : ℚ)⟩)))) (.node 0 (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (328085660409 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (41081425473 / 137438953472 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163317062541 / 549755813888 : ℚ), true, (0 : ℚ)⟩)) (.node 1 (.node 0 (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (329213886857 / 1099511627776 : ℚ), true, (0 : ℚ)⟩) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (82443277417 / 274877906944 : ℚ), true, (0 : ℚ)⟩)) (.leaf ⟨(374042393701 / 1099511627776 : ℚ), (163887006585 / 549755813888 : ℚ), true, (0 : ℚ)⟩))))))

theorem check_ok : tree.check (3 / 40) (cpathBox ssRoot path) = true := by decide +kernel

theorem cap : CapOn (cpathBox ssRoot path) (3 / 40) := CTree.sound_path check_ok

end CKLaneM06.Cap.CapSS.C038

end
Source
arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneM06.CapSS.C030 (+8 modules: CKLaneM06.CapSS.C031, CKLaneM06.CapSS.C032, CKLaneM06.CapSS.C033, CKLaneM06.CapSS.C034, CKLaneM06.CapSS.C035, CKLaneM06.CapSS.C036, CKLaneM06.CapSS.C037, CKLaneM06.CapSS.C038) (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneM06/CapSS/C030 (+8 modules: CKLaneM06/CapSS/C031, CKLaneM06/CapSS/C032, CKLaneM06/CapSS/C033, CKLaneM06/CapSS/C034, CKLaneM06/CapSS/C035, CKLaneM06/CapSS/C036, CKLaneM06/CapSS/C037, CKLaneM06/CapSS/C038).lean)

View graph