Prove2Me

Courtade–Kumar proof module `CKLaneD.Structural` (transplant)

Definition
CK_CKLaneD_Structural

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

general-courtade-kumartransplant

Verbatim transplant of the Lean module CKLaneD.Structural 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 CKLaneD.Structural from release v1.0 (sources_v3.tar.zst).

Definition code
import Definitions.Def_CK_CKLaneD_OCompact

-- ===== source module CKLaneD.Structural =====
section

/-!
# Lane D: structural leaf families of the archived (O) tree

* label 5 (`outside`, 449 leaves): the physical image `InUVT (uvtBox q.1)` is EMPTY (certified by exact
  Nat-power bounds: `2^-v0 ≤ x < r ≤ 2^-u1` forces `a + b > 1`, or `1/10 < r ≤ 2^-u1` forces `a > 1/10`),
  so `SemUVT` and `OLeafOK` hold vacuously;
* label 12 (`global_corner`, 1 leaf): the image lies in `a + (1 - b) ≤ 2^-13`, so `OLeafOK` holds
  vacuously (the row hypothesis `1/8192 < a + (1 - b)` fails).
Leaf lists are bound to `ArchTree.archTree` by kernel-checked list equalities.
-/

namespace CKLaneD.Structural

open CKLaneD GeneralCK

/-- Emptiness certificate of an `outside` leaf image. -/
inductive OutCert where
  | big (r : ℚ)
  | sep (x r : ℚ)
  deriving Repr

def outCheck (U : UVT) : OutCert → Bool
  | .big r => decide (1 / 10 < r) && pow2LowerOK r U.u1
  | .sep x r => decide (x < r) && pow2UpperOK x U.v0 && pow2LowerOK r U.u1

theorem outCheck_empty {U : UVT} {c : OutCert} (h : outCheck U c = true) {a b E : ℝ}
    (hin : InUVT U a b E) : False := by
  obtain ⟨h1, h2, h3, h4, h5, h6, h7, h8⟩ := hin
  cases c with
  | big r =>
    simp only [outCheck, Bool.and_eq_true, decide_eq_true_eq] at h
    have hr := pow2LowerOK_sound h.2
    have h10 : ((1 / 10 : ℚ) : ℝ) < (r : ℝ) := Rat.cast_lt.mpr h.1
    have e10 : ((1 / 10 : ℚ) : ℝ) = 1 / 10 := by norm_num
    rw [e10] at h10
    linarith
  | sep x r =>
    simp only [outCheck, Bool.and_eq_true, decide_eq_true_eq] at h
    obtain ⟨⟨hxr, hx⟩, hr⟩ := h
    have hx' := pow2UpperOK_sound hx
    have hr' := pow2LowerOK_sound hr
    have hxr' : (x : ℝ) < (r : ℝ) := Rat.cast_lt.mpr hxr
    linarith

def cornerCheck (U : UVT) (ha hx : ℚ) : Bool :=
  pow2UpperOK ha U.u0 && pow2UpperOK hx U.v0 && decide (ha + hx ≤ 1 / 8192)

theorem cornerCheck_sound {U : UVT} {ha hx : ℚ} (h : cornerCheck U ha hx = true) {a b E : ℝ}
    (hin : InUVT U a b E) : a + (1 - b) ≤ 1 / 8192 := by
  obtain ⟨h1, h2, h3, h4, h5, h6, h7, h8⟩ := hin
  simp only [cornerCheck, Bool.and_eq_true, decide_eq_true_eq] at h
  obtain ⟨⟨hA, hX⟩, hs⟩ := h
  have hA' := pow2UpperOK_sound hA
  have hX' := pow2UpperOK_sound hX
  have hs' : ((ha + hx : ℚ) : ℝ) ≤ ((1 / 8192 : ℚ) : ℝ) := Rat.cast_le.mpr hs
  push_cast at hs'
  linarith

-- generated by work/gen_structural.py
set_option maxHeartbeats 4000000 in
noncomputable def outsideCerts : List (List ℕ × OutCert) := [
  ([0, 2, 4, 0, 2, 4, 0, 3, 5, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 4, 0, 3, 5, 0, 2, 4, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 4, 0, 2, 4, 0, 3, 5, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 4, 0, 3, 5, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 4, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 4, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 5, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 270651822392855466733 74)),
  ([0, 2, 4, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 4, 0, 3, 4, 1, 3], OutCert.sep (dy 541303644785710933467 80) (dy 496377630869922078343 78)),
  ([0, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 270651822392855466733 74)),
  ([0, 2, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 4, 0, 3, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 1743528573152561684309 80) (dy 496377630869922078343 78)),
  ([0, 2, 4, 0, 3, 5, 1, 3], OutCert.sep (dy 541303644785710933467 80) (dy 496377630869922078343 78)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 4, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 5, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 4, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 5, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 4, 1, 3, 4, 0, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 0, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 0, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 0, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 4, 1, 3, 5, 0, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0, 3, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0, 3, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 1, 3, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 1, 3, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 104565274270369391440123 80) (dy 115270937174462722794525 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 4, 1, 3], OutCert.sep (dy 2439161032330159605275 75) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 104565274270369391440123 80) (dy 115270937174462722794525 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3, 5, 1, 3], OutCert.sep (dy 2439161032330159605275 75) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0, 2, 4, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0], OutCert.big (dy 131982012127308362811607 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.big (dy 123343788769788239648867 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 104565274270369391440123 80) (dy 115270937174462722794525 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 2439161032330159605275 75) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 104565274270369391440123 80) (dy 115270937174462722794525 80)),
  ([0, 2, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 2439161032330159605275 75) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 4, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 2, 5, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 4, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3, 5, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 2, 5, 1, 3], OutCert.sep (dy 10872674869940964339533 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 4, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 87928564293975092766161 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 4, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 4, 1, 2, 5, 1, 3], OutCert.sep (dy 12584469602060304164313 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 10872674869940964339533 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 67071827542255321026715 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 12584469602060304164313 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 58263077691401519879139 80) (dy 3661215027612086139221 76)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 12584469602060304164313 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 10872674869940964339533 78) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 2, 5, 1, 3], OutCert.sep (dy 32463800681066177145325 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 0, 3], OutCert.sep (dy 18088614546627827380719 80) (dy 6395291004095081843859 77)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0, 3, 5, 1, 3], OutCert.sep (dy 24232729463235461574761 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 1, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 37574903850724652899695 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 10872674869940964339533 78) (dy 44684343004824898954503 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 37574903850724652899695 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 24232729463235461574761 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 39026576517282553684399 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 28047932174274020708941 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 32463800681066177145325 80) (dy 17042587763848878000625 79)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 28047932174274020708941 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 24232729463235461574761 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 24298431058027438548667 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 24298431058027438548667 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 10468243676390726260285 79) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 26000140376429344595389 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 24298431058027438548667 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 24232729463235461574761 80) (dy 24298431058027438548667 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 10468243676390726260285 79) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 10468243676390726260285 79) (dy 21221853453985647954651 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 10468243676390726260285 79) (dy 21221853453985647954651 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 10468243676390726260285 79) (dy 21221853453985647954651 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3, 5, 1, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 10468243676390726260285 79) (dy 21221853453985647954651 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 2, 5, 1, 3], OutCert.sep (dy 13502316225371238712349 80) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 4, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 29769436482328244065287 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 4, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 13502316225371238712349 80) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 22708098623073481336609 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 4, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 18534820744060157809085 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 18534820744060157809085 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 244189404470623090583 74) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 4958220759672376526775 78)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 18534820744060157809085 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 8406709714355265220905 79) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 18088614546627827380719 80) (dy 18534820744060157809085 80)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 244189404470623090583 74) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 13502316225371238712349 80) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3, 5, 1, 3], OutCert.sep (dy 1259857015168078877615 77) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 4, 1, 3, 5, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 4, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 1, 3, 5, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0, 3, 5, 1, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 4, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 0, 2, 4, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 0, 2, 5, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 1, 3, 5, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 4, 0, 3, 4, 0], OutCert.sep (dy 244189404470623090583 74) (dy 16188010192386048742521 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 4, 0, 3, 5, 0], OutCert.sep (dy 244189404470623090583 74) (dy 16188010192386048742521 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 244189404470623090583 74) (dy 16188010192386048742521 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 244189404470623090583 74) (dy 15649293613715296009155 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 14526384399259018373579 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 244189404470623090583 74) (dy 16188010192386048742521 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 244189404470623090583 74) (dy 15649293613715296009155 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 14526384399259018373579 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 14526384399259018373579 80) (dy 14625047267991373871693 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 14526384399259018373579 80) (dy 14625047267991373871693 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 14138344125759842148411 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 2916417992808278007809 78) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 15128504843878715049505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 14138344125759842148411 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 3137610475515556755751 78) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 14138344125759842148411 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 6833918925373203645033 79)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 13502316225371238712349 80) (dy 6833918925373203645033 79)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 3137610475515556755751 78) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 2916417992808278007809 78) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 4, 0, 3, 5, 0], OutCert.sep (dy 2916417992808278007809 78) (dy 12348199206868946873665 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 3137610475515556755751 78) (dy 12773277794674294385677 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 3137610475515556755751 78) (dy 12773277794674294385677 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 2916417992808278007809 78) (dy 12348199206868946873665 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 2916417992808278007809 78) (dy 12348199206868946873665 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 2916417992808278007809 78) (dy 11937266698771184394421 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 2916417992808278007809 78) (dy 11937266698771184394421 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 5421637883445862791273 79) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 1, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 5421637883445862791273 79) (dy 11155972533299551062571 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 2, 5, 1, 3, 5, 1, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 5421637883445862791273 79) (dy 11155972533299551062571 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 4, 1, 2, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 13212989431621744731387 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 4, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 10784715826424560661491 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 4, 1, 3], OutCert.sep (dy 544242870048897088389 76) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 11540009506675578942777 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 10784715826424560661491 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 10784715826424560661491 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 2, 5, 1, 2, 4, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 10425814074887461966291 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 2, 5, 1, 2, 5, 0], OutCert.sep (dy 1259857015168078877615 77) (dy 10425814074887461966291 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 9368325854529610213769 80) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 2, 5, 1, 3], OutCert.sep (dy 544242870048897088389 76) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 10078856121344631020919 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 0, 2, 4, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 0, 2, 5, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 4, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 4, 0, 2, 5, 0, 3], OutCert.sep (dy 9368325854529610213769 80) (dy 294349841797256874579 75)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 4, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 4, 1, 3, 5, 0, 3], OutCert.sep (dy 8094005096193024371261 80) (dy 8226571260549332460505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 4, 0, 3], OutCert.sep (dy 9368325854529610213769 80) (dy 294349841797256874579 75)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 5, 0, 2, 5, 0, 3], OutCert.sep (dy 9368325854529610213769 80) (dy 294349841797256874579 75)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 5, 0, 3], OutCert.sep (dy 544242870048897088389 76) (dy 8802708581479327512213 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 5, 1, 3, 4, 0, 3], OutCert.sep (dy 8094005096193024371261 80) (dy 8226571260549332460505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 2, 5, 1, 3, 5, 0, 3], OutCert.sep (dy 8094005096193024371261 80) (dy 8226571260549332460505 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 0, 3], OutCert.sep (dy 3761700548972780477685 79) (dy 7688142130171819534765 80)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 1, 3, 5, 0, 2, 5, 0, 3], OutCert.sep (dy 6993023034689061455123 80) (dy 3592476594542739966129 79)),
  ([0, 2, 5, 0, 2, 5, 1, 3, 5, 0, 3, 5, 1, 3, 5, 1, 3, 5, 0, 3], OutCert.sep (dy 406252193381708509303 76) (dy 3357348983361985014709 79)),
  ([0, 2, 5, 0, 3, 4, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 3, 4, 1, 2, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 5, 0, 3, 4, 1, 3], OutCert.sep (dy 541303644785710933467 80) (dy 496377630869922078343 78)),
  ([0, 2, 5, 0, 3, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 270651822392855466733 74)),
  ([0, 2, 5, 0, 3, 5, 1, 2, 4, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 5, 0, 3, 5, 1, 2, 5, 0], OutCert.sep (dy 2807935910539478789959 79) (dy 5864507708225651694401 80)),
  ([0, 2, 5, 0, 3, 5, 1, 3], OutCert.sep (dy 541303644785710933467 80) (dy 496377630869922078343 78)),
  ([0, 3, 4, 0], OutCert.sep (dy 26087635650665564425 79) (dy 496377630869922078343 78)),
  ([0, 3, 5, 0], OutCert.sep (dy 26087635650665564425 79) (dy 496377630869922078343 78))]

set_option maxHeartbeats 4000000 in
noncomputable def cornerCerts : List (List ℕ × ℚ × ℚ) := [
  ([1, 3], (dy 26087635650665564425 80), (dy 26087635650665564425 79))]

theorem outside_ok : (outsideCerts.all fun x => outCheck (uvtBox x.1) x.2) = true := by
  decide +kernel

theorem corner_ok : (cornerCerts.all fun x => cornerCheck (uvtBox x.1) x.2.1 x.2.2) = true := by
  decide +kernel

/-- The certified lists are exactly the archived label-5 and label-12 leaves of the tree. -/
theorem structural_paths :
    (ArchTree.archTree.leaves.filter (fun x => x.2 = 5)).map Prod.fst = outsideCerts.map Prod.fst ∧
    (ArchTree.archTree.leaves.filter (fun x => x.2 = 12)).map Prod.fst = cornerCerts.map Prod.fst := by
  decide +kernel

/-- Every archived `outside` leaf (label 5) has empty physical image, hence `SemUVT` (vacuously). -/
theorem outside_leaves : ∀ q ∈ ArchTree.archTree.leaves, q.2 = 5 → SemUVT (uvtBox q.1) := by
  intro q hq hl k μ hin
  exfalso
  have hmem : q.1 ∈ outsideCerts.map Prod.fst := by
    rw [← structural_paths.1]
    exact List.mem_map.mpr ⟨q, List.mem_filter.mpr ⟨hq, by simpa using hl⟩, rfl⟩
  obtain ⟨x, hx, hxe⟩ := List.mem_map.mp hmem
  have hc := (List.all_eq_true.mp outside_ok) x hx
  rw [hxe] at hc
  exact outCheck_empty hc hin

theorem outside_oLeafOK :
    ∀ q ∈ ArchTree.archTree.leaves, q.2 = 5 → OCompact.OLeafOK (uvtBox q.1) :=
  fun q hq hl => OCompact.oLeafOK_of_semUVT _ (outside_leaves q hq hl)

/-- The archived `global_corner` leaf (label 12) lies in `a + (1 - b) ≤ 2^-13`: `OLeafOK` is vacuous. -/
theorem corner_oLeafOK :
    ∀ q ∈ ArchTree.archTree.leaves, q.2 = 12 → OCompact.OLeafOK (uvtBox q.1) := by
  intro q hq hl k μ _ _ _ _ _ hcor _ hin _
  exfalso
  have hmem : q.1 ∈ cornerCerts.map Prod.fst := by
    rw [← structural_paths.2]
    exact List.mem_map.mpr ⟨q, List.mem_filter.mpr ⟨hq, by simpa using hl⟩, rfl⟩
  obtain ⟨x, hx, hxe⟩ := List.mem_map.mp hmem
  have hc := (List.all_eq_true.mp corner_ok) x hx
  rw [hxe] at hc
  have := cornerCheck_sound hc hin
  linarith

end CKLaneD.Structural

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

View graph