MaxLeafFormal.RSCCheck

Source file MaxLeafFormal/RSCCheck.lean of the Lean project (how it is built).

import MaxLeafFormal.RSCParams

/-!
# Exact checkers for the RSC certificate

A hand-written mirror of the graded merge and of `Init~` at the RSC constants over natural
numbers with common denominators, and the Boolean checkers that the generated shard theorems run
(by `native_decide`, see `RSCFinal.lean`); their soundness theorems are kernel-checked.

A point is a pair `(N, D)` of eight natural numerators and a positive common denominator; its
value is `N / D`. Working with natural numbers keeps the kernel's work on GMP-accelerated literal
arithmetic (no rational normalisation).
-/

namespace MaxLeafFormal.RSCCheck

/-! ### Computable data -/

/-- Eight natural numerators and a common denominator. -/
abbrev IPt := List ℕ × ℕ

def zeroI : IPt := ([0, 0, 0, 0, 0, 0, 0, 0], 1)

/-- `P ∘̃ Q` at the RSC constants: all coefficients times `1000` are integers
(`2λ = 11/5`, `q₂ = 93/100`, `q₃ = 923/1000`), so the merge has denominator `1000 · D · E`. -/
def mergeN : List ℕ → List ℕ → List ℕ
  | [P0, P1, P2, P3, P4, P5, P6, P7], [Q0, _, Q2, Q3, Q4, Q5, Q6, Q7] =>
    let S := 2000 * Q0 + 2000 * Q2 + 2200 * Q3 + 1000 * Q4 + 1000 * Q5 + 930 * Q6 + 923 * Q7
    let Cs := 2000 * Q0
    let Cu := 2000 * Q3 + 1000 * Q4 + 1000 * Q5 + 1000 * Q6 + 930 * Q7
    let Os := 1000 * Q0
    let Ox := 1000 * Q3
    let Ou := 500 * Q4 + 1000 * Q5 + 1000 * Q6 + 930 * Q7
    [P0 * S, P1 * Cu, P2 * Cu + P1 * Cs, P3 * (Cu + Cs) + P2 * Cs, P4 * Ou,
      P5 * (Ou + Ox) + P4 * Ox, P6 * (Ou + Ox) + (P4 + P5) * Os, P7 * (Ou + Ox + Os) + P6 * Os]
  | _, _ => [0, 0, 0, 0, 0, 0, 0, 0]

def mergeI (P Q : IPt) : IPt := (mergeN P.1 Q.1, 1000 * P.2 * Q.2)

/-- `ê = eN / eD`. -/
def eN : ℕ := 145729958

def eD : ℕ := 189014575

/-- `ê^{-1-ν} Init~(ν; c₂, c₃)` at the RSC constants:
`(u·y/2, u·p₂/2, 0, 0, 2^{-ν} ϖ₂^{c₂} ϖ₃^{c₃}, 0, 0, 0) · ê^{-1-ν}` with `u = q₂^{c₂} q₃^{c₃}`,
over the common denominator `eN^{1+ν} · 200 · 100^{c₂} · 1000^{c₃} · 2^ν · 250000^{c₂+c₃}`. -/
def initI (ν c₂ c₃ : ℕ) : IPt :=
  let s := eD ^ (1 + ν)
  let uN := 93 ^ c₂ * 923 ^ c₃
  let uD := 100 ^ c₂ * 1000 ^ c₃
  let wN := 272657 ^ c₂ * 288677 ^ c₃
  let wD := 2 ^ ν * 250000 ^ (c₂ + c₃)
  let D := eN ^ (1 + ν) * 200 * uD * wD
  ([s * uN * 31 * wD, s * uN * 7 * wD, 0, 0, s * wN * 200 * uD, 0, 0, 0], D)

/-- `ê^{-(ν₀+2)} Init(∞) = ê^{-26} (y/2, p₂/2, 0, …, 0)`. -/
def initInfI : IPt := ([eD ^ 26 * 31, eD ^ 26 * 7, 0, 0, 0, 0, 0, 0], eN ^ 26 * 200)

/-- Membership of an integer vector in `𝒦_pos`, by peeling the leaves of the Hasse tree
(`O₂, O₀₀, C₀, O₁, C₁, O₀₁`). -/
def inK : List ℤ → Bool
  | [d0, d1, d2, d3, d4, d5, d6, d7] =>
    decide (0 ≤ d0) &&
      decide (0 ≤ d3 + min 0 (d2 + min 0 d1) + min 0 (d5 + min 0 d4 + min 0 (d6 + min 0 d7)))
  | _ => false

/-- Points in chunks of 32, for fast lookup in the kernel (structural recursion on a fuel bound). -/
def chunksAux : ℕ → List IPt → List (List IPt)
  | 0, _ => []
  | _, [] => []
  | n + 1, l@(_ :: _) => l.take 32 :: chunksAux n (l.drop 32)

def chunks32 (l : List IPt) : List (List IPt) := chunksAux l.length l

def getPt (Yc : List (List IPt)) (k : ℕ) : IPt := (Yc.getD (k / 32) []).getD (k % 32) zeroI

/-- Accumulate `∑ (aₖ/bₖ) · Y[kₖ]` as `(V, T)` with value `V / T`, and the weight sum as `s / t`. -/
def combI (Yc : List (List IPt)) : List (ℕ × ℕ × ℕ) → List ℕ × ℕ × ℕ × ℕ
  | [] => ([0, 0, 0, 0, 0, 0, 0, 0], 1, 0, 1)
  | (k, a, b) :: cs =>
    let r := combI Yc cs
    let y := getPt Yc k
    (List.zipWith (fun v n => v * (b * y.2) + a * n * r.2.1) r.1 y.1, r.2.1 * (b * y.2),
      r.2.2.1 * b + a * r.2.2.2, r.2.2.2 * b)

/-- The check of one condition of `prop:rsc-cert` for `P = M / F`: indices `< n`, denominators `> 0`, weight sum
`≥ 1`, and `M/F - ∑ (aₖ/bₖ) Y[kₖ] ∈ 𝒦_pos` (cleared of the positive denominator `F · T`). -/
def dom (n : ℕ) (Yc : List (List IPt)) (P : IPt) (comb : List (ℕ × ℕ × ℕ)) : Bool :=
  comb.all (fun e => decide (e.1 < n) && decide (0 < e.2.2)) &&
    (let r := combI Yc comb
     decide (r.2.2.2 ≤ r.2.2.1) &&
      inK (List.zipWith (fun m v => (m * r.2.1 : ℤ) - (P.2 * v : ℤ)) P.1 r.1))

/-- One stage block: for each `x` in `xs` and each `z` in `Zs`, `x ∘ z` dominates the given
combination of `Y` (of size `n`, chunked as `Yc`). -/
def checkBlock (n : ℕ) (Yc : List (List IPt)) (Zs : List IPt) (xs : List IPt)
    (combos : List (List (List (ℕ × ℕ × ℕ)))) : Bool :=
  xs.length == combos.length &&
    (xs.zip combos).all (fun xc => xc.2.length == Zs.length &&
      (Zs.zip xc.2).all (fun zc => dom n Yc (mergeI xc.1 zc.1) zc.2))

/-! ### Decoding the flat data -/

/-- Read `c` weight entries `(k, a, b)`. -/
def takeComb : ℕ → List ℕ → List (ℕ × ℕ × ℕ) × List ℕ
  | 0, l => ([], l)
  | c + 1, k :: a :: b :: l =>
    let r := takeComb c l
    ((k, a, b) :: r.1, r.2)
  | _ + 1, _ => ([], [])

/-- Read `m` combinations, each given as its length followed by its entries. -/
def decodeCombs : ℕ → List ℕ → List (List (ℕ × ℕ × ℕ))
  | 0, _ => []
  | _ + 1, [] => []
  | m + 1, c :: l =>
    let r := takeComb c l
    r.1 :: decodeCombs m r.2

/-- Read a point: eight numerators followed by the common denominator. -/
def decodePt : List ℕ → IPt
  | [a0, a1, a2, a3, a4, a5, a6, a7, d] => ([a0, a1, a2, a3, a4, a5, a6, a7], d)
  | _ => zeroI

/-- Read a leaf entry: `ν, c₂, c₃`, then one combination. -/
def decodeLeaf : List ℕ → (ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ)
  | ν :: c₂ :: c₃ :: c :: l => ((ν, c₂, c₃), (takeComb c l).1)
  | _ => ((0, 0, 0), [])

/-- Read a chain of length one: `ν, c₂, c₃`, then `n` combinations. -/
def decodeChain1 (n : ℕ) : List ℕ → (ℕ × ℕ × ℕ) × List (List (ℕ × ℕ × ℕ))
  | ν :: c₂ :: c₃ :: l => ((ν, c₂, c₃), decodeCombs n l)
  | _ => ((0, 0, 0), [])

/-! ### Family checkers -/

def okPt (P : IPt) : Bool := P.1.length == 8 && decide (0 < P.2)

def okPts (Y : List IPt) : Bool := Y.all okPt

/-- `2000 · D · fin~(N / D)`, with `fin~ = A + C₂ + O₀₀/2 + O₀₁ + O₁ + q₂ O₂`. -/
def finN : List ℕ → ℕ
  | [N0, _, _, N3, N4, N5, N6, N7] =>
    2000 * N0 + 2000 * N3 + 1000 * N4 + 2000 * N5 + 2000 * N6 + 1860 * N7
  | _ => 0

/-- Strict lexicographic order of the values `N / D`, `N' / D'` (cross-multiplied). -/
def ltLex (D D' : ℕ) : List ℕ → List ℕ → Bool
  | a :: as, b :: bs => decide (a * D' < b * D) || (decide (a * D' = b * D) && ltLex D D' as bs)
  | _, _ => false

def sortedZ : List IPt → Bool
  | P :: Q :: rest => ltLex P.2 Q.2 P.1 Q.1 && sortedZ (Q :: rest)
  | _ => true

/-- The facts about `Z` itself: `1024` well-formed points in strictly increasing lexicographic
order, each with `fin~ > 0.6060`. -/
def checkZ (Z : List IPt) : Bool :=
  Z.length == 1024 && okPts Z && sortedZ Z &&
    Z.all (fun z => decide (6060 * 2000 * z.2 < 10000 * finN z.1))

/-- (C2): `ê^{-1-ν} Init(ν)` for `ν ≤ 24` (entries `0, …, 24`) and `ê^{-26} Init(∞)` (entry `25`). -/
def checkC2 (n : ℕ) (Yc : List (List IPt)) (combos : List (List (ℕ × ℕ × ℕ))) : Bool :=
  combos.length == 26 &&
    ((List.range 25).zip combos).all (fun e => dom n Yc (initI e.1 0 0) e.2) &&
    dom n Yc initInfI (combos.getD 25 [])

/-- Leaf entries `((ν, c₂, c₃), comb)`: `ê^{-1-ν} Init~(ν; c₂, c₃)` dominates `comb`. -/
def checkLeaves (n : ℕ) (Yc : List (List IPt)) (entries : List ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ))) :
    Bool :=
  entries.all (fun e => dom n Yc (initI e.1.1 e.1.2.1 e.1.2.2) e.2)

/-- Chains of length one `((ν, c₂, c₃), combos)`: `ê^{-1-ν} Init~(ν; c₂, c₃) ∘̃ z` dominates the
given combination of `Z` for every `z ∈ Z`. -/
def checkChain1 (n : ℕ) (Yc : List (List IPt)) (Zs : List IPt)
    (entries : List ((ℕ × ℕ × ℕ) × List (List (ℕ × ℕ × ℕ)))) : Bool :=
  entries.all (fun e => checkBlock n Yc Zs [initI e.1.1 e.1.2.1 e.1.2.2] [e.2])

/-- `u = q₂^{c₂} q₃^{c₃}` and `w = ϖ₂^{c₂} ϖ₃^{c₃}` as numerator/denominator pairs. -/
def uF (c₂ c₃ : ℕ) : ℕ × ℕ := (93 ^ c₂ * 923 ^ c₃, 100 ^ c₂ * 1000 ^ c₃)

def wF (c₂ c₃ : ℕ) : ℕ × ℕ := (272657 ^ c₂ * 288677 ^ c₃, 250000 ^ (c₂ + c₃))

/-- The target chain length `j` of (C5) at `(ν, c₂, c₃)`, from the paper's `d_min`. -/
def jTarget (ν c₂ : ℕ) : ℕ := if c₂ = 0 then RSCCert.jOf RSCParams.d₃ ν else RSCCert.jOf RSCParams.d₂ ν

/-- The lattice of (C5): `1 ≤ ν ≤ 36`, `1 ≤ c₂ + c₃ ≤ ν`, in a fixed order. -/
def lattice5 : List (ℕ × ℕ × ℕ) :=
  (List.range 36).flatMap fun i =>
    (List.range (i + 2)).flatMap fun c₂ =>
      ((List.range (i + 2 - c₂)).filter (fun c₃ => decide (1 ≤ c₂ + c₃))).map fun c₃ => (i + 1, c₂, c₃)

/-- The lattice of (C4): `4 ≤ ν ≤ 36` (exactly the `2 ≤ ν ≤ 36` with `d₃ ν ≤ 1`) and
`1 ≤ c₂ + c₃ ≤ ν - 1`. -/
def lattice4 : List (ℕ × ℕ × ℕ) :=
  (List.range 33).flatMap fun i =>
    (List.range (i + 4)).flatMap fun c₂ =>
      ((List.range (i + 4 - c₂)).filter (fun c₃ => decide (1 ≤ c₂ + c₃))).map fun c₃ => (i + 4, c₂, c₃)

/-- Read `m` combination components `(kind, idx, a, b)` with `λ = a / b`. -/
def takeComp : ℕ → List ℕ → List (ℕ × ℕ × ℕ × ℕ)
  | 0, _ => []
  | m + 1, k :: i :: a :: b :: l => (k, i, a, b) :: takeComp m l
  | _ + 1, _ => []

/-- A convex-combination witness, components `((c₂', c₃'), a, b)` with `λ = a / b`:
`b > 0`, `∑ λ = 1`, `∑ λ u' = u`, `∑ λ w' = w`, all exactly. -/
def combWitness (c₂ c₃ : ℕ) (comps : List ((ℕ × ℕ) × ℕ × ℕ)) : Bool :=
  comps.all (fun e => decide (0 < e.2.2)) &&
  (let S := comps.foldr (fun e r => (r.1 * e.2.2 + e.2.1 * r.2, r.2 * e.2.2)) (0, 1)
   decide (S.1 = S.2)) &&
  (let u := uF c₂ c₃
   let S := comps.foldr (fun e r =>
     let uk := uF e.1.1 e.1.2
     (r.1 * (e.2.2 * uk.2) + e.2.1 * uk.1 * r.2, r.2 * (e.2.2 * uk.2))) (0, 1)
   decide (S.1 * u.2 = u.1 * S.2)) &&
  (let w := wF c₂ c₃
   let S := comps.foldr (fun e r =>
     let wk := wF e.1.1 e.1.2
     (r.1 * (e.2.2 * wk.2) + e.2.1 * wk.1 * r.2, r.2 * (e.2.2 * wk.2))) (0, 1)
   decide (S.1 * w.2 = w.1 * S.2))

/-- The exposure counts of component `e`: kind `0` is `(0, 0)`, otherwise entry `idx` of `T`. -/
def compPt {α : Type} (T : List ((ℕ × ℕ × ℕ) × α)) (d : α) (e : ℕ × ℕ × ℕ × ℕ) : ℕ × ℕ :=
  if e.1 = 0 then (0, 0) else ((T.getD e.2.1 ((0, 0, 0), d)).1.2.1, (T.getD e.2.1 ((0, 0, 0), d)).1.2.2)

/-- (C5) lattice check against the table `T` of certified chains (entries `((ν, c₂, c₃), j)`).
Per lattice point the data is `[0, k]` (entry `k` of `T` is this point, with `j ≤ jTarget`) or
`[1, m, kind₁, idx₁, a₁, b₁, …]` (a convex combination of `(0, 0)` (kind `0`) and entries of `T`
(kind `1`) at the same `ν` with `j ≤ jTarget`). -/
def latOK5 (T : List ((ℕ × ℕ × ℕ) × ℕ)) (pt : ℕ × ℕ × ℕ) (dat : List ℕ) : Bool :=
  match dat with
  | [0, k] => decide (k < T.length) && decide ((T.getD k ((0, 0, 0), 0)).1 = pt) &&
      decide ((T.getD k ((0, 0, 0), 0)).2 ≤ jTarget pt.1 pt.2.1)
  | 1 :: m :: rest =>
    let comps := takeComp m rest
    comps.all (fun e => decide (e.1 = 0) ||
      (decide (e.1 = 1) && decide (e.2.1 < T.length) &&
        decide ((T.getD e.2.1 ((0, 0, 0), 0)).1.1 = pt.1) &&
        decide ((T.getD e.2.1 ((0, 0, 0), 0)).2 ≤ jTarget pt.1 pt.2.1))) &&
    combWitness pt.2.1 pt.2.2 (comps.map fun e => (compPt T 0 e, e.2.2.1, e.2.2.2))
  | _ => false

def checkLattice5 (T : List ((ℕ × ℕ × ℕ) × ℕ)) (wit : List (List ℕ)) : Bool :=
  lattice5.length == wit.length && (lattice5.zip wit).all (fun e => latOK5 T e.1 e.2)

/-- (C4) lattice check against the table `T` of certified leaves (entries `((ν, c₂, c₃), ())`),
in the same data format; components are `(0, 0)` or leaves at the same `ν`. -/
def latOK4 (T : List ((ℕ × ℕ × ℕ) × Unit)) (pt : ℕ × ℕ × ℕ) (dat : List ℕ) : Bool :=
  match dat with
  | [0, k] => decide (k < T.length) && decide ((T.getD k ((0, 0, 0), ())).1 = pt)
  | 1 :: m :: rest =>
    let comps := takeComp m rest
    comps.all (fun e => decide (e.1 = 0) ||
      (decide (e.1 = 1) && decide (e.2.1 < T.length) &&
        decide ((T.getD e.2.1 ((0, 0, 0), ())).1.1 = pt.1))) &&
    combWitness pt.2.1 pt.2.2 (comps.map fun e => (compPt T () e, e.2.2.1, e.2.2.2))
  | _ => false

def checkLattice4 (T : List ((ℕ × ℕ × ℕ) × Unit)) (wit : List (List ℕ)) : Bool :=
  lattice4.length == wit.length && (lattice4.zip wit).all (fun e => latOK4 T e.1 e.2)

/-! ### Real-valued semantics -/

open MaxLeafFormal.RSCCert MaxLeafFormal.RSCParams
open MaxLeafFormal.Antinorm8 (Kpos PZ initInf)
open Pointwise

noncomputable section

/-- The value `N / D` of a point. -/
def val (P : IPt) : Fin 8 → ℝ := fun s => ((P.1.getD s 0 : ℕ) : ℝ) / (P.2 : ℝ)

/-- The finite set of values of a list of points. -/
def finsetOf (Y : List IPt) : Finset (Fin 8 → ℝ) :=
  open Classical in (Y.map val).toFinset

