Courtade–Kumar proof module `CKLaneN4.L4.S05` (transplant)

Definition
CK_CKLaneN4_L4_S05
by tianyipeng · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)
general-courtade-kumartransplant
Verbatim transplant of the Lean module CKLaneN4.L4.S05 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 CKLaneN4.L4.S05 from release v1.0 (sources_v3.tar.zst).
Definition code
import Definitions.Def_CK_CKLaneN4_OLeafKernel

-- ===== source module CKLaneN4.L4.S05 =====
section

/-! Lane N4 label-4 (`global_eight_ratio`) shard 05: archived OUTER_OPPOSITE leaves
02502413512413513503 .. 02502513503513412412513 (120 leaves, lexicographic = left-first DFS order).  Witnesses generated by
`work/gen_leaves4.py` (untrusted), checked in the kernel by `checkL4` (path binding by `imageCheck`,
log certificates, and the archived label-4 test on the full leaf image). -/

namespace CKLaneN4.L4.S05

open CKLaneD CKLaneN4

set_option maxRecDepth 100000

/-- path 02502413512413513503 (E-class gt) -/
noncomputable def w0 : L4Witness :=
  { box := { alo := (17344316420444129 / 9223372036854775808 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (43 / 64 : ℚ), t1 := (11 / 16 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512413513513 (E-class gt) -/
noncomputable def w1 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (34688632840888259 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (43 / 64 : ℚ), t1 := (11 / 16 : ℚ) },
      pa := ⟨⟨9, 6, (-7409665859894938928093 / 1180591620717411303424 : ℚ), (-14819331719789877856185 / 2361183241434822606848 : ℚ)⟩, ⟨0, 3, (-8888650069197449871 / 4722366482869645213696 : ℚ), (-1111081258649681233 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513403403 (E-class gt) -/
noncomputable def w2 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (11 / 16 : ℚ), t1 := (45 / 64 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513403413 (E-class gt) -/
noncomputable def w3 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (11 / 16 : ℚ), t1 := (45 / 64 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513403513 (E-class gt) -/
noncomputable def w4 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (45 / 64 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513413403 (E-class gt) -/
noncomputable def w5 : L4Witness :=
  { box := { alo := (17344316420444129 / 9223372036854775808 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (11 / 16 : ℚ), t1 := (45 / 64 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513413413 (E-class gt) -/
noncomputable def w6 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (34688632840888259 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (11 / 16 : ℚ), t1 := (45 / 64 : ℚ) },
      pa := ⟨⟨9, 6, (-7409665859894938928093 / 1180591620717411303424 : ℚ), (-14819331719789877856185 / 2361183241434822606848 : ℚ)⟩, ⟨0, 3, (-8888650069197449871 / 4722366482869645213696 : ℚ), (-1111081258649681233 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513413503 (E-class gt) -/
noncomputable def w7 : L4Witness :=
  { box := { alo := (17344316420444129 / 9223372036854775808 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (45 / 64 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513413513 (E-class gt) -/
noncomputable def w8 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (34688632840888259 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (45 / 64 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨9, 6, (-7409665859894938928093 / 1180591620717411303424 : ℚ), (-14819331719789877856185 / 2361183241434822606848 : ℚ)⟩, ⟨0, 3, (-8888650069197449871 / 4722366482869645213696 : ℚ), (-1111081258649681233 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513513403 (E-class gt) -/
noncomputable def w9 : L4Witness :=
  { box := { alo := (17344316420444129 / 9223372036854775808 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (23 / 32 : ℚ), t1 := (47 / 64 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413512513513413 (E-class gt) -/
noncomputable def w10 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (34688632840888259 / 18446744073709551616 : ℚ), blo := (18127278629483760409 / 18446744073709551616 : ℚ), bhi := (1135670857494355533 / 1152921504606846976 : ℚ), t0 := (23 / 32 : ℚ), t1 := (47 / 64 : ℚ) },
      pa := ⟨⟨9, 6, (-7409665859894938928093 / 1180591620717411303424 : ℚ), (-14819331719789877856185 / 2361183241434822606848 : ℚ)⟩, ⟨0, 3, (-8888650069197449871 / 4722366482869645213696 : ℚ), (-1111081258649681233 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-41249804207949275367 / 2361183241434822606848 : ℚ), (-82499608415898550733 / 4722366482869645213696 : ℚ)⟩, ⟨6, 8, (-19153890350513578173541 / 4722366482869645213696 : ℚ), (-19153890350513578173539 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 025024135134 (E-class straddle) -/
noncomputable def w11 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (5 / 8 : ℚ), t1 := (11 / 16 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 025024135135024024 (E-class gt) -/
noncomputable def w12 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (11 / 16 : ℚ), t1 := (45 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513502402503 (E-class gt) -/
noncomputable def w13 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (45 / 64 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250241351350240251 (E-class gt) -/
noncomputable def w14 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (45 / 64 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513502403 (E-class straddle) -/
noncomputable def w15 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (11 / 16 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 0250241351350241 (E-class straddle) -/
noncomputable def w16 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (11 / 16 : ℚ), t1 := (23 / 32 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513502502403 (E-class gt) -/
noncomputable def w17 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (23 / 32 : ℚ), t1 := (47 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413513502502413 (E-class gt) -/
noncomputable def w18 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (23 / 32 : ℚ), t1 := (47 / 64 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413513502502503 (E-class gt) -/
noncomputable def w19 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (47 / 64 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413513502502513 (E-class gt) -/
noncomputable def w20 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (47 / 64 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502413513502503 (E-class straddle) -/
noncomputable def w21 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (23 / 32 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 025024135135025124 (E-class gt) -/
noncomputable def w22 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (23 / 32 : ℚ), t1 := (47 / 64 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513502512503 (E-class gt) -/
noncomputable def w23 : L4Witness :=
  { box := { alo := (59616553825835715 / 18446744073709551616 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (47 / 64 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250241351350251251 (E-class gt) -/
noncomputable def w24 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (47 / 64 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513502513 (E-class straddle) -/
noncomputable def w25 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (23 / 32 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502413513503 (E-class straddle) -/
noncomputable def w26 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (11 / 16 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250241351351 (E-class straddle) -/
noncomputable def w27 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (11 / 16 : ℚ), t1 := (3 / 4 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513403412403413 (E-class gt) -/
noncomputable def w28 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403412403513 (E-class gt) -/
noncomputable def w29 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403412413403 (E-class gt) -/
noncomputable def w30 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 0250251340341241341 (E-class gt) -/
noncomputable def w31 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513403412413503 (E-class gt) -/
noncomputable def w32 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 0250251340341241351 (E-class gt) -/
noncomputable def w33 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513403412513403 (E-class gt) -/
noncomputable def w34 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403412513413 (E-class gt) -/
noncomputable def w35 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403412513503 (E-class gt) -/
noncomputable def w36 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403412513513 (E-class gt) -/
noncomputable def w37 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 025025134034134 (E-class straddle) -/
noncomputable def w38 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (153791139546884629 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (3 / 4 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251340341350241 (E-class gt) -/
noncomputable def w39 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251340341350251 (E-class gt) -/
noncomputable def w40 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251340341351 (E-class straddle) -/
noncomputable def w41 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (25 / 32 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513403512413413 (E-class gt) -/
noncomputable def w42 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513403512413513 (E-class gt) -/
noncomputable def w43 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 0250251340351340241 (E-class gt) -/
noncomputable def w44 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513403513402513 (E-class gt) -/
noncomputable def w45 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251340351341 (E-class straddle) -/
noncomputable def w46 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (13 / 16 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513403513502413 (E-class gt) -/
noncomputable def w47 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (27 / 32 : ℚ), t1 := (55 / 64 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513403513502513 (E-class gt) -/
noncomputable def w48 : L4Witness :=
  { box := { alo := (117311739046811211 / 18446744073709551616 : ℚ), ahi := (134318673423451653 / 18446744073709551616 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (18329432334662740405 / 18446744073709551616 : ℚ), t0 := (55 / 64 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨7, 7, (-23245509116978427979415 / 4722366482869645213696 : ℚ), (-23245509116978427979413 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-34511379529647635279 / 4722366482869645213696 : ℚ), (-34511379529647635277 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251340351351 (E-class straddle) -/
noncomputable def w49 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (27 / 32 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402402413 (E-class gt) -/
noncomputable def w50 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402402513 (E-class gt) -/
noncomputable def w51 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402403 (E-class straddle) -/
noncomputable def w52 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413402412403 (E-class gt) -/
noncomputable def w53 : L4Witness :=
  { box := { alo := (59616553825835715 / 18446744073709551616 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251341340241241 (E-class gt) -/
noncomputable def w54 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (3 / 4 : ℚ), t1 := (49 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413402412503 (E-class gt) -/
noncomputable def w55 : L4Witness :=
  { box := { alo := (59616553825835715 / 18446744073709551616 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402412513 (E-class gt) -/
noncomputable def w56 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (49 / 64 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402413 (E-class straddle) -/
noncomputable def w57 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413402503 (E-class gt) -/
noncomputable def w58 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413402512403 (E-class gt) -/
noncomputable def w59 : L4Witness :=
  { box := { alo := (59616553825835715 / 18446744073709551616 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402512413 (E-class gt) -/
noncomputable def w60 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402512503 (E-class gt) -/
noncomputable def w61 : L4Witness :=
  { box := { alo := (59616553825835715 / 18446744073709551616 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402512513 (E-class gt) -/
noncomputable def w62 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413402513 (E-class straddle) -/
noncomputable def w63 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413403 (E-class straddle) -/
noncomputable def w64 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (3 / 4 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 025025134134124 (E-class straddle) -/
noncomputable def w65 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (3 / 4 : ℚ), t1 := (25 / 32 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413412502403 (E-class gt) -/
noncomputable def w66 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251341341250241 (E-class gt) -/
noncomputable def w67 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (25 / 32 : ℚ), t1 := (51 / 64 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413412502503 (E-class gt) -/
noncomputable def w68 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413412502513 (E-class gt) -/
noncomputable def w69 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (51 / 64 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413412503 (E-class straddle) -/
noncomputable def w70 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 0250251341341251 (E-class straddle) -/
noncomputable def w71 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (25 / 32 : ℚ), t1 := (13 / 16 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 025025134135024034 (E-class gt) -/
noncomputable def w72 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413502403503 (E-class gt) -/
noncomputable def w73 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 0250251341350240351 (E-class gt) -/
noncomputable def w74 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413502412413 (E-class gt) -/
noncomputable def w75 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (14904138456458929 / 4611686018427387904 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-27081401710539224645799 / 4722366482869645213696 : ℚ), (-27081401710539224645795 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15286552798647712241 / 4722366482869645213696 : ℚ), (-955409549915482015 / 295147905179352825856 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413502413 (E-class straddle) -/
noncomputable def w76 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (13 / 16 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413502503403 (E-class gt) -/
noncomputable def w77 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (27 / 32 : ℚ), t1 := (55 / 64 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 0250251341350250341 (E-class gt) -/
noncomputable def w78 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (27 / 32 : ℚ), t1 := (55 / 64 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413502503503 (E-class gt) -/
noncomputable def w79 : L4Witness :=
  { box := { alo := (39077494815224457 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (55 / 64 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513413502503513 (E-class gt) -/
noncomputable def w80 : L4Witness :=
  { box := { alo := (68259293477601201 / 18446744073709551616 : ℚ), ahi := (78154989630448915 / 18446744073709551616 : ℚ), blo := (18268740045828186991 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (55 / 64 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 7, (-12901385423009479539019 / 2361183241434822606848 : ℚ), (-3225346355752369884753 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-2506272701343555593 / 590295810358705651712 : ℚ), (-20050181610748444743 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-45790317706569249379 / 4722366482869645213696 : ℚ), (-11447579426642312341 / 1180591620717411303424 : ℚ)⟩, ⟨7, 10, (-684866656808667243363 / 147573952589676412928 : ℚ), (-5478933254469337946897 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513413502513 (E-class gt) -/
noncomputable def w81 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (34129646738800601 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (27 / 32 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 6, (-26442086278279091850947 / 4722366482869645213696 : ℚ), (-13221043139139545925453 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-1094174357061605587 / 295147905179352825856 : ℚ), (-17506789712985689391 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413503 (E-class straddle) -/
noncomputable def w82 : L4Witness :=
  { box := { alo := (26034062975139279 / 9223372036854775808 : ℚ), ahi := (22371321518805129 / 4611686018427387904 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 10, (-12581727706879413152253 / 2361183241434822606848 : ℚ), (-12581727706879413152229 / 2361183241434822606848 : ℚ)⟩, ⟨0, 4, (-11481988793303635765 / 2361183241434822606848 : ℚ), (-22963977586607271529 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512402403 (E-class gt) -/
noncomputable def w83 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512402413 (E-class gt) -/
noncomputable def w84 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512402503 (E-class gt) -/
noncomputable def w85 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512402513 (E-class gt) -/
noncomputable def w86 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (53 / 64 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512403 (E-class straddle) -/
noncomputable def w87 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (13 / 16 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413512412403 (E-class gt) -/
noncomputable def w88 : L4Witness :=
  { box := { alo := (17344316420444129 / 9223372036854775808 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251341351241241 (E-class gt) -/
noncomputable def w89 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (34688632840888259 / 18446744073709551616 : ℚ), blo := (18170733719909688527 / 18446744073709551616 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (53 / 64 : ℚ) },
      pa := ⟨⟨9, 6, (-7409665859894938928093 / 1180591620717411303424 : ℚ), (-14819331719789877856185 / 2361183241434822606848 : ℚ)⟩, ⟨0, 3, (-8888650069197449871 / 4722366482869645213696 : ℚ), (-1111081258649681233 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-71192600274498306705 / 4722366482869645213696 : ℚ), (-4449537517156144169 / 295147905179352825856 : ℚ)⟩, ⟨6, 6, (-19844351017354521578777 / 4722366482869645213696 : ℚ), (-9922175508677260789387 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413512413 (E-class straddle) -/
noncomputable def w90 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (13 / 16 : ℚ), t1 := (27 / 32 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413512502403 (E-class gt) -/
noncomputable def w91 : L4Witness :=
  { box := { alo := (22737726067614299 / 9223372036854775808 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (27 / 32 : ℚ), t1 := (55 / 64 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512502413 (E-class gt) -/
noncomputable def w92 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (45475452135228599 / 18446744073709551616 : ℚ), blo := (9104138929203104377 / 9223372036854775808 : ℚ), bhi := (9120357539285720337 / 9223372036854775808 : ℚ), t0 := (27 / 32 : ℚ), t1 := (55 / 64 : ℚ) },
      pa := ⟨⟨9, 11, (-14180016287529745120927 / 2361183241434822606848 : ℚ), (-28360032575059490241851 / 4722366482869645213696 : ℚ)⟩, ⟨0, 3, (-5828044561360193033 / 2361183241434822606848 : ℚ), (-11656089122720386023 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 5, (-30722686574994779673 / 2361183241434822606848 : ℚ), (-61445373149989559345 / 4722366482869645213696 : ℚ)⟩, ⟨6, 10, (-20534811684195464987593 / 4722366482869645213696 : ℚ), (-20534811684195464987589 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513413512503 (E-class straddle) -/
noncomputable def w93 : L4Witness :=
  { box := { alo := (39717518331239337 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (27 / 32 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413512513 (E-class straddle) -/
noncomputable def w94 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (19858759165619669 / 9223372036854775808 : ℚ), blo := (18240715078571440673 / 18446744073709551616 : ℚ), bhi := (4573238233540666747 / 4611686018427387904 : ℚ), t0 := (27 / 32 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨9, 8, (-28999348007319623024189 / 4722366482869645213696 : ℚ), (-7249837001829905756047 / 1180591620717411303424 : ℚ)⟩, ⟨0, 3, (-5089323202557376849 / 2361183241434822606848 : ℚ), (-10178646405114753681 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-53040176221260653199 / 4722366482869645213696 : ℚ), (-26520088110630326573 / 2361183241434822606848 : ℚ)⟩, ⟨6, 13, (-5306318087759102094609 / 1180591620717411303424 : ℚ), (-10612636175518204189213 / 2361183241434822606848 : ℚ)⟩⟩ }

/-- path 02502513413513 (E-class straddle) -/
noncomputable def w95 : L4Witness :=
  { box := { alo := (30296486259150517 / 18446744073709551616 : ℚ), ahi := (52068125950278559 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (9180526335094835031 / 9223372036854775808 : ℚ), t0 := (13 / 16 : ℚ), t1 := (7 / 8 : ℚ) },
      pa := ⟨⟨8, 13, (-27720717142799357462315 / 4722366482869645213696 : ℚ), (-27720717142799357462311 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-13348287681784877827 / 4722366482869645213696 : ℚ), (-6674143840892438913 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341341240251 (E-class gt) -/
noncomputable def w96 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (6852105321012001 / 1152921504606846976 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (113 / 128 : ℚ), t1 := (57 / 64 : ℚ) },
      pa := ⟨⟨7, 12, (-24204482265368627145371 / 4722366482869645213696 : ℚ), (-3025560283171078393171 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-28149957676052909607 / 4722366482869645213696 : ℚ), (-14074978838026454803 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413412403 (E-class gt) -/
noncomputable def w97 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (7 / 8 : ℚ), t1 := (57 / 64 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341341241 (E-class gt) -/
noncomputable def w98 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (7 / 8 : ℚ), t1 := (57 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341341250241 (E-class gt) -/
noncomputable def w99 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (6852105321012001 / 1152921504606846976 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (57 / 64 : ℚ), t1 := (115 / 128 : ℚ) },
      pa := ⟨⟨7, 12, (-24204482265368627145371 / 4722366482869645213696 : ℚ), (-3025560283171078393171 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-28149957676052909607 / 4722366482869645213696 : ℚ), (-14074978838026454803 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413412503 (E-class gt) -/
noncomputable def w100 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (57 / 64 : ℚ), t1 := (29 / 32 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341341251 (E-class gt) -/
noncomputable def w101 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (57 / 64 : ℚ), t1 := (29 / 32 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413413 (E-class straddle) -/
noncomputable def w102 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18331946083323419399 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (7 / 8 : ℚ), t1 := (29 / 32 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-29480111463868904069 / 4722366482869645213696 : ℚ), (-7370027865967226017 / 1180591620717411303424 : ℚ)⟩, ⟨7, 11, (-23987115018400182006503 / 4722366482869645213696 : ℚ), (-5996778754600045501625 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513503413512403 (E-class gt) -/
noncomputable def w103 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (29 / 32 : ℚ), t1 := (59 / 64 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341351241 (E-class gt) -/
noncomputable def w104 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (29 / 32 : ℚ), t1 := (59 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413512503 (E-class gt) -/
noncomputable def w105 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (59 / 64 : ℚ), t1 := (15 / 16 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413512512403 (E-class gt) -/
noncomputable def w106 : L4Witness :=
  { box := { alo := (47876136406182201 / 9223372036854775808 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (59 / 64 : ℚ), t1 := (119 / 128 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341351251241 (E-class gt) -/
noncomputable def w107 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (95752272812364403 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (59 / 64 : ℚ), t1 := (119 / 128 : ℚ) },
      pa := ⟨⟨8, 12, (-24843797697628759944331 / 4722366482869645213696 : ℚ), (-24843797697628759944325 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-6144105521931863719 / 1180591620717411303424 : ℚ), (-24576422087727454875 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413512512503 (E-class gt) -/
noncomputable def w108 : L4Witness :=
  { box := { alo := (47876136406182201 / 9223372036854775808 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (119 / 128 : ℚ), t1 := (15 / 16 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350341351251251 (E-class gt) -/
noncomputable def w109 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (95752272812364403 / 18446744073709551616 : ℚ), blo := (18292952934162666987 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (119 / 128 : ℚ), t1 := (15 / 16 : ℚ) },
      pa := ⟨⟨8, 12, (-24843797697628759944331 / 4722366482869645213696 : ℚ), (-24843797697628759944325 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-6144105521931863719 / 1180591620717411303424 : ℚ), (-24576422087727454875 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-9883891592184874021 / 1180591620717411303424 : ℚ), (-39535566368739496079 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-353221776323723362417 / 73786976294838206464 : ℚ), (-22606193684718295194687 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413512513 (E-class gt) -/
noncomputable def w110 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (59 / 64 : ℚ), t1 := (15 / 16 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503413513 (E-class gt) -/
noncomputable def w111 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18331946083323419399 / 18446744073709551616 : ℚ), bhi := (18357258787634331101 / 18446744073709551616 : ℚ), t0 := (29 / 32 : ℚ), t1 := (15 / 16 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-29480111463868904069 / 4722366482869645213696 : ℚ), (-7370027865967226017 / 1180591620717411303424 : ℚ)⟩, ⟨7, 11, (-23987115018400182006503 / 4722366482869645213696 : ℚ), (-5996778754600045501625 / 1180591620717411303424 : ℚ)⟩⟩ }

/-- path 02502513503513412403403 (E-class gt) -/
noncomputable def w112 : L4Witness :=
  { box := { alo := (109633685136192015 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18323239357275942235 / 18446744073709551616 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (15 / 16 : ℚ), t1 := (121 / 128 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-31723524041990286759 / 4722366482869645213696 : ℚ), (-15861762020995143379 / 2361183241434822606848 : ℚ)⟩, ⟨7, 9, (-11820942342489855151073 / 2361183241434822606848 : ℚ), (-23641884684979710302139 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350351341240341 (E-class gt) -/
noncomputable def w113 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (6852105321012001 / 1152921504606846976 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (15 / 16 : ℚ), t1 := (121 / 128 : ℚ) },
      pa := ⟨⟨7, 12, (-24204482265368627145371 / 4722366482869645213696 : ℚ), (-3025560283171078393171 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-28149957676052909607 / 4722366482869645213696 : ℚ), (-14074978838026454803 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503513412403503 (E-class gt) -/
noncomputable def w114 : L4Witness :=
  { box := { alo := (109633685136192015 / 18446744073709551616 : ℚ), ahi := (29327934761702803 / 4611686018427387904 : ℚ), blo := (18323239357275942235 / 18446744073709551616 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (121 / 128 : ℚ), t1 := (61 / 64 : ℚ) },
      pa := ⟨⟨7, 10, (-1492801534327410046175 / 295147905179352825856 : ℚ), (-23884824549238560738783 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-15063852679905405301 / 2361183241434822606848 : ℚ), (-30127705359810810601 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-31723524041990286759 / 4722366482869645213696 : ℚ), (-15861762020995143379 / 2361183241434822606848 : ℚ)⟩, ⟨7, 9, (-11820942342489855151073 / 2361183241434822606848 : ℚ), (-23641884684979710302139 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 0250251350351341240351 (E-class gt) -/
noncomputable def w115 : L4Witness :=
  { box := { alo := (51229079946319351 / 9223372036854775808 : ℚ), ahi := (6852105321012001 / 1152921504606846976 : ℚ), blo := (4578468069816005025 / 4611686018427387904 : ℚ), bhi := (2291493260415427425 / 2305843009213693952 : ℚ), t0 := (121 / 128 : ℚ), t1 := (61 / 64 : ℚ) },
      pa := ⟨⟨7, 12, (-24204482265368627145371 / 4722366482869645213696 : ℚ), (-3025560283171078393171 / 590295810358705651712 : ℚ)⟩, ⟨0, 4, (-28149957676052909607 / 4722366482869645213696 : ℚ), (-14074978838026454803 / 2361183241434822606848 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-34138276419230446711 / 4722366482869645213696 : ℚ), (-34138276419230446709 / 4722366482869645213696 : ℚ)⟩, ⟨7, 7, (-23296654351559238602195 / 4722366482869645213696 : ℚ), (-23296654351559238602181 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503513412412403 (E-class gt) -/
noncomputable def w116 : L4Witness :=
  { box := { alo := (47876136406182201 / 9223372036854775808 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (15 / 16 : ℚ), t1 := (121 / 128 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503513412412413 (E-class gt) -/
noncomputable def w117 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (95752272812364403 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (15 / 16 : ℚ), t1 := (121 / 128 : ℚ) },
      pa := ⟨⟨8, 12, (-24843797697628759944331 / 4722366482869645213696 : ℚ), (-24843797697628759944325 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-6144105521931863719 / 1180591620717411303424 : ℚ), (-24576422087727454875 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503513412412503 (E-class gt) -/
noncomputable def w118 : L4Witness :=
  { box := { alo := (47876136406182201 / 9223372036854775808 : ℚ), ahi := (102458159892638703 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (121 / 128 : ℚ), t1 := (61 / 64 : ℚ) },
      pa := ⟨⟨7, 13, (-12262069990749346774091 / 2361183241434822606848 : ℚ), (-24524139981498693548167 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-26302402034494298921 / 4722366482869645213696 : ℚ), (-3287800254311787365 / 590295810358705651712 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }

/-- path 02502513503513412412513 (E-class gt) -/
noncomputable def w119 : L4Witness :=
  { box := { alo := (89485286075220515 / 18446744073709551616 : ℚ), ahi := (95752272812364403 / 18446744073709551616 : ℚ), blo := (18303794765626519233 / 18446744073709551616 : ℚ), bhi := (18313872279264020101 / 18446744073709551616 : ℚ), t0 := (121 / 128 : ℚ), t1 := (61 / 64 : ℚ) },
      pa := ⟨⟨8, 12, (-24843797697628759944331 / 4722366482869645213696 : ℚ), (-24843797697628759944325 / 4722366482869645213696 : ℚ)⟩, ⟨0, 4, (-6144105521931863719 / 1180591620717411303424 : ℚ), (-24576422087727454875 / 4722366482869645213696 : ℚ)⟩⟩,
      pb := ⟨⟨0, 4, (-2296097033954275801 / 295147905179352825856 : ℚ), (-36737552543268412813 / 4722366482869645213696 : ℚ)⟩, ⟨7, 4, (-22951424018138766889907 / 4722366482869645213696 : ℚ), (-22951424018138766889903 / 4722366482869645213696 : ℚ)⟩⟩ }


noncomputable def leaves : List (List ℕ × L4Witness) := [
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 4, 1, 3, 5, 1, 3, 5, 0, 3], w0),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 4, 1, 3, 5, 1, 3, 5, 1, 3], w1),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 0, 3, 4, 0, 3], w2),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3], w3),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3], w4),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 1, 3, 4, 0, 3], w5),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 1, 3, 4, 1, 3], w6),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 1, 3, 5, 0, 3], w7),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 4, 1, 3, 5, 1, 3], w8),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 4, 0, 3], w9),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 4, 1, 3], w10),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 4], w11),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 4, 0, 2, 4], w12),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 4, 0, 2, 5, 0, 3], w13),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 4, 0, 2, 5, 1], w14),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 4, 0, 3], w15),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 4, 1], w16),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 4, 0, 3], w17),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 4, 1, 3], w18),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3], w19),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 5, 1, 3], w20),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 3], w21),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 1, 2, 4], w22),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 1, 2, 5, 0, 3], w23),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 1, 2, 5, 1], w24),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 2, 5, 1, 3], w25),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 0, 3], w26),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 1, 3, 5, 1], w27),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 0, 3, 4, 1, 3], w28),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 0, 3, 5, 1, 3], w29),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 1, 3, 4, 0, 3], w30),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 1, 3, 4, 1], w31),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 1, 3, 5, 0, 3], w32),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 4, 1, 3, 5, 1], w33),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 5, 1, 3, 4, 0, 3], w34),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 5, 1, 3, 4, 1, 3], w35),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 5, 1, 3, 5, 0, 3], w36),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 2, 5, 1, 3, 5, 1, 3], w37),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3, 4], w38),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3, 5, 0, 2, 4, 1], w39),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3, 5, 0, 2, 5, 1], w40),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3, 5, 1], w41),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 2, 4, 1, 3, 4, 1, 3], w42),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 2, 4, 1, 3, 5, 1, 3], w43),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 4, 0, 2, 4, 1], w44),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 4, 0, 2, 5, 1, 3], w45),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 4, 1], w46),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 5, 0, 2, 4, 1, 3], w47),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 5, 0, 2, 5, 1, 3], w48),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 5, 1], w49),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 0, 2, 4, 1, 3], w50),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 0, 2, 5, 1, 3], w51),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 0, 3], w52),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 1, 2, 4, 0, 3], w53),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 1, 2, 4, 1], w54),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 1, 2, 5, 0, 3], w55),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 1, 2, 5, 1, 3], w56),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 4, 1, 3], w57),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 0, 3], w58),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 1, 2, 4, 0, 3], w59),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 1, 2, 4, 1, 3], w60),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 1, 2, 5, 0, 3], w61),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 1, 2, 5, 1, 3], w62),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 2, 5, 1, 3], w63),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 0, 3], w64),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 4], w65),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 0, 2, 4, 0, 3], w66),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 0, 2, 4, 1], w67),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 0, 2, 5, 0, 3], w68),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 0, 2, 5, 1, 3], w69),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 0, 3], w70),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 4, 1, 2, 5, 1], w71),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 4, 0, 3, 4], w72),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 4, 0, 3, 5, 0, 3], w73),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 4, 0, 3, 5, 1], w74),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 4, 1, 2, 4, 1, 3], w75),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 4, 1, 3], w76),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 5, 0, 3, 4, 0, 3], w77),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 5, 0, 3, 4, 1], w78),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 5, 0, 3, 5, 0, 3], w79),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 5, 0, 3, 5, 1, 3], w80),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 2, 5, 1, 3], w81),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 0, 3], w82),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 0, 2, 4, 0, 3], w83),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 0, 2, 4, 1, 3], w84),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 0, 2, 5, 0, 3], w85),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 0, 2, 5, 1, 3], w86),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 0, 3], w87),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 1, 2, 4, 0, 3], w88),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 1, 2, 4, 1], w89),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 4, 1, 3], w90),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 5, 0, 2, 4, 0, 3], w91),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 5, 0, 2, 4, 1, 3], w92),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 5, 0, 3], w93),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 2, 5, 1, 3], w94),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 1, 3, 5, 1, 3], w95),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 4, 0, 2, 5, 1], w96),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 4, 0, 3], w97),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 4, 1], w98),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 5, 0, 2, 4, 1], w99),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 5, 0, 3], w100),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 2, 5, 1], w101),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 1, 3], w102),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 4, 0, 3], w103),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 4, 1], w104),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 0, 3], w105),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 1, 2, 4, 0, 3], w106),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 1, 2, 4, 1], w107),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 1, 2, 5, 0, 3], w108),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 1, 2, 5, 1], w109),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 1, 3], w110),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 1, 3], w111),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0, 3, 4, 0, 3], w112),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0, 3, 4, 1], w113),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0, 3, 5, 0, 3], w114),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0, 3, 5, 1], w115),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 1, 2, 4, 0, 3], w116),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 1, 2, 4, 1, 3], w117),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 1, 2, 5, 0, 3], w118),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 1, 2, 5, 1, 3], w119)]

theorem ok : (leaves.all fun x => checkL4 x.1 x.2) = true := by decide +kernel

theorem sem : ∀ x ∈ leaves, CKLaneD.OCompact.OLeafOK (uvtBox x.1) := l4_list_sound leaves ok

end CKLaneN4.L4.S05

end
Source
arXiv:2609.24931; https://github.com/dpwoodru/general-courtade-kumar-lean release v1.0, module CKLaneN4.L4.S05 (browse copy where available: https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneN4/L4/S05.lean)
View graph