/-- `x ∘̃ z ∈ conv(Y') + 𝒦_pos` for all `x ∈ X`, `z ∈ Z` (one stage of a chain). -/
def StageFact (Z X Y' : List IPt) : Prop :=
  ∀ x ∈ X, ∀ z ∈ Z, merge p₂ p₃ (val x) (val z) ∈ convexHull ℝ (finsetOf Y' : Set (Fin 8 → ℝ)) + Kpos

/-- (C5) for one exposure point with chains of length `j`. -/
def ChainFact (Z : List IPt) (e : (ℕ × ℕ × ℕ) × ℕ) : Prop :=
  ∀ Qs : List (Fin 8 → ℝ), Qs.length = e.2 → (∀ Q ∈ Qs, Q ∈ PZ (finsetOf Z) ∧ 0 ≤ Q) →
    Qs.foldl (merge p₂ p₃) ((ê ^ (1 + e.1.1))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ e.1.1 e.1.2.1 e.1.2.2)
      ∈ PZ (finsetOf Z)

/-- (C4) for one leaf exposure point. -/
def LeafFact (Z : List IPt) (e : (ℕ × ℕ × ℕ) × Unit) : Prop :=
  init p₂ p₃ y ϖ₂ ϖ₃ e.1.1 e.1.2.1 e.1.2.2 ∈ ê ^ (1 + e.1.1) • PZ (finsetOf Z)

/-! ### Soundness -/

theorem val_nonneg (P : IPt) : 0 ≤ val P := fun _ => div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)

theorem okPt_parts_aux {P : IPt} (h : okPt P = true) :
    ∃ a0 a1 a2 a3 a4 a5 a6 a7 D : ℕ, P = ([a0, a1, a2, a3, a4, a5, a6, a7], D) ∧ 0 < D := by
  obtain ⟨N, D⟩ := P
  unfold okPt at h
  simp only [Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq] at h
  obtain ⟨hl, hD⟩ := h
  rcases N with _ | ⟨a0, _ | ⟨a1, _ | ⟨a2, _ | ⟨a3, _ | ⟨a4, _ | ⟨a5, _ | ⟨a6, _ | ⟨a7, _ | ⟨a8, N⟩⟩⟩⟩⟩⟩⟩⟩⟩
  all_goals first
    | exact ⟨_, _, _, _, _, _, _, _, D, rfl, hD⟩
    | (simp only [List.length_cons, List.length_nil] at hl; omega)

theorem ehat_eq : ê = (eN : ℝ) / (eD : ℝ) := by
  unfold ê eN eD; norm_num

theorem val_mergeI {P Q : IPt} (hP : okPt P = true) (hQ : okPt Q = true) :
    val (mergeI P Q) = merge p₂ p₃ (val P) (val Q) := by
  obtain ⟨a0, a1, a2, a3, a4, a5, a6, a7, D, rfl, hD⟩ := okPt_parts_aux hP
  obtain ⟨b0, b1, b2, b3, b4, b5, b6, b7, E, rfl, hE⟩ := okPt_parts_aux hQ
  have hD' : (D : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hD.ne'
  have hE' : (E : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hE.ne'
  funext s
  fin_cases s <;>
  simp [val, mergeI, mergeN, MaxLeafFormal.RSCCert.merge, MaxLeafFormal.RSCCert.chiS,
    MaxLeafFormal.Antinorm8.chiCu, MaxLeafFormal.Antinorm8.chiCs, MaxLeafFormal.Antinorm8.chiOs,
    MaxLeafFormal.Antinorm8.chiOx, MaxLeafFormal.Antinorm8.chiOu, p₂, p₃] <;>
  push_cast <;> field_simp <;> ring

theorem okPt_mergeI {P Q : IPt} (hP : okPt P = true) (hQ : okPt Q = true) :
    okPt (mergeI P Q) = true := by
  obtain ⟨a0, a1, a2, a3, a4, a5, a6, a7, D, rfl, hD⟩ := okPt_parts_aux hP
  obtain ⟨b0, b1, b2, b3, b4, b5, b6, b7, E, rfl, hE⟩ := okPt_parts_aux hQ
  have hpos : 0 < 1000 * D * E := Nat.mul_pos (Nat.mul_pos (by norm_num) hD) hE
  simp [okPt, mergeI, mergeN, hpos]

theorem val_initI (ν c₂ c₃ : ℕ) :
    val (initI ν c₂ c₃) = (ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ := by
  rw [ehat_eq]
  funext s
  fin_cases s <;>
  norm_num [val, initI, init, eN, eD, p₂, p₃, y, ϖ₂, ϖ₃, div_pow, inv_pow, mul_pow] <;>
  field_simp <;> ring

theorem okPt_initI (ν c₂ c₃ : ℕ) : okPt (initI ν c₂ c₃) = true := by
  have hD : 0 < eN ^ (1 + ν) * 200 * (100 ^ c₂ * 1000 ^ c₃) * (2 ^ ν * 250000 ^ (c₂ + c₃)) := by
    unfold eN; positivity
  simpa [okPt, initI] using hD

theorem val_initInfI : val initInfI = (ê ^ (ν₀ + 2))⁻¹ • initInf p₂ y := by
  rw [ehat_eq]
  funext s
  fin_cases s <;>
  norm_num [val, initInfI, initInf, eN, eD, ν₀, p₂, y, div_pow, inv_pow, mul_pow] <;>
  field_simp <;> ring

theorem okPt_initInfI : okPt initInfI = true := by
  have hD : 0 < eN ^ 26 * 200 := by unfold eN; positivity
  simpa [okPt, initInfI] using hD

/-- Peeling construction: a point with `P 0 ≥ 0` and the `e₃`-coefficient nonnegative is in `Kpos`. -/
theorem kpos_of_peel (P : Fin 8 → ℝ) (h0 : 0 ≤ P 0)
    (h3 : 0 ≤ P 3 + min 0 (cgS2 P) + min 0 (cgS5 P)) : P ∈ Kpos := by
  have kA : ∀ x : ℝ, max 0 x - max 0 (-x) = x := by
    intro x
    rcases le_total 0 x with h | h
    · rw [max_eq_right h, max_eq_left (by linarith)]; ring
    · rw [max_eq_left h, max_eq_right (by linarith)]; ring
  have kB : ∀ x : ℝ, min 0 x + max 0 (-x) = 0 := by
    intro x
    rcases le_total 0 x with h | h
    · rw [min_eq_left h, max_eq_left (by linarith)]; ring
    · rw [min_eq_right h, max_eq_right (by linarith)]; ring
  have hS2 : cgS2 P = P 2 + min 0 (P 1) := rfl
  have hS6 : cgS6 P = P 6 + min 0 (P 7) := rfl
  have hS5 : cgS5 P = P 5 + min 0 (P 4) + min 0 (cgS6 P) := rfl
  refine Kpos_of_gen P ⟨![P 0, max 0 (P 1), max 0 (cgS2 P), P 3 + min 0 (cgS2 P) + min 0 (cgS5 P),
    max 0 (P 4), max 0 (cgS5 P), max 0 (cgS6 P), max 0 (P 7), max 0 (-cgS2 P), max 0 (-P 1),
    max 0 (-cgS5 P), max 0 (-P 4), max 0 (-cgS6 P), max 0 (-P 7)], ?_, ?_⟩
  · intro i
    fin_cases i <;> first | exact h0 | exact le_max_left _ _ | exact h3
  · funext k
    fin_cases k <;> simp [Fin.sum_univ_succ, gen, unitVec] <;>
      linarith [kA (cgS2 P), kA (P 1), kA (P 4), kA (cgS5 P), kA (cgS6 P), kA (P 7),
        kB (cgS2 P), kB (P 1), kB (cgS5 P), kB (P 4), kB (cgS6 P), kB (P 7), hS2, hS5, hS6]

theorem inK_sound {v : List ℤ} (h : inK v = true) :
    (fun s : Fin 8 => ((v.getD s 0 : ℤ) : ℝ)) ∈ Kpos := by
  rcases v with _ | ⟨d0, _ | ⟨d1, _ | ⟨d2, _ | ⟨d3, _ | ⟨d4, _ | ⟨d5, _ | ⟨d6, _ | ⟨d7, _ | ⟨d8, vs⟩⟩⟩⟩⟩⟩⟩⟩⟩
  all_goals try (simp [inK] at h; done)
  case cons.cons.cons.cons.cons.cons.cons.cons.nil =>
  simp only [inK, Bool.and_eq_true, decide_eq_true_eq] at h
  obtain ⟨h0, h3⟩ := h
  apply kpos_of_peel
  · show (0:ℝ) ≤ (d0:ℝ)
    exact_mod_cast h0
  · show (0:ℝ) ≤ (d3:ℝ) + min 0 ((d2:ℝ) + min 0 (d1:ℝ))
        + min 0 ((d5:ℝ) + min 0 (d4:ℝ) + min 0 ((d6:ℝ) + min 0 (d7:ℝ)))
    exact_mod_cast h3

theorem getPt_chunksAux_aux (n : ℕ) : ∀ (l : List IPt), l.length ≤ n →
    ∀ k (hk : k < l.length), getPt (chunksAux n l) k = l[k] := by
  induction n with
  | zero => intro l hl k hk; omega
  | succ n ih =>
    intro l hl k hk
    match l, hl, hk with
    | [], _, hk => simp at hk
    | x :: xs, hl, hk =>
      simp only [chunksAux]
      unfold getPt
      by_cases hk32 : k < 32
      · have h1 : k / 32 = 0 := by omega
        have h2 : k % 32 = k := by omega
        rw [h1, h2, List.getD_cons_zero]
        rw [List.getD_eq_getElem]
        · exact List.getElem_take
        · simp only [List.length_take, List.length_cons] at hk ⊢
          omega
      · have h1 : k / 32 = (k - 32) / 32 + 1 := by omega
        have h2 : k % 32 = (k - 32) % 32 := by omega
        rw [h1, h2, List.getD_cons_succ]
        have key := ih (List.drop 32 (x :: xs)) (by simp only [List.length_drop, List.length_cons] at hl ⊢; omega)
          (k - 32) (by simp only [List.length_drop, List.length_cons] at hk ⊢; omega)
        unfold getPt at key
        rw [key]
        simp only [List.getElem_drop]
        congr 1
        omega

theorem getPt_chunks32 (Y : List IPt) (k : ℕ) (hk : k < Y.length) :
    getPt (chunks32 Y) k = Y[k] := by
  unfold chunks32
  exact getPt_chunksAux_aux Y.length Y le_rfl k hk

theorem dom_aux_okdims {P : IPt} (h : okPt P = true) : P.1.length = 8 ∧ 0 < P.2 := by
  unfold okPt at h
  simpa only [Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq] using h

theorem dom_aux_getD {α β γ : Type} (f : β → γ → α) (d : α) (d1 : β) (d2 : γ) (l : List β)
    (l' : List γ) (hl : l.length = 8) (hl' : l'.length = 8) (s : ℕ) (hs : s < 8) :
    (List.zipWith f l l').getD s d = f (l.getD s d1) (l'.getD s d2) := by
  have h1 : s < l.length := by omega
  have h2 : s < l'.length := by omega
  have h3 : s < (List.zipWith f l l').length := by
    rw [List.length_zipWith, hl, hl']; omega
  rw [List.getD_eq_getElem _ _ h3, List.getD_eq_getElem _ _ h1, List.getD_eq_getElem _ _ h2,
    List.getElem_zipWith]

theorem dom_aux_coe (l : List ℕ) :
    (do let a ← l; pure (a : ℤ) : List ℤ) = l.map (fun a : ℕ => (a : ℤ)) := by
  induction l with
  | nil => rfl
  | cons x xs ih => rw [List.map_cons, ← ih]; rfl

theorem dom_aux_map_getD (l : List ℕ) (s : ℕ) (hs : s < l.length) :
    (l.map (fun a : ℕ => (a : ℤ))).getD s 0 = ((l.getD s 0 : ℕ) : ℤ) := by
  rw [List.getD_eq_getElem _ _ (show s < (l.map (fun a : ℕ => (a : ℤ))).length by simpa using hs),
    List.getD_eq_getElem _ _ hs, List.getElem_map]

theorem dom_aux_spec (Yc : List (List IPt)) : ∀ comb : List (ℕ × ℕ × ℕ),
    (∀ e ∈ comb, 0 < e.2.2 ∧ okPt (getPt Yc e.1) = true) →
    0 < (combI Yc comb).2.1 ∧ 0 < (combI Yc comb).2.2.2 ∧ (combI Yc comb).1.length = 8 ∧
    (fun s : Fin 8 => (((combI Yc comb).1.getD s 0 : ℕ) : ℝ) / ((combI Yc comb).2.1 : ℝ)) =
      (comb.map fun e => ((e.2.1 : ℝ) / e.2.2) • val (getPt Yc e.1)).sum ∧
    (((combI Yc comb).2.2.1 : ℝ) / ((combI Yc comb).2.2.2 : ℝ)) =
      (comb.map fun e => (e.2.1 : ℝ) / e.2.2).sum := by
  intro comb
  induction comb with
  | nil =>
    intro _
    refine ⟨by simp [combI], by simp [combI], by simp [combI], ?_, by simp [combI]⟩
    funext s
    fin_cases s <;> simp [combI]
  | cons e cs ih =>
    obtain ⟨k, a, b⟩ := e
    intro h
    have hb : 0 < b := by
      have := (h (k, a, b) (by simp)).1
      simpa using this
    have hy : okPt (getPt Yc k) = true := (h (k, a, b) (by simp)).2
    obtain ⟨hT', ht', hl', hV', hs'⟩ := ih (fun e he => h e (by simp [he]))
    obtain ⟨hyl, hyp⟩ := dom_aux_okdims hy
    simp only [combI]
    generalize combI Yc cs = r at hT' ht' hl' hV' hs' ⊢
    have hT0 : (r.2.1 : ℝ) ≠ 0 := by exact_mod_cast hT'.ne'
    have hb0 : (b : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
    have hy0 : ((getPt Yc k).2 : ℝ) ≠ 0 := by exact_mod_cast hyp.ne'
    have ht0 : (r.2.2.2 : ℝ) ≠ 0 := by exact_mod_cast ht'.ne'
    refine ⟨Nat.mul_pos hT' (Nat.mul_pos hb hyp), Nat.mul_pos ht' hb, ?_, ?_, ?_⟩
    · rw [List.length_zipWith, hl', hyl, min_self]
    · funext s
      rw [dom_aux_getD _ _ 0 0 _ _ hl' hyl s.1 s.isLt]
      have hVs := congrFun hV' s
      simp only [List.map_cons, List.sum_cons, Pi.add_apply, Pi.smul_apply, smul_eq_mul, val] at hVs ⊢
      rw [← hVs]
      push_cast
      field_simp
      ring
    · simp only [List.map_cons, List.sum_cons]
      rw [← hs']
      push_cast
      field_simp
      ring

theorem dom_aux_conv {α : Type} (C : Set (Fin 8 → ℝ)) (hC : Convex ℝ C) (x0 : Fin 8 → ℝ)
    (hx0 : x0 ∈ C) (f : α → ℝ) (g : α → Fin 8 → ℝ) (L : List α)
    (hL : ∀ a ∈ L, 0 ≤ f a ∧ g a ∈ C) :
    ∃ c ∈ C, (L.map fun a => f a • g a).sum = (L.map f).sum • c := by
  induction L with
  | nil => exact ⟨x0, hx0, by simp⟩
  | cons a L ih =>
    obtain ⟨c', hc', hsum⟩ := ih (fun b hb => hL b (List.mem_cons_of_mem _ hb))
    obtain ⟨ha, hga⟩ := hL a (List.mem_cons_self ..)
    have hμ : 0 ≤ (L.map f).sum := List.sum_nonneg (fun x hx => by
      obtain ⟨b, hb, rfl⟩ := List.mem_map.mp hx
      exact (hL b (List.mem_cons_of_mem _ hb)).1)
    by_cases hz : f a + (L.map f).sum = 0
    · have h1 : f a = 0 := by linarith
      have h2 : (L.map f).sum = 0 := by linarith
      refine ⟨x0, hx0, ?_⟩
      simp only [List.map_cons, List.sum_cons]
      rw [hsum]
      simp [h1, h2]
    · have hw : 0 < f a + (L.map f).sum := lt_of_le_of_ne (add_nonneg ha hμ) (Ne.symm hz)
      have hw' : f a + (L.map f).sum ≠ 0 := hw.ne'
      refine ⟨(f a / (f a + (L.map f).sum)) • g a +
        ((L.map f).sum / (f a + (L.map f).sum)) • c', ?_, ?_⟩
      · exact hC hga hc' (div_nonneg ha hw.le) (div_nonneg hμ hw.le)
          (by rw [← add_div, div_self hw'])
      · have e1 : (f a + (L.map f).sum) * (f a / (f a + (L.map f).sum)) = f a := by
          field_simp
        have e2 : (f a + (L.map f).sum) * ((L.map f).sum / (f a + (L.map f).sum)) =
            (L.map f).sum := by
          field_simp
        simp only [List.map_cons, List.sum_cons]
        rw [hsum, smul_add, smul_smul, smul_smul, e1, e2]

theorem dom_aux_val_mem (Y : List IPt) (k : ℕ) (hk : k < Y.length) :
    val (getPt (chunks32 Y) k) ∈ convexHull ℝ (finsetOf Y : Set (Fin 8 → ℝ)) := by
  rw [getPt_chunks32 Y k hk]
  have hm : val (Y[k]) ∈ finsetOf Y := by
    unfold finsetOf
    exact List.mem_toFinset.mpr (List.mem_map_of_mem (List.getElem_mem ..))
  exact subset_convexHull ℝ _ (Finset.mem_coe.mpr hm)

theorem dom_aux_nonneg (Y : List IPt) : ∀ y ∈ finsetOf Y, 0 ≤ y := by
  intro y hy
  unfold finsetOf at hy
  obtain ⟨p, _, rfl⟩ := List.mem_map.mp (List.mem_toFinset.mp hy)
  exact val_nonneg p

/-- The domination check is sound: `P ∈ conv(Y) + 𝒦_pos`. -/
theorem dom_sound {Y : List IPt} (hY : okPts Y = true) {P : IPt} (hP : okPt P = true)
    {comb : List (ℕ × ℕ × ℕ)} (h : dom Y.length (chunks32 Y) P comb = true) :
    val P ∈ convexHull ℝ (finsetOf Y : Set (Fin 8 → ℝ)) + Kpos := by
  have hne : ∃ e, e ∈ comb := by
    cases comb with
    | nil => simp [dom, combI] at h
    | cons e cs => exact ⟨e, by simp⟩
  have hY' : Y.all okPt = true := hY
  have hcomb : ∀ e ∈ comb, e.1 < Y.length ∧ 0 < e.2.2 := by
    intro e he
    have h1 := h
    unfold dom at h1
    rw [Bool.and_eq_true] at h1
    have h2 := List.all_eq_true.mp h1.1 e he
    simpa using h2
  have hrest := h
  unfold dom at hrest
  rw [Bool.and_eq_true] at hrest
  obtain ⟨-, hK⟩ := hrest
  simp only [Bool.and_eq_true, decide_eq_true_eq] at hK
  obtain ⟨hle, hKin⟩ := hK
  have hpts : ∀ e ∈ comb, okPt (getPt (chunks32 Y) e.1) = true := by
    intro e he
    have hk := (hcomb e he).1
    rw [getPt_chunks32 Y _ hk]
    exact List.all_eq_true.mp hY' _ (List.getElem_mem ..)
  obtain ⟨hT, ht, hVl, hV, hst⟩ :=
    dom_aux_spec (chunks32 Y) comb (fun e he => ⟨(hcomb e he).2, hpts e he⟩)
  obtain ⟨hPl, hPpos⟩ := dom_aux_okdims hP
  set r := combI (chunks32 Y) comb with hr
  have hD0 : (P.2 : ℝ) ≠ 0 := by exact_mod_cast hPpos.ne'
  have hT0 : (r.2.1 : ℝ) ≠ 0 := by exact_mod_cast hT.ne'
  have ht' : (0 : ℝ) < (r.2.2.2 : ℝ) := by exact_mod_cast ht
  have hKW : (fun s : Fin 8 => ((P.1.getD s 0 : ℕ) : ℝ) * (r.2.1 : ℝ) -
      (P.2 : ℝ) * ((r.1.getD s 0 : ℕ) : ℝ)) ∈ Kpos := by
    rw [dom_aux_coe, dom_aux_coe] at hKin
    have hA : (P.1.map (fun a : ℕ => (a : ℤ))).length = 8 := by simp [hPl]
    have hB : (r.1.map (fun a : ℕ => (a : ℤ))).length = 8 := by simp [hVl]
    convert MaxLeafFormal.RSCCheck.inK_sound hKin using 1
    funext s
    have hsP : s.1 < P.1.length := by omega
    have hsV : s.1 < r.1.length := by omega
    rw [dom_aux_getD _ _ 0 0 _ _ hA hB s.1 s.isLt, dom_aux_map_getD _ _ hsP,
      dom_aux_map_getD _ _ hsV]
    push_cast
    ring
  have hV' : ∀ s : Fin 8, ((r.1.getD s 0 : ℕ) : ℝ) / (r.2.1 : ℝ) = (comb.map fun e =>
      ((e.2.1 : ℝ) / e.2.2) • val (getPt (chunks32 Y) e.1)).sum s := fun s => congrFun hV s
  obtain ⟨x0, hx0⟩ : ∃ x0, x0 ∈ convexHull ℝ (finsetOf Y : Set (Fin 8 → ℝ)) := by
    obtain ⟨e, he⟩ := hne
    exact ⟨_, dom_aux_val_mem Y _ (hcomb e he).1⟩
  obtain ⟨c, hcC, hcS⟩ := dom_aux_conv (convexHull ℝ (finsetOf Y : Set (Fin 8 → ℝ)))
    (convex_convexHull ℝ _) _ hx0 (fun e : ℕ × ℕ × ℕ => (e.2.1 : ℝ) / e.2.2)
    (fun e => val (getPt (chunks32 Y) e.1)) comb
    (fun e he => ⟨div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _),
      dom_aux_val_mem Y _ (hcomb e he).1⟩)
  have hσ : 1 ≤ (comb.map fun e => (e.2.1 : ℝ) / e.2.2).sum := by
    rw [← hst]
    exact (one_le_div ht').mpr (by exact_mod_cast hle)
  have hc0 : 0 ≤ c := MaxLeafFormal.Antinorm8.convexHull_nonneg (dom_aux_nonneg Y) hcC
  set σ := (comb.map fun e => (e.2.1 : ℝ) / e.2.2).sum with hσdef
  set S := (comb.map fun e => ((e.2.1 : ℝ) / e.2.2) • val (getPt (chunks32 Y) e.1)).sum
    with hSdef
  have hVs : ∀ s : Fin 8, ((r.1.getD s 0 : ℕ) : ℝ) / (r.2.1 : ℝ) = S s := hV'
  have hDiff : val P - S ∈ Kpos := by
    have hEq : val P - S = (1 / ((P.2 : ℝ) * (r.2.1 : ℝ))) •
        (fun s : Fin 8 => ((P.1.getD s 0 : ℕ) : ℝ) * (r.2.1 : ℝ) -
          (P.2 : ℝ) * ((r.1.getD s 0 : ℕ) : ℝ)) := by
      funext s
      have := hVs s
      simp only [Pi.sub_apply, Pi.smul_apply, smul_eq_mul, val]
      rw [← this]
      field_simp
    rw [hEq]
    exact MaxLeafFormal.Antinorm8.Kpos_smul (by positivity) hKW
  have hSc : S - c = (σ - 1) • c := by
    rw [hcS, sub_smul, one_smul]
  have hSK : S - c ∈ Kpos := by
    rw [hSc]
    apply MaxLeafFormal.Antinorm8.Kpos_of_nonneg
    rw [Pi.le_def]
    intro s
    simp only [Pi.zero_apply, Pi.smul_apply, smul_eq_mul]
    exact mul_nonneg (by linarith) (hc0 s)
  have key : val P = c + ((val P - S) + (S - c)) := by abel
  rw [key]
  exact Set.add_mem_add hcC (MaxLeafFormal.Antinorm8.Kpos_add hDiff hSK)

theorem checkBlock_sound {Y Zs xs : List IPt} (hY : okPts Y = true) (hZs : okPts Zs = true)
    (hxs : okPts xs = true) {combos : List (List (List (ℕ × ℕ × ℕ)))}
    (h : checkBlock Y.length (chunks32 Y) Zs xs combos = true) : StageFact Zs xs Y := by
  unfold StageFact
  unfold checkBlock at h
  simp only [Bool.and_eq_true, beq_iff_eq, List.all_eq_true] at h
  obtain ⟨hlen, hall⟩ := h
  have hxs' : xs.all okPt = true := hxs
  have hZs' : Zs.all okPt = true := hZs
  intro x hx z hz
  obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hx
  obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp hz
  have hic : i < combos.length := by omega
  have hm1 : (xs[i], combos[i]) ∈ xs.zip combos :=
    List.mem_iff_getElem.mpr ⟨i, by rw [List.length_zip]; omega, by simp⟩
  obtain ⟨hcl, hall2⟩ := hall _ hm1
  have hcl' : combos[i].length = Zs.length := hcl
  have hm2 : (Zs[j], combos[i][j]) ∈ Zs.zip combos[i] :=
    List.mem_iff_getElem.mpr ⟨j, by rw [List.length_zip]; omega, by simp⟩
  have hd := hall2 _ hm2
  have hxok : okPt xs[i] = true := List.all_eq_true.mp hxs' _ (List.getElem_mem ..)
  have hzok : okPt Zs[j] = true := List.all_eq_true.mp hZs' _ (List.getElem_mem ..)
  have hd' := dom_sound hY (okPt_mergeI hxok hzok) hd
  rw [val_mergeI hxok hzok] at hd'
  exact hd'

theorem okPts_of_subset {Y X : List IPt} (hY : okPts Y = true) (hX : ∀ x ∈ X, x ∈ Y) :
    okPts X = true := by
  simp only [okPts, List.all_eq_true] at hY ⊢
  exact fun x hx => hY x (hX x hx)

/-- The value vector of a point, as a list of real numbers. -/
def vlist (P : IPt) : List ℝ := P.1.map (fun (a : ℕ) => (a : ℝ) / (P.2 : ℝ))

theorem okPt_pos {P : IPt} (h : okPt P = true) : 0 < P.2 := by
  simp only [okPt, Bool.and_eq_true, decide_eq_true_eq] at h
  exact h.2

theorem ltLex_lex {D D' : ℕ} (hD : 0 < D) (hD' : 0 < D') :
    ∀ (as bs : List ℕ), ltLex D D' as bs = true →
      List.Lex (· < ·) (as.map (fun (a : ℕ) => (a : ℝ) / (D : ℝ)))
        (bs.map (fun (b : ℕ) => (b : ℝ) / (D' : ℝ)))
  | [], [], h => by simp [ltLex] at h
  | [], _ :: _, h => by simp [ltLex] at h
  | _ :: _, [], h => by simp [ltLex] at h
  | a :: as, b :: bs, h => by
    simp only [ltLex, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] at h
    have hDr : (0:ℝ) < D := by exact_mod_cast hD
    have hD'r : (0:ℝ) < D' := by exact_mod_cast hD'
    rw [List.map_cons, List.map_cons]
    rcases h with h1 | ⟨h1, h2⟩
    · apply List.Lex.rel
      have h1' : (a:ℝ) * D' < b * D := by exact_mod_cast h1
      rw [div_lt_div_iff₀ hDr hD'r]
      exact h1'
    · have h1' : (a:ℝ) * D' = b * D := by exact_mod_cast h1
      have e : (a:ℝ) / D = b / D' := by
        rw [div_eq_div_iff hDr.ne' hD'r.ne']
        exact h1'
      rw [e]
      exact List.Lex.cons (ltLex_lex hD hD' as bs h2)

theorem ltLex_vlist {P Q : IPt} (hP : 0 < P.2) (hQ : 0 < Q.2)
    (h : ltLex P.2 Q.2 P.1 Q.1 = true) : vlist P < vlist Q :=
  (List.lt_iff_lex_lt _ _).2 (ltLex_lex hP hQ _ _ h)

theorem chain_vlist : ∀ (Z : List IPt), (∀ P ∈ Z, 0 < P.2) → sortedZ Z = true →
    List.IsChain (fun P Q => vlist P < vlist Q) Z
  | [], _, _ => by simp
  | [_], _, _ => by simp
  | P :: Q :: rest, hpos, hs => by
    simp only [sortedZ, Bool.and_eq_true] at hs
    refine List.isChain_cons_cons.2 ⟨ltLex_vlist (hpos P (by simp)) (hpos Q (by simp)) hs.1, ?_⟩
    exact chain_vlist (Q :: rest) (fun R hR => hpos R (List.mem_cons_of_mem _ hR)) hs.2

theorem nodup_vlist {Z : List IPt} (hpos : ∀ P ∈ Z, 0 < P.2) (hs : sortedZ Z = true) :
    (Z.map vlist).Nodup := by
  have hc := chain_vlist Z hpos hs
  have hc' : List.IsChain (· < ·) (Z.map vlist) := (List.isChain_map vlist).2 hc
  have hpw := List.isChain_iff_pairwise.1 hc'
  exact List.Pairwise.imp (fun h => ne_of_lt h) hpw

theorem list8_of_length {l : List ℕ} (hl : l.length = 8) :
    ∃ a0 a1 a2 a3 a4 a5 a6 a7 : ℕ, l = [a0, a1, a2, a3, a4, a5, a6, a7] := by
  rcases l with _ | ⟨a0, _ | ⟨a1, _ | ⟨a2, _ | ⟨a3, _ | ⟨a4, _ | ⟨a5, _ | ⟨a6, _ | ⟨a7, _ | ⟨a8, l⟩⟩⟩⟩⟩⟩⟩⟩⟩
  all_goals first
    | exact ⟨_, _, _, _, _, _, _, _, rfl⟩
    | simp at hl

theorem vlist_eq_of_val {P Q : IPt} (hP : okPt P = true) (hQ : okPt Q = true)
    (h : val P = val Q) : vlist P = vlist Q := by
  have hP' := hP
  have hQ' := hQ
  simp only [okPt, Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq] at hP' hQ'
  apply List.ext_getElem
  · simp [vlist, hP'.1, hQ'.1]
  · intro i h1 h2
    have hi : i < P.1.length := by simpa [vlist] using h1
    have hi' : i < Q.1.length := by simpa [vlist] using h2
    have := congrFun h ⟨i, by omega⟩
    simp only [val] at this
    rw [List.getD_eq_getElem _ _ hi, List.getD_eq_getElem _ _ hi'] at this
    simp only [vlist, List.getElem_map]
    exact this

theorem checkZ_okPts {Z : List IPt} (h : checkZ Z = true) : okPts Z = true := by
  simp only [checkZ, Bool.and_eq_true] at h
  exact h.1.1.2

theorem checkZ_length {Z : List IPt} (h : checkZ Z = true) : Z.length = 1024 := by
  simp only [checkZ, Bool.and_eq_true, beq_iff_eq] at h
  exact h.1.1.1

theorem checkZ_nodup {Z : List IPt} (h : checkZ Z = true) : (Z.map val).Nodup := by
  have hok : okPts Z = true := checkZ_okPts h
  have hsort : sortedZ Z = true := by
    simp only [checkZ, Bool.and_eq_true] at h
    exact h.1.2
  have hokL : ∀ P ∈ Z, okPt P = true := by
    simp only [okPts, List.all_eq_true] at hok
    exact hok
  have hpos : ∀ P ∈ Z, 0 < P.2 := fun P hP => okPt_pos (hokL P hP)
  have hnV := nodup_vlist hpos hsort
  have hZ : Z.Nodup := List.Nodup.of_map vlist hnV
  refine List.Nodup.map_on ?_ hZ
  intro x hx y hy hxy
  exact List.inj_on_of_nodup_map hnV hx hy (vlist_eq_of_val (hokL x hx) (hokL y hy) hxy)

theorem checkZ_fin {Z : List IPt} (h : checkZ Z = true) :
    ∀ z ∈ finsetOf Z, (6060 / 10000 : ℝ) < Antinorm8.fin p₂ z := by
  have hok : okPts Z = true := checkZ_okPts h
  have hokL : ∀ P ∈ Z, okPt P = true := by
    simp only [okPts, List.all_eq_true] at hok
    exact hok
  have hall : ∀ P ∈ Z, 6060 * 2000 * P.2 < 10000 * finN P.1 := by
    simp only [checkZ, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at h
    exact h.2
  intro z hz
  obtain ⟨P, hP, rfl⟩ : ∃ P ∈ Z, val P = z := by
    simpa [finsetOf] using hz
  have hk := hall P hP
  have hDpos : 0 < P.2 := okPt_pos (hokL P hP)
  have hL : P.1.length = 8 := by
    have := hokL P hP
    simp only [okPt, Bool.and_eq_true, beq_iff_eq] at this
    exact this.1
  obtain ⟨L, D⟩ := P
  obtain ⟨N0, N1, N2, N3, N4, N5, N6, N7, rfl⟩ := list8_of_length hL
  simp only [finN] at hk
  have hDr : (0:ℝ) < D := by exact_mod_cast hDpos
  have hk' : (6060 * 2000 * (D:ℝ)) < 10000 * (2000 * (N0:ℝ) + 2000 * (N3:ℝ) + 1000 * (N4:ℝ)
      + 2000 * (N5:ℝ) + 2000 * (N6:ℝ) + 1860 * (N7:ℝ)) := by
    exact_mod_cast hk
  have e : Antinorm8.fin p₂ (val ([N0, N1, N2, N3, N4, N5, N6, N7], D))
      = (2000 * (N0:ℝ) + 2000 * (N3:ℝ) + 1000 * (N4:ℝ)
      + 2000 * (N5:ℝ) + 2000 * (N6:ℝ) + 1860 * (N7:ℝ)) / (2000 * (D:ℝ)) := by
    rw [p2v]
    simp [Antinorm8.fin, val]
    field_simp
    ring
  rw [e, lt_div_iff₀ (mul_pos (by norm_num) hDr)]
  linarith [hk']

theorem fam_mem_finsetOf {Y : List IPt} {x : Fin 8 → ℝ} :
    x ∈ finsetOf Y ↔ ∃ P ∈ Y, val P = x := by
  unfold finsetOf
  simp

theorem fam_finsetOf_nonneg (Y : List IPt) : ∀ x ∈ finsetOf Y, 0 ≤ x := by
  intro x hx
  obtain ⟨P, _, rfl⟩ := (fam_mem_finsetOf).1 hx
  exact val_nonneg P

theorem fam_leaf_mem {Z : List IPt} (hZ : okPts Z = true) {ν c₂ c₃ : ℕ}
    {comb : List (ℕ × ℕ × ℕ)} (h : dom Z.length (chunks32 Z) (initI ν c₂ c₃) comb = true) :
    init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ (finsetOf Z) := by
  have hη : (0:ℝ) < ê ^ (1 + ν) := pow_pos (by norm_num [ê]) _
  rw [MaxLeafFormal.Antinorm8.mem_smul_PZ_iff hη, ← val_initI ν c₂ c₃]
  exact dom_sound hZ (okPt_initI ν c₂ c₃) h

theorem fam_inf_mem {Z : List IPt} (hZ : okPts Z = true) {comb : List (ℕ × ℕ × ℕ)}
    (h : dom Z.length (chunks32 Z) initInfI comb = true) :
    initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ (finsetOf Z) := by
  have hη : (0:ℝ) < ê ^ (ν₀ + 2) := pow_pos (by norm_num [ê]) _
  rw [MaxLeafFormal.Antinorm8.mem_smul_PZ_iff hη, ← val_initInfI]
  exact dom_sound hZ okPt_initInfI h

theorem checkC2_sound {Z : List IPt} (hZ : okPts Z = true) {combos : List (List (ℕ × ℕ × ℕ))}
    (h : checkC2 Z.length (chunks32 Z) combos = true) :
    (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ (finsetOf Z)) ∧
      initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ (finsetOf Z) := by
  unfold checkC2 at h
  simp only [Bool.and_eq_true, beq_iff_eq, List.all_eq_true] at h
  obtain ⟨⟨hlen, hz⟩, hinf⟩ := h
  have h24 : ν₀ = 24 := rfl
  refine ⟨fun ν hν => ?_, fam_inf_mem hZ hinf⟩
  have hlt : ν < combos.length := by omega
  have hmem : ((ν, combos[ν]'hlt) : ℕ × List (ℕ × ℕ × ℕ)) ∈ (List.range 25).zip combos := by
    rw [List.mem_iff_getElem]
    refine ⟨ν, ?_, ?_⟩
    · simp only [List.length_zip, List.length_range, hlen]; omega
    · simp only [List.getElem_zip, List.getElem_range]
  have h1 := hz _ hmem
  dsimp only at h1
  exact fam_leaf_mem (ν := ν) (c₂ := 0) (c₃ := 0) (comb := combos[ν]'hlt) hZ h1

theorem checkLeaves_sound {Z : List IPt} (hZ : okPts Z = true)
    {entries : List ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ))}
    (h : checkLeaves Z.length (chunks32 Z) entries = true) :
    ∀ e ∈ entries, LeafFact Z (e.1, ()) := by
  intro e he
  unfold checkLeaves at h
  have h1 : dom Z.length (chunks32 Z) (initI e.1.1 e.1.2.1 e.1.2.2) e.2 = true :=
    List.all_eq_true.1 h e he
  exact fam_leaf_mem hZ h1

/-- The stage list `[initI] :: stages ++ [Z]` used in the chain. -/
def famL (ν c₂ c₃ : ℕ) (stages : List (List IPt)) (Z : List IPt) : List (List IPt) :=
  ([initI ν c₂ c₃] :: stages) ++ [Z]

/-- A chain with stages `Y₁, …, Y_{j-1}` (and `Y_j = Z`) gives (C5) with chains of length `j`. -/
theorem chainFact_of_stages {Z : List IPt} (hZ : okPts Z = true) (ν c₂ c₃ : ℕ)
    (stages : List (List IPt)) (hst : ∀ Y ∈ stages, okPts Y = true)
    (hfacts : ∀ i < stages.length + 1,
      StageFact Z (([initI ν c₂ c₃] :: stages).getD i []) ((stages ++ [Z]).getD i [])) :
    ChainFact Z ((ν, c₂, c₃), stages.length + 1) := by
  have hY0 : finsetOf ((famL ν c₂ c₃ stages Z).getD 0 []) = {val (initI ν c₂ c₃)} := by
    simp [famL, finsetOf]
  have hYj : finsetOf ((famL ν c₂ c₃ stages Z).getD (stages.length + 1) []) = finsetOf Z := by
    simp [famL]
  have hYnn : ∀ i < stages.length + 1,
      ∀ x ∈ finsetOf ((famL ν c₂ c₃ stages Z).getD i []), 0 ≤ x :=
    fun i _ x hx => fam_finsetOf_nonneg _ x hx
  have hpre : ∀ k < stages.length + 1,
      (famL ν c₂ c₃ stages Z).getD k [] = ([initI ν c₂ c₃] :: stages).getD k [] := by
    intro k hk
    have hk' : k < ([initI ν c₂ c₃] :: stages).length := by simpa using hk
    rw [famL, List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD,
      List.getElem?_append_left hk']
  have hshift : ∀ i, 1 ≤ i →
      (famL ν c₂ c₃ stages Z).getD i [] = (stages ++ [Z]).getD (i - 1) [] := by
    intro i hi
    obtain ⟨k, rfl⟩ : ∃ k, i = k + 1 := ⟨i - 1, by omega⟩
    simp [famL]
  have hY : ∀ i, 1 ≤ i → i ≤ stages.length + 1 →
      ∀ x ∈ finsetOf ((famL ν c₂ c₃ stages Z).getD (i - 1) []), ∀ z ∈ finsetOf Z,
        merge p₂ p₃ x z ∈ convexHull ℝ ((finsetOf ((famL ν c₂ c₃ stages Z).getD i []) :
          Finset (Fin 8 → ℝ)) : Set (Fin 8 → ℝ)) + Kpos := by
    intro i hi1 hi2 x hx z hz
    obtain ⟨x', hx', rfl⟩ := (fam_mem_finsetOf).1 hx
    obtain ⟨z', hz', rfl⟩ := (fam_mem_finsetOf).1 hz
    have hx'' : x' ∈ ([initI ν c₂ c₃] :: stages).getD (i - 1) [] := by
      rw [← hpre (i - 1) (by omega)]
      exact hx'
    have hS := (hfacts (i - 1) (by omega)) x' hx'' z' hz'
    rw [hshift i hi1]
    exact hS
  have key := C5_of_stages (p₂ := p₂) (p₃ := p₃)
    ⟨by norm_num [p₂], by norm_num [p₂, p₃], by norm_num [p₃]⟩
    (fam_finsetOf_nonneg Z) (val (initI ν c₂ c₃)) (val_nonneg _) (stages.length + 1)
    (fun i => finsetOf ((famL ν c₂ c₃ stages Z).getD i []))
    hY0 hYj hYnn hY
  unfold ChainFact
  intro Qs hlen hQ
  have key' := key Qs hlen hQ
  rw [val_initI ν c₂ c₃] at key'
  exact key'

theorem checkChain1_sound {Z : List IPt} (hZ : okPts Z = true)
    {entries : List ((ℕ × ℕ × ℕ) × List (List (ℕ × ℕ × ℕ)))}
    (h : checkChain1 Z.length (chunks32 Z) Z entries = true) :
    ∀ e ∈ entries, ChainFact Z (e.1, 1) := by
  intro e he
  unfold checkChain1 at h
  have h1 : checkBlock Z.length (chunks32 Z) Z [initI e.1.1 e.1.2.1 e.1.2.2] [e.2] = true :=
    List.all_eq_true.1 h e he
  have hxs : okPts [initI e.1.1 e.1.2.1 e.1.2.2] = true := by
    simp [okPts, okPt_initI]
  have hfacts : ∀ i < ([] : List (List IPt)).length + 1,
      StageFact Z (([initI e.1.1 e.1.2.1 e.1.2.2] :: []).getD i [])
        ((([] : List (List IPt)) ++ [Z]).getD i []) := by
    intro i hi
    have hi0 : i = 0 := by simp at hi; omega
    subst hi0
    exact checkBlock_sound hZ hZ hxs h1
  exact chainFact_of_stages hZ e.1.1 e.1.2.1 e.1.2.2 [] (by simp) hfacts

/-- Blocks of `B` consecutive elements cover a list. -/
theorem cover_blocks {α : Type} (P : α → Prop) (X : List α) (B : ℕ) (hB : 0 < B)
    (h : ∀ r < (X.length + B - 1) / B, ∀ x ∈ (X.drop (B * r)).take B, P x) :
    ∀ x ∈ X, P x := by
  intro x hx
  obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hx
  have hdm := Nat.div_add_mod i B
  have hmod := Nat.mod_lt i hB
  have hr : i / B < (X.length + B - 1) / B := by
    have h1 : (i + B) / B = i / B + 1 := Nat.add_div_right i hB
    have h2 : (i + B) / B ≤ (X.length + B - 1) / B := by
      apply Nat.div_le_div_right
      omega
    omega
  apply h (i / B) hr
  apply List.mem_iff_getElem.mpr
  refine ⟨i - B * (i / B), ?_, ?_⟩
  · simp only [List.length_take, List.length_drop]
    omega
  · simp only [List.getElem_take, List.getElem_drop]
    congr 1
    omega

/-- `Init(ν) ∈ ê^{1+ν} 𝒫_Z` for every `ν`, from (C2) and `ê < 1`. -/
theorem init00_mem {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
      initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z) (ν : ℕ) :
    init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z := by
  obtain ⟨hp3, -, ⟨hê, hêq⟩, -, -⟩ := rsc_side
  have hê1 : ê ≤ 1 := by linarith [hp3.1, hp3.2.1, hp3.2.2]
  by_cases hν : ν ≤ ν₀
  · exact C2.1 ν hν
  · have hsplit : init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0
        = initInf p₂ y + ![0, 0, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0] := by
      funext i; fin_cases i <;> simp [init, initInf]
    have hK : 0 ≤ (![0, 0, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0] : Fin 8 → ℝ) := by
      have h4 : (0 : ℝ) ≤ (1/2 : ℝ) ^ ν := pow_nonneg (by norm_num) _
      intro i; fin_cases i <;> simpa using h4
    rw [hsplit]
    refine MaxLeafFormal.Antinorm8.smul_PZ_mono hZ0 (pow_pos hê _) ?_
      (MaxLeafFormal.Antinorm8.smul_PZ_add_Kpos (pow_pos hê _) C2.2 (MaxLeafFormal.Antinorm8.Kpos_of_nonneg hK))
    exact pow_le_pow_of_le_one hê.le hê1 (by omega)

/-- A fold that starts in `𝒫_Z` stays in `𝒫_Z` (Step 1 with `η = η' = 1`, using (C1)). -/
theorem foldl_mem_PZ {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z) :
    ∀ (Qs : List (Fin 8 → ℝ)) (X : Fin 8 → ℝ), X ∈ PZ Z → (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
      Qs.foldl (merge p₂ p₃) X ∈ PZ Z := by
  obtain ⟨hp3, -⟩ := rsc_side
  have hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 := ⟨hp3.1, hp3.2.1, by linarith [hp3.2.2]⟩
  intro Qs
  induction Qs with
  | nil => intro X hX _; exact hX
  | cons Q Qs ih =>
    intro X hX hQs
    rw [List.foldl_cons]
    have hX1 : X ∈ (1:ℝ) • PZ Z := by rw [one_smul]; exact hX
    have hQ1 : Q ∈ (1:ℝ) • PZ Z := by rw [one_smul]; exact (hQs Q (by simp)).1
    have hm := merge_mem_smul_PZ hp hZ0 C1 one_pos one_pos hX1 hQ1 (hQs Q (by simp)).2
    rw [mul_one, one_smul] at hm
    exact ih _ hm (fun Q' hQ' => hQs Q' (by simp [hQ']))

theorem foldl_merge_add_left (Qs : List (Fin 8 → ℝ)) (X X' : Fin 8 → ℝ) :
    Qs.foldl (merge p₂ p₃) (X + X') = Qs.foldl (merge p₂ p₃) X + Qs.foldl (merge p₂ p₃) X' := by
  induction Qs generalizing X X' with
  | nil => rfl
  | cons Q Qs ih =>
    simp only [List.foldl_cons]
    rw [merge_add_left]
    exact ih _ _

theorem foldl_merge_smul_left (Qs : List (Fin 8 → ℝ)) (a : ℝ) (X : Fin 8 → ℝ) :
    Qs.foldl (merge p₂ p₃) (a • X) = a • Qs.foldl (merge p₂ p₃) X := by
  induction Qs generalizing X with
  | nil => rfl
  | cons Q Qs ih =>
    simp only [List.foldl_cons]
    rw [merge_smul_left]
    exact ih _

/-! ### Helpers for `combWitness_sound` -/

theorem mem_lattice5 {ν c₂ c₃ : ℕ} (h1 : 1 ≤ ν) (h2 : ν ≤ 36) (h3 : 1 ≤ c₂ + c₃)
    (h4 : c₂ + c₃ ≤ ν) : (ν, c₂, c₃) ∈ lattice5 := by
  unfold lattice5
  rw [List.mem_flatMap]
  refine ⟨ν - 1, List.mem_range.mpr (by omega), ?_⟩
  rw [List.mem_flatMap]
  refine ⟨c₂, List.mem_range.mpr (by omega), ?_⟩
  rw [List.mem_map]
  refine ⟨c₃, ?_, ?_⟩
  · rw [List.mem_filter]
    exact ⟨List.mem_range.mpr (by omega), decide_eq_true h3⟩
  · show (ν - 1 + 1, c₂, c₃) = (ν, c₂, c₃)
    rw [Nat.sub_add_cancel h1]

theorem mem_lattice4 {ν c₂ c₃ : ℕ} (h1 : 4 ≤ ν) (h2 : ν ≤ 36) (h3 : 1 ≤ c₂ + c₃)
    (h4 : c₂ + c₃ ≤ ν - 1) : (ν, c₂, c₃) ∈ lattice4 := by
  unfold lattice4
  rw [List.mem_flatMap]
  refine ⟨ν - 4, List.mem_range.mpr (by omega), ?_⟩
  rw [List.mem_flatMap]
  refine ⟨c₂, List.mem_range.mpr (by omega), ?_⟩
  rw [List.mem_map]
  refine ⟨c₃, ?_, ?_⟩
  · rw [List.mem_filter]
    exact ⟨List.mem_range.mpr (by omega), decide_eq_true h3⟩
  · show (ν - 4 + 4, c₂, c₃) = (ν, c₂, c₃)
    rw [Nat.sub_add_cancel h1]

def scS (l : List ((ℕ × ℕ) × ℕ × ℕ)) : ℕ × ℕ :=
  l.foldr (fun e r => (r.1 * e.2.2 + e.2.1 * r.2, r.2 * e.2.2)) (0, 1)

def scG (g : ℕ × ℕ → ℕ × ℕ) (l : List ((ℕ × ℕ) × ℕ × ℕ)) : ℕ × ℕ :=
  l.foldr (fun e r => (r.1 * (e.2.2 * (g e.1).2) + e.2.1 * (g e.1).1 * r.2,
    r.2 * (e.2.2 * (g e.1).2))) (0, 1)

theorem scS_spec : ∀ l : List ((ℕ × ℕ) × ℕ × ℕ), (∀ e ∈ l, 0 < e.2.2) →
    0 < (scS l).2 ∧ ((scS l).1 : ℝ) / ((scS l).2 : ℝ)
      = (l.map fun e => ((e.2.1 : ℝ) / e.2.2)).sum := by
  intro l
  induction l with
  | nil => intro _; simp [scS]
  | cons e l ih =>
    intro hl
    obtain ⟨hS2, hval⟩ := ih (fun e' he' => hl e' (by simp [he']))
    have hb : 0 < e.2.2 := hl e (by simp)
    have hb' : (e.2.2 : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
    have hS2' : ((scS l).2 : ℝ) ≠ 0 := by exact_mod_cast hS2.ne'
    have hfold : scS (e :: l) = ((scS l).1 * e.2.2 + e.2.1 * (scS l).2, (scS l).2 * e.2.2) := rfl
    rw [hfold, List.map_cons, List.sum_cons, ← hval]
    refine ⟨Nat.mul_pos hS2 hb, ?_⟩
    dsimp only
    push_cast
    field_simp
    ring

theorem scG_spec (g : ℕ × ℕ → ℕ × ℕ) (hg : ∀ c, 0 < (g c).2) :
    ∀ l : List ((ℕ × ℕ) × ℕ × ℕ), (∀ e ∈ l, 0 < e.2.2) →
    0 < (scG g l).2 ∧ ((scG g l).1 : ℝ) / ((scG g l).2 : ℝ)
      = (l.map fun e => ((e.2.1 : ℝ) / e.2.2) * (((g e.1).1 : ℝ) / ((g e.1).2 : ℝ))).sum := by
  intro l
  induction l with
  | nil => intro _; simp [scG]
  | cons e l ih =>
    intro hl
    obtain ⟨hS2, hval⟩ := ih (fun e' he' => hl e' (by simp [he']))
    have hb : 0 < e.2.2 := hl e (by simp)
    have hG : 0 < (g e.1).2 := hg _
    have hb' : (e.2.2 : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
    have hG' : ((g e.1).2 : ℝ) ≠ 0 := by exact_mod_cast hG.ne'
    have hS2' : ((scG g l).2 : ℝ) ≠ 0 := by exact_mod_cast hS2.ne'
    have hfold : scG g (e :: l) = ((scG g l).1 * (e.2.2 * (g e.1).2) + e.2.1 * (g e.1).1 * (scG g l).2,
        (scG g l).2 * (e.2.2 * (g e.1).2)) := rfl
    rw [hfold, List.map_cons, List.sum_cons, ← hval]
    refine ⟨Nat.mul_pos hS2 (Nat.mul_pos hb hG), ?_⟩
    dsimp only
    push_cast
    field_simp
    ring

theorem sc_uF_ratio (c₁ c₂ : ℕ) :
    (1 - p₂) ^ c₁ * (1 - p₃) ^ c₂ = ((uF c₁ c₂).1 : ℝ) / ((uF c₁ c₂).2 : ℝ) := by
  simp only [uF, p2v, p3v]
  push_cast
  rw [show (1:ℝ) - 7/100 = 93/100 by norm_num, show (1:ℝ) - 77/1000 = 923/1000 by norm_num,
    div_pow, div_pow, div_mul_div_comm]

theorem sc_wF_ratio (c₁ c₂ : ℕ) :
    ϖ₂ ^ c₁ * ϖ₃ ^ c₂ = ((wF c₁ c₂).1 : ℝ) / ((wF c₁ c₂).2 : ℝ) := by
  simp only [wF, ϖ₂, ϖ₃]
  push_cast
  rw [pow_add, div_pow, div_pow, div_mul_div_comm]

def vecN (ν : ℕ) (x z : ℝ) : Fin 8 → ℝ :=
  ![x * (y / 2), x * (p₂ / 2), 0, 0, (1/2 : ℝ) ^ ν * z, 0, 0, 0]

theorem init_eq_vecN (ν c₂ c₃ : ℕ) :
    init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ = vecN ν ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃) (ϖ₂ ^ c₂ * ϖ₃ ^ c₃) := by
  funext i; fin_cases i <;> simp [init, vecN] <;> ring

theorem vecN_smul (ν : ℕ) (c x z : ℝ) : c • vecN ν x z = vecN ν (c * x) (c * z) := by
  funext i; fin_cases i <;> simp [vecN] <;> ring

theorem vecN_add (ν : ℕ) (x z x' z' : ℝ) :
    vecN ν x z + vecN ν x' z' = vecN ν (x + x') (z + z') := by
  funext i; fin_cases i <;> simp [vecN] <;> ring

theorem vecN_zero (ν : ℕ) : vecN ν 0 0 = 0 := by
  funext i; fin_cases i <;> simp [vecN]

theorem sc_listSum (ν : ℕ) : ∀ l : List ((ℕ × ℕ) × ℕ × ℕ),
    (l.map fun e => ((e.2.1 : ℝ) / e.2.2) • init p₂ p₃ y ϖ₂ ϖ₃ ν e.1.1 e.1.2).sum
      = vecN ν (l.map fun e => ((e.2.1 : ℝ) / e.2.2) * ((1 - p₂) ^ e.1.1 * (1 - p₃) ^ e.1.2)).sum
        (l.map fun e => ((e.2.1 : ℝ) / e.2.2) * (ϖ₂ ^ e.1.1 * ϖ₃ ^ e.1.2)).sum := by
  intro l
  induction l with
  | nil => simp only [List.map_nil, List.sum_nil, vecN_zero]
  | cons e l ih =>
    simp only [List.map_cons, List.sum_cons]
    rw [ih, init_eq_vecN, vecN_smul, vecN_add]

/-- `eq:rsc-init-linear`: a convex-combination witness writes `Init~(ν; c₂, c₃)` as the
combination of the `Init~(ν; c₂', c₃')`. -/
theorem combWitness_sound {c₂ c₃ : ℕ} {comps : List ((ℕ × ℕ) × ℕ × ℕ)}
    (h : combWitness c₂ c₃ comps = true) (ν : ℕ) :
    (∀ e ∈ comps, 0 ≤ ((e.2.1 : ℝ) / e.2.2)) ∧ (comps.map fun e => ((e.2.1 : ℝ) / e.2.2)).sum = 1 ∧
      init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ =
        (comps.map fun e => ((e.2.1 : ℝ) / e.2.2) • init p₂ p₃ y ϖ₂ ϖ₃ ν e.1.1 e.1.2).sum := by
  unfold combWitness at h
  simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true] at h
  obtain ⟨⟨⟨h1, h2⟩, h3⟩, h4⟩ := h
  have hpos : ∀ e ∈ comps, 0 < e.2.2 := h1
  have h2' : (scS comps).1 = (scS comps).2 := h2
  have h3' : (scG (fun c => uF c.1 c.2) comps).1 * (uF c₂ c₃).2
      = (uF c₂ c₃).1 * (scG (fun c => uF c.1 c.2) comps).2 := h3
  have h4' : (scG (fun c => wF c.1 c.2) comps).1 * (wF c₂ c₃).2
      = (wF c₂ c₃).1 * (scG (fun c => wF c.1 c.2) comps).2 := h4
  obtain ⟨hSpos, hSval⟩ := scS_spec comps hpos
  obtain ⟨hUpos, hUval⟩ := scG_spec (fun c => uF c.1 c.2)
    (fun c => by show 0 < (uF c.1 c.2).2; simp only [uF]; positivity) comps hpos
  obtain ⟨hWpos, hWval⟩ := scG_spec (fun c => wF c.1 c.2)
    (fun c => by show 0 < (wF c.1 c.2).2; simp only [wF]; positivity) comps hpos
  have hSne : ((scS comps).2 : ℝ) ≠ 0 := by exact_mod_cast hSpos.ne'
  have hUne : ((scG (fun c => uF c.1 c.2) comps).2 : ℝ) ≠ 0 := by exact_mod_cast hUpos.ne'
  have hWne : ((scG (fun c => wF c.1 c.2) comps).2 : ℝ) ≠ 0 := by exact_mod_cast hWpos.ne'
  have hu0 : ((uF c₂ c₃).2 : ℝ) ≠ 0 := by
    have : 0 < (uF c₂ c₃).2 := by simp only [uF]; positivity
    exact_mod_cast this.ne'
  have hw0 : ((wF c₂ c₃).2 : ℝ) ≠ 0 := by
    have : 0 < (wF c₂ c₃).2 := by simp only [wF]; positivity
    exact_mod_cast this.ne'
  have hsum1 : (comps.map fun e => ((e.2.1 : ℝ) / e.2.2)).sum = 1 := by
    have hc : ((scS comps).1 : ℝ) = ((scS comps).2 : ℝ) := by rw [h2']
    rw [hc, div_self hSne] at hSval
    exact hSval.symm
  have hsumU : (comps.map fun e => ((e.2.1 : ℝ) / e.2.2) * ((1 - p₂) ^ e.1.1 * (1 - p₃) ^ e.1.2)).sum
      = (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ := by
    simp only [sc_uF_ratio]
    rw [← hUval, div_eq_div_iff hUne hu0]
    exact_mod_cast h3'
  have hsumW : (comps.map fun e => ((e.2.1 : ℝ) / e.2.2) * (ϖ₂ ^ e.1.1 * ϖ₃ ^ e.1.2)).sum
      = ϖ₂ ^ c₂ * ϖ₃ ^ c₃ := by
    simp only [sc_wF_ratio]
    rw [← hWval, div_eq_div_iff hWne hw0]
    exact_mod_cast h4'
  refine ⟨fun e _ => div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _), hsum1, ?_⟩
  rw [init_eq_vecN, sc_listSum ν comps, hsumU, hsumW]

theorem rsc5_list_sum_eq {α β : Type*} [AddCommMonoid β] (L : List α) (g : α → β) :
    (L.map g).sum = ∑ i : Fin L.length, g (L[i]) := by
  induction L with
  | nil => simp
  | cons a L ih =>
    rw [List.map_cons, List.sum_cons, ih]
    show _ = ∑ i : Fin (L.length + 1), g (a :: L)[i]
    rw [Fin.sum_univ_succ]
    simp

theorem rsc5_convex_sum {V : Type*} [AddCommGroup V] [Module ℝ V] {S : Set V} (hS : Convex ℝ S)
    {α : Type*} (L : List α) (w : α → ℝ) (z : α → V) (hw : ∀ a ∈ L, 0 ≤ w a)
    (hsum : (L.map w).sum = 1) (hz : ∀ a ∈ L, z a ∈ S) :
    (L.map fun a => w a • z a).sum ∈ S := by
  rw [rsc5_list_sum_eq L (fun a => w a • z a)]
  rw [rsc5_list_sum_eq L w] at hsum
  have key := hS.sum_mem (t := (Finset.univ : Finset (Fin L.length)))
    (w := fun i => w L[i]) (z := fun i => z L[i])
    (fun i _ => hw _ (List.getElem_mem _)) hsum (fun i _ => hz _ (List.getElem_mem _))
  exact key

theorem rsc5_foldl_sum {α : Type*} (Qs : List (Fin 8 → ℝ)) (L : List α) (w : α → ℝ)
    (z : α → Fin 8 → ℝ) :
    Qs.foldl (merge p₂ p₃) (L.map fun a => w a • z a).sum =
      (L.map fun a => w a • Qs.foldl (merge p₂ p₃) (z a)).sum := by
  have h0 : Qs.foldl (merge p₂ p₃) 0 = 0 := by
    simpa using foldl_merge_smul_left Qs 0 0
  induction L with
  | nil => simpa using h0
  | cons a L ih =>
    simp only [List.map_cons, List.sum_cons]
    rw [foldl_merge_add_left, ih, foldl_merge_smul_left]

theorem rsc5_foldl_conv {S : Set (Fin 8 → ℝ)} (hS : Convex ℝ S) (Qs : List (Fin 8 → ℝ))
    {α : Type*} (L : List α) (w : α → ℝ) (z : α → Fin 8 → ℝ) (hw : ∀ a ∈ L, 0 ≤ w a)
    (hsum : (L.map w).sum = 1) (hx : ∀ a ∈ L, Qs.foldl (merge p₂ p₃) (z a) ∈ S) :
    Qs.foldl (merge p₂ p₃) (L.map fun a => w a • z a).sum ∈ S := by
  rw [rsc5_foldl_sum]
  exact rsc5_convex_sum hS L w (fun a => Qs.foldl (merge p₂ p₃) (z a)) hw hsum hx

theorem rsc5_smul_sum {α : Type*} (c : ℝ) (L : List α) (w : α → ℝ) (z : α → Fin 8 → ℝ) :
    c • (L.map fun a => w a • z a).sum = (L.map fun a => w a • (c • z a)).sum := by
  induction L with
  | nil => simp
  | cons a L ih =>
    simp only [List.map_cons, List.sum_cons, smul_add, ih, smul_comm c (w a) (z a)]

theorem rsc5_finset_nonneg (Z : List IPt) : ∀ z ∈ finsetOf Z, 0 ≤ z := by
  intro z hz
  unfold finsetOf at hz
  obtain ⟨P, -, rfl⟩ := List.mem_map.1 (List.mem_toFinset.1 hz)
  exact val_nonneg P

theorem rsc5_chain {Z : List IPt}
    (C1 : ∀ z ∈ finsetOf Z, ∀ z' ∈ finsetOf Z, merge p₂ p₃ z z' ∈ PZ (finsetOf Z))
    {e : (ℕ × ℕ × ℕ) × ℕ} (hc : ChainFact Z e) {Qs : List (Fin 8 → ℝ)} (hlen : e.2 ≤ Qs.length)
    (hQ : ∀ Q ∈ Qs, Q ∈ PZ (finsetOf Z) ∧ 0 ≤ Q) :
    Qs.foldl (merge p₂ p₃) ((ê ^ (1 + e.1.1))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ e.1.1 e.1.2.1 e.1.2.2)
      ∈ PZ (finsetOf Z) := by
  have hsplit := List.take_append_drop e.2 Qs
  have hlt : (Qs.take e.2).length = e.2 := by simp [hlen]
  rw [← hsplit, List.foldl_append]
  exact foldl_mem_PZ (rsc5_finset_nonneg Z) C1 _ _
    (hc _ hlt (fun Q hQm => hQ Q (List.mem_of_mem_take hQm)))
    (fun Q hQm => hQ Q (List.mem_of_mem_drop hQm))

theorem rsc5_shape5 (T : List ((ℕ × ℕ × ℕ) × ℕ)) (pt : ℕ × ℕ × ℕ) (dat : List ℕ)
    (h : latOK5 T pt dat = true) :
    (∃ k, dat = [0, k]) ∨ (∃ m rest, dat = 1 :: m :: rest) := by
  rcases dat with _ | ⟨a, _ | ⟨b, _ | ⟨c, rest⟩⟩⟩
  · simp [latOK5] at h
  · simp [latOK5] at h
  · rcases a with _ | _ | a
    · exact Or.inl ⟨b, rfl⟩
    · exact Or.inr ⟨b, [], rfl⟩
    · simp [latOK5] at h
  · rcases a with _ | _ | a
    · simp [latOK5] at h
    · exact Or.inr ⟨b, c :: rest, rfl⟩
    · simp [latOK5] at h

theorem rsc4_shape4 (T : List ((ℕ × ℕ × ℕ) × Unit)) (pt : ℕ × ℕ × ℕ) (dat : List ℕ)
    (h : latOK4 T pt dat = true) :
    (∃ k, dat = [0, k]) ∨ (∃ m rest, dat = 1 :: m :: rest) := by
  rcases dat with _ | ⟨a, _ | ⟨b, _ | ⟨c, rest⟩⟩⟩
  · simp [latOK4] at h
  · simp [latOK4] at h
  · rcases a with _ | _ | a
    · exact Or.inl ⟨b, rfl⟩
    · exact Or.inr ⟨b, [], rfl⟩
    · simp [latOK4] at h
  · rcases a with _ | _ | a
    · simp [latOK4] at h
    · exact Or.inr ⟨b, c :: rest, rfl⟩
    · simp [latOK4] at h

theorem rsc5_point {Z : List IPt}
    (C1 : ∀ z ∈ finsetOf Z, ∀ z' ∈ finsetOf Z, merge p₂ p₃ z z' ∈ PZ (finsetOf Z))
    (h00 : ∀ ν, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ (finsetOf Z))
    {T : List ((ℕ × ℕ × ℕ) × ℕ)} (hT : ∀ e ∈ T, ChainFact Z e) (ν c₂ c₃ : ℕ)
    (dat : List ℕ) (hok : latOK5 T (ν, c₂, c₃) dat = true)
    (Qs : List (Fin 8 → ℝ)) (hlen : Qs.length = jTarget ν c₂)
    (hQ : ∀ Q ∈ Qs, Q ∈ PZ (finsetOf Z) ∧ 0 ≤ Q) :
    Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ (finsetOf Z) := by
  have hê : 0 < ê := by norm_num [ê]
  have hη : 0 < ê ^ (1 + ν) := pow_pos hê _
  have hS : Convex ℝ (PZ (finsetOf Z)) := MaxLeafFormal.Antinorm8.convex_hullKpos (finsetOf Z)
  have hchain : ∀ t : (ℕ × ℕ × ℕ) × ℕ, ChainFact Z t → t.1.1 = ν → t.2 ≤ jTarget ν c₂ →
      Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν t.1.2.1 t.1.2.2)
        ∈ PZ (finsetOf Z) := by
    intro t hc hn hj
    have ht : ((ν, t.1.2.1, t.1.2.2), t.2) = t := Prod.ext (Prod.ext hn.symm rfl) rfl
    have hc' : ChainFact Z ((ν, t.1.2.1, t.1.2.2), t.2) := by rw [ht]; exact hc
    exact rsc5_chain C1 hc' (by rw [hlen]; exact hj) hQ
  rcases rsc5_shape5 T _ dat hok with ⟨k, rfl⟩ | ⟨m, rest, rfl⟩
  · simp only [latOK5, Bool.and_eq_true, decide_eq_true_eq] at hok
    obtain ⟨⟨hk, hpt⟩, hj⟩ := hok
    have hmem : T.getD k ((0, 0, 0), 0) ∈ T := by
      rw [List.getD_eq_getElem _ _ hk]; exact List.getElem_mem _
    have key := hchain _ (hT _ hmem) (by rw [hpt]) hj
    rw [hpt] at key
    exact key
  · simp only [latOK5, Bool.and_eq_true, List.all_eq_true, Bool.or_eq_true,
      decide_eq_true_eq] at hok
    obtain ⟨hcomp, hB⟩ := hok
    obtain ⟨hnn, hsum, heq⟩ := combWitness_sound hB ν
    rw [heq, rsc5_smul_sum]
    refine rsc5_foldl_conv hS Qs _ (fun a : (ℕ × ℕ) × ℕ × ℕ => ((a.2.1 : ℝ) / a.2.2))
      (fun a : (ℕ × ℕ) × ℕ × ℕ => (ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν a.1.1 a.1.2)
      hnn hsum ?_
    intro a ha
    obtain ⟨e0, he0, rfl⟩ := List.mem_map.1 ha
    rcases hcomp e0 he0 with h0 | ⟨⟨⟨h1, hlt⟩, hn⟩, hle⟩
    · have hc0 : compPt T 0 e0 = (0, 0) := by simp [compPt, h0]
      show Qs.foldl (merge p₂ p₃)
        ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν (compPt T 0 e0).1 (compPt T 0 e0).2)
          ∈ PZ (finsetOf Z)
      rw [hc0]
      exact foldl_mem_PZ (rsc5_finset_nonneg Z) C1 _ _
        ((MaxLeafFormal.Antinorm8.mem_smul_PZ_iff hη).1 (h00 ν)) hQ
    · have hc0 : compPt T 0 e0 = ((T.getD e0.2.1 ((0, 0, 0), 0)).1.2.1,
          (T.getD e0.2.1 ((0, 0, 0), 0)).1.2.2) := by simp [compPt, h1]
      have hmem : T.getD e0.2.1 ((0, 0, 0), 0) ∈ T := by
        rw [List.getD_eq_getElem _ _ hlt]; exact List.getElem_mem _
      show Qs.foldl (merge p₂ p₃)
        ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν (compPt T 0 e0).1 (compPt T 0 e0).2)
          ∈ PZ (finsetOf Z)
      rw [hc0]
      exact hchain (T.getD e0.2.1 ((0, 0, 0), 0)) (hT _ hmem) hn hle

theorem rsc4_dat {T : List ((ℕ × ℕ × ℕ) × Unit)} {wit : List (List ℕ)}
    (h : checkLattice4 T wit = true) {ν c₂ c₃ : ℕ} (hm : (ν, c₂, c₃) ∈ lattice4) :
    ∃ dat, latOK4 T (ν, c₂, c₃) dat = true := by
  rw [checkLattice4, Bool.and_eq_true, beq_iff_eq, List.all_eq_true] at h
  obtain ⟨hlen, hall⟩ := h
  obtain ⟨i, hi, hiEq⟩ := List.getElem_of_mem hm
  have hi' : i < wit.length := by rw [← hlen]; exact hi
  have hi2 : i < (lattice4.zip wit).length := by
    rw [List.length_zip, hlen, min_self]; exact hi'
  have hz := hall _ (List.getElem_mem hi2)
  simp only [List.getElem_zip] at hz
  rw [hiEq] at hz
  exact ⟨_, hz⟩

theorem rsc4_point {Z : List IPt}
    (h00 : ∀ ν, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ (finsetOf Z))
    {T : List ((ℕ × ℕ × ℕ) × Unit)} (hT : ∀ e ∈ T, LeafFact Z e) (ν c₂ c₃ : ℕ)
    (dat : List ℕ) (hok : latOK4 T (ν, c₂, c₃) dat = true) :
    init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ (finsetOf Z) := by
  have hS : Convex ℝ (ê ^ (1 + ν) • PZ (finsetOf Z)) :=
    (MaxLeafFormal.Antinorm8.convex_hullKpos (finsetOf Z)).smul _
  have hleaf : ∀ t : (ℕ × ℕ × ℕ) × Unit, t ∈ T → t.1.1 = ν →
      init p₂ p₃ y ϖ₂ ϖ₃ ν t.1.2.1 t.1.2.2 ∈ ê ^ (1 + ν) • PZ (finsetOf Z) := by
    intro t ht hn
    have ht' : ((ν, t.1.2.1, t.1.2.2), t.2) = t := Prod.ext (Prod.ext hn.symm rfl) rfl
    have hc : LeafFact Z ((ν, t.1.2.1, t.1.2.2), t.2) := by rw [ht']; exact hT t ht
    exact hc
  rcases rsc4_shape4 T _ dat hok with ⟨k, rfl⟩ | ⟨m, rest, rfl⟩
  · simp only [latOK4, Bool.and_eq_true, decide_eq_true_eq] at hok
    obtain ⟨hk, hpt⟩ := hok
    have hmem : T.getD k ((0, 0, 0), ()) ∈ T := by
      rw [List.getD_eq_getElem _ _ hk]; exact List.getElem_mem _
    have key := hleaf _ hmem (by rw [hpt])
    rw [hpt] at key
    exact key
  · simp only [latOK4, Bool.and_eq_true, List.all_eq_true, Bool.or_eq_true,
      decide_eq_true_eq] at hok
    obtain ⟨hcomp, hB⟩ := hok
    obtain ⟨hnn, hsum, heq⟩ := combWitness_sound hB ν
    rw [heq]
    refine rsc5_convex_sum hS _ (fun a : (ℕ × ℕ) × ℕ × ℕ => ((a.2.1 : ℝ) / a.2.2))
      (fun a : (ℕ × ℕ) × ℕ × ℕ => init p₂ p₃ y ϖ₂ ϖ₃ ν a.1.1 a.1.2) hnn hsum ?_
    intro a ha
    obtain ⟨e0, he0, rfl⟩ := List.mem_map.1 ha
    rcases hcomp e0 he0 with h0 | ⟨⟨h1, hlt⟩, hn⟩
    · have hc0 : compPt T () e0 = (0, 0) := by simp [compPt, h0]
      show init p₂ p₃ y ϖ₂ ϖ₃ ν (compPt T () e0).1 (compPt T () e0).2
        ∈ ê ^ (1 + ν) • PZ (finsetOf Z)
      rw [hc0]
      exact h00 ν
    · have hc0 : compPt T () e0 = ((T.getD e0.2.1 ((0, 0, 0), ())).1.2.1,
          (T.getD e0.2.1 ((0, 0, 0), ())).1.2.2) := by simp [compPt, h1]
      have hmem : T.getD e0.2.1 ((0, 0, 0), ()) ∈ T := by
        rw [List.getD_eq_getElem _ _ hlt]; exact List.getElem_mem _
      show init p₂ p₃ y ϖ₂ ϖ₃ ν (compPt T () e0).1 (compPt T () e0).2
        ∈ ê ^ (1 + ν) • PZ (finsetOf Z)
      rw [hc0]
      exact hleaf (T.getD e0.2.1 ((0, 0, 0), ())) hmem hn

/-- (C5) at every lattice point, from the lattice check. -/
theorem checkLattice5_sound {Z : List IPt} (hZ : okPts Z = true)
    (C1 : ∀ z ∈ finsetOf Z, ∀ z' ∈ finsetOf Z, merge p₂ p₃ z z' ∈ PZ (finsetOf Z))
    (h00 : ∀ ν, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ (finsetOf Z))
    {T : List ((ℕ × ℕ × ℕ) × ℕ)} (hT : ∀ e ∈ T, ChainFact Z e)
    {wit : List (List ℕ)} (h : checkLattice5 T wit = true) :
    ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
      ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
      (∀ Q ∈ Qs, Q ∈ PZ (finsetOf Z) ∧ 0 ≤ Q) →
      Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ (finsetOf Z) := by
  intro ν hν1 hνE c₂ c₃ hc1 hc2 Qs hlen hQ
  have hν36 : ν ≤ 36 := by simpa [νE] using hνE
  have hmem : (ν, c₂, c₃) ∈ lattice5 := mem_lattice5 hν1 hν36 hc1 hc2
  rw [checkLattice5, Bool.and_eq_true, beq_iff_eq, List.all_eq_true] at h
  obtain ⟨hlen5, hall⟩ := h
  obtain ⟨i, hi, hiEq⟩ := List.getElem_of_mem hmem
  have hi' : i < wit.length := by rw [← hlen5]; exact hi
  have hi2 : i < (lattice5.zip wit).length := by
    rw [List.length_zip, hlen5, min_self]; exact hi'
  have hz := hall _ (List.getElem_mem hi2)
  simp only [List.getElem_zip] at hz
  rw [hiEq] at hz
  exact rsc5_point C1 h00 hT ν c₂ c₃ _ hz Qs hlen hQ

/-- (C4) at every lattice point, from the lattice check. -/
theorem checkLattice4_sound {Z : List IPt} (hZ : okPts Z = true)
    (h00 : ∀ ν, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ (finsetOf Z))
    {T : List ((ℕ × ℕ × ℕ) × Unit)} (hT : ∀ e ∈ T, LeafFact Z e)
    {wit : List (List ℕ)} (h : checkLattice4 T wit = true) :
    ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
      (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ (finsetOf Z)) ∧
      (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
        init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ (finsetOf Z)) := by
  intro ν h2 hνE hd
  have hν36 : ν ≤ 36 := by simpa [νE] using hνE
  have h4 : 4 ≤ ν := by
    unfold d₃ at hd
    split_ifs at hd <;> omega
  have hlat : ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν - 1 →
      init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ (finsetOf Z) := by
    intro c₂ c₃ hc1 hc2
    obtain ⟨dat, hok⟩ := rsc4_dat h (mem_lattice4 h4 hν36 hc1 hc2)
    exact rsc4_point h00 hT ν c₂ c₃ dat hok
  exact ⟨fun c₃ h1 h2' => hlat 0 c₃ (by omega) (by omega),
    fun _ c₂ c₃ h1 h2' => hlat c₂ c₃ (by omega) h2'⟩


/-! ### Aggregation helpers (used by the generated `RSCData.All`) -/

theorem forall_mem_append' {α : Type} {P : α → Prop} {l₁ l₂ : List α}
    (h₁ : ∀ e ∈ l₁, P e) (h₂ : ∀ e ∈ l₂, P e) : ∀ e ∈ l₁ ++ l₂, P e := by
  intro e he
  rcases List.mem_append.1 he with h | h
  · exact h₁ e h
  · exact h₂ e h

theorem forall_lt_of_forall_range {P : ℕ → Prop} {n : ℕ} (h : List.Forall P (List.range n)) :
    ∀ r < n, P r := by
  intro r hr
  exact List.forall_iff_forall_mem.1 h r (List.mem_range.2 hr)

theorem agg_getD_okPts : ∀ (l : List (List IPt)) (i : ℕ), l.all okPts = true → okPts (l.getD i []) = true
  | [], i, _ => by simp [okPts]
  | a :: l, 0, h => by
      simp only [List.all_cons, Bool.and_eq_true] at h
      simpa using h.1
  | a :: l, i + 1, h => by
      simp only [List.all_cons, Bool.and_eq_true] at h
      simpa using agg_getD_okPts l i h.2

theorem agg_stage_aux {Z X Yt : List IPt} (hZ : checkZ Z = true) (hX : okPts X = true)
    (hYt : okPts Yt = true) (N : ℕ) (hN : (X.length + 7) / 8 ≤ N)
    (h : ∀ r < N, ∃ c, checkBlock Yt.length (chunks32 Yt) Z ((X.drop (8 * r)).take 8) c = true) :
    StageFact Z X Yt := by
  unfold StageFact
  refine cover_blocks (fun x => ∀ z ∈ Z, merge p₂ p₃ (val x) (val z) ∈
    convexHull ℝ (finsetOf Yt : Set (Fin 8 → ℝ)) + Kpos) X 8 (by norm_num) ?_
  intro r hr x hx
  obtain ⟨c, hcb⟩ := h r (by omega)
  have hsub : ∀ y ∈ (X.drop (8 * r)).take 8, y ∈ X :=
    fun y hy => List.mem_of_mem_drop (List.mem_of_mem_take hy)
  have := checkBlock_sound hYt (checkZ_okPts hZ) (okPts_of_subset hX hsub) hcb
  unfold StageFact at this
  exact this x hx

theorem c1_of_blocks {Z : List IPt} (hZ : checkZ Z = true)
    (h : List.Forall (fun r => ∃ c, checkBlock Z.length (chunks32 Z) Z ((Z.drop (8 * r)).take 8) c = true)
      (List.range 128)) :
    ∀ z ∈ finsetOf Z, ∀ z' ∈ finsetOf Z, merge p₂ p₃ z z' ∈ PZ (finsetOf Z) := by
  have hS : StageFact Z Z Z := agg_stage_aux hZ (checkZ_okPts hZ) (checkZ_okPts hZ) 128
    (by have := checkZ_length hZ; omega) (forall_lt_of_forall_range h)
  unfold StageFact at hS
  intro z hz z' hz'
  obtain ⟨x, hx, rfl⟩ := fam_mem_finsetOf.1 hz
  obtain ⟨x', hx', rfl⟩ := fam_mem_finsetOf.1 hz'
  exact hS x hx x' hx'

theorem stage_of_blocks {Z X Yt : List IPt} (hZ : checkZ Z = true) (hX : okPts X = true)
    (hYt : okPts Yt = true) (nb : ℕ) (hnb : decide ((X.length + 7) / 8 ≤ nb) = true)
    (h : List.Forall (fun r => ∃ c, checkBlock Yt.length (chunks32 Yt) Z ((X.drop (8 * r)).take 8) c = true)
      (List.range nb)) : StageFact Z X Yt :=
  agg_stage_aux hZ hX hYt nb (of_decide_eq_true hnb) (forall_lt_of_forall_range h)

theorem stage_X_ok {stages : List (List IPt)} (hst : stages.all okPts = true) (key : ℕ × ℕ × ℕ)
    (i : ℕ) : okPts (([initI key.1 key.2.1 key.2.2] :: stages).getD i []) = true := by
  rcases i with _ | i
  · simp [okPts, okPt_initI]
  · simpa using agg_getD_okPts stages i hst

theorem stage_Yt_ok {Z : List IPt} (hZ : checkZ Z = true) {stages : List (List IPt)}
    (hst : stages.all okPts = true) (i : ℕ) : okPts ((stages ++ [Z]).getD i []) = true := by
  have hall : (stages ++ [Z]).all okPts = true := by
    simp only [List.all_append, Bool.and_eq_true, List.all_cons, List.all_nil, Bool.and_true]
    exact ⟨hst, checkZ_okPts hZ⟩
  exact agg_getD_okPts _ i hall

theorem chain1_table {Z : List IPt} (hZ : checkZ Z = true)
    {es : List ((ℕ × ℕ × ℕ) × List (List (ℕ × ℕ × ℕ)))}
    (h : checkChain1 Z.length (chunks32 Z) Z es = true) :
    ∀ e ∈ es.map (fun e => (e.1, 1)), ChainFact Z e := by
  intro e he
  obtain ⟨e0, he0, rfl⟩ := List.mem_map.1 he
  exact checkChain1_sound (checkZ_okPts hZ) h e0 he0

theorem chain_stages_table {Z : List IPt} (hZ : checkZ Z = true) (key : ℕ × ℕ × ℕ)
    (stages : List (List IPt)) (hst : stages.all okPts = true)
    (hfacts : List.Forall (fun i => StageFact Z (([initI key.1 key.2.1 key.2.2] :: stages).getD i [])
      ((stages ++ [Z]).getD i [])) (List.range (stages.length + 1))) :
    ∀ e ∈ [(key, stages.length + 1)], ChainFact Z e := by
  obtain ⟨ν, c₂, c₃⟩ := key
  intro e he
  rw [List.mem_singleton] at he
  subst he
  exact chainFact_of_stages (checkZ_okPts hZ) ν c₂ c₃ stages
    (fun Y hY => List.all_eq_true.1 hst Y hY)
    (fun i hi => forall_lt_of_forall_range hfacts i hi)

theorem leaf_table {Z : List IPt} (hZ : checkZ Z = true)
    {es : List ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ))}
    (h : checkLeaves Z.length (chunks32 Z) es = true) :
    ∀ e ∈ es.map (fun e => (e.1, ())), LeafFact Z e := by
  intro e he
  obtain ⟨e0, he0, rfl⟩ := List.mem_map.1 he
  exact checkLeaves_sound (checkZ_okPts hZ) h e0 he0

end

end MaxLeafFormal.RSCCheck