import MaxLeafFormal.DSTData
import MaxLeafFormal.Antinorm8
import MaxLeafFormal.Enclose

/-!
# Directed Steiner Tree: the three certificates

`prop:fa-dst-certs` of the paper, exact part:
the certificates of `DSTData.lean` satisfy the hypotheses (C1)–(C3) of `lem:fa-dst-cert`, with
`|Z_j| = 27, 10, 28`, `c_{Z_j} e_{2,j} ≥ 0.40, 0.41, 0.011`, and the weights `λ_j` form a
probability vector. The proof of `thm:fa-dst` uses `c_{Z_j} e_{2,j} ≥ 1/100`, which follows from the
three stated bounds (`0.011 ≥ 1/100`) and is not stated separately.

The finite part is a Boolean checker evaluated by `decide +kernel`; `checkCert_sound` turns its
`true` into the real statement `CertHyp`.
-/

namespace MaxLeafFormal.DSTCert

open Pointwise

noncomputable section

/-- The product `x ∘ x'` of `prop:fa-dst-certs`. -/
def comp (x x' : ℝ × ℝ) : ℝ × ℝ := (x.1 * (x'.1 + x'.2), x.2 * (x'.1 / 2 + x'.2))

/-- `ℛ_Z = conv(Z) + ℝ²_{≥0}`. -/
def RZ (Z : Finset (ℝ × ℝ)) : Set (ℝ × ℝ) := convexHull ℝ (Z : Set (ℝ × ℝ)) + {q | 0 ≤ q}

/-- `c_Z = min_{z ∈ Z} z₁`. -/
def cZ (Z : Finset (ℝ × ℝ)) (hZ : Z.Nonempty) : ℝ := Z.inf' hZ Prod.fst

/-- The hypotheses of lem:fa-dst-cert, verbatim. -/
def CertHyp (y e₁ e₂ : ℝ) (Z : Finset (ℝ × ℝ)) : Prop :=
  0 ≤ y ∧ 0 < e₁ ∧ 0 < e₂ ∧ (∀ z ∈ Z, 0 ≤ z ∧ 0 < z.1) ∧
  (∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z) ∧                -- (C1)
  ((1, 0) : ℝ × ℝ) ∈ e₂ • RZ Z ∧                            -- (C2)
  (∀ z ∈ Z, comp (y, 1) z ∈ e₁ • RZ Z)                      -- (C3)

/-- Coordinatewise cast `ℚ² → ℝ²`. -/
def castP (z : ℚ × ℚ) : ℝ × ℝ := ((z.1 : ℝ), (z.2 : ℝ))

/-- The real point set of a rational list. -/
def ZL (Z : List (ℚ × ℚ)) : Finset (ℝ × ℝ) := (Z.map castP).toFinset

/-- The point set of certificate `j`. -/
def ZR (j : Fin 3) : Finset (ℝ × ℝ) := ((Zq j).map fun z => ((z.1 : ℝ), (z.2 : ℝ))).toFinset

end

theorem ZR_eq (j : Fin 3) : ZR j = ZL (Zq j) := rfl

/-! ### The checker -/

section Check

/-- The product over `ℚ`. -/
def compQ (x x' : ℚ × ℚ) : ℚ × ℚ := (x.1 * (x'.1 + x'.2), x.2 * (x'.1 / 2 + x'.2))

/-- `∑ μ_k z_k` for a list of pairs `(k, μ_k)`. -/
def combQ (Z : List (ℚ × ℚ)) (mu : List (ℕ × ℚ)) : ℚ × ℚ :=
  mu.foldr (fun km acc => (acc.1 + km.2 * (Z.getD km.1 0).1, acc.2 + km.2 * (Z.getD km.1 0).2))
    (0, 0)

/-- The coefficients form a probability vector on valid indices. -/
def muOK (n : ℕ) (mu : List (ℕ × ℚ)) : Bool :=
  mu.all (fun km => decide (km.1 < n) && decide (0 ≤ km.2)) && decide ((mu.map Prod.snd).sum = 1)

/-- `s ∑ μ_k z_k ≤ P` coordinatewise: the witness that `P ∈ s • ℛ_Z`. -/
def domQ (Z : List (ℚ × ℚ)) (P : ℚ × ℚ) (s : ℚ) (mu : List (ℕ × ℚ)) : Bool :=
  muOK Z.length mu && decide (s * (combQ Z mu).1 ≤ P.1) && decide (s * (combQ Z mu).2 ≤ P.2)

/-- (C1) for every ordered pair, row-major witnesses. -/
def checkPairs (Z : List (ℚ × ℚ)) (pairs : List (List (ℕ × ℚ))) : Bool :=
  (List.range Z.length).all fun a => (List.range Z.length).all fun b =>
    domQ Z (compQ (Z.getD a 0) (Z.getD b 0)) 1 (pairs.getD (a * Z.length + b) [])

/-- `Z ≠ ∅` and every point is nonnegative with positive first coordinate. -/
def checkZ (Z : List (ℚ × ℚ)) : Bool :=
  !Z.isEmpty && Z.all (fun z => decide (0 < z.1) && decide (0 ≤ z.2))

/-- All of `CertHyp`, decided over `ℚ` with the given witnesses. -/
def checkCert (y e₁ e₂ : ℚ) (Z : List (ℚ × ℚ)) (pairs : List (List (ℕ × ℚ)))
    (c2 : List (ℕ × ℚ)) (c3 : List (List (ℕ × ℚ))) : Bool :=
  decide (0 ≤ y) && decide (0 < e₁) && decide (0 < e₂) && checkZ Z && checkPairs Z pairs &&
    domQ Z (1, 0) e₂ c2 &&
    (List.range Z.length).all (fun a => domQ Z (compQ (y, 1) (Z.getD a 0)) e₁ (c3.getD a []))

/-- `b ≤ z₁ e` for every point: the bound on `c_Z e₂`. -/
def checkCZ (Z : List (ℚ × ℚ)) (e b : ℚ) : Bool := Z.all (fun z => decide (b ≤ z.1 * e))

end Check

/-! ### Soundness -/

section Sound

theorem castP_compQ (x x' : ℚ × ℚ) : castP (compQ x x') = comp (castP x) (castP x') := by
  simp only [castP, compQ, comp]; push_cast; rfl

theorem getD_mem_ZL {Z : List (ℚ × ℚ)} {k : ℕ} (hk : k < Z.length) :
    castP (Z.getD k 0) ∈ ZL Z := by
  rw [ZL, List.mem_toFinset, List.getD_eq_getElem _ _ hk]
  exact List.mem_map_of_mem (List.getElem_mem hk)

theorem combQ_mem {Z : List (ℚ × ℚ)} (hZ : Z ≠ []) :
    ∀ mu : List (ℕ × ℚ), (∀ km ∈ mu, km.1 < Z.length ∧ 0 ≤ km.2) →
      castP (combQ Z mu) ∈ (((mu.map Prod.snd).sum : ℚ) : ℝ) • convexHull ℝ (ZL Z : Set _) := by
  have hne : (convexHull ℝ (ZL Z : Set (ℝ × ℝ))).Nonempty := by
    obtain ⟨z, hz⟩ := List.exists_mem_of_ne_nil Z hZ
    exact ⟨castP z, subset_convexHull ℝ _
      (Finset.mem_coe.2 (List.mem_toFinset.2 (List.mem_map_of_mem hz)))⟩
  intro mu
  induction mu with
  | nil =>
    intro _
    obtain ⟨z, hz⟩ := hne
    have : castP (combQ Z []) = (0 : ℝ) • z := by simp [castP, combQ]
    simpa [this] using Set.smul_mem_smul_set (a := (0 : ℝ)) hz
  | cons km mu ih =>
    intro hmu
    have hk := hmu km (List.mem_cons_self ..)
    have ih' := ih (fun x hx => hmu x (List.mem_cons_of_mem _ hx))
    have hs : (0 : ℝ) ≤ (((mu.map Prod.snd).sum : ℚ) : ℝ) := by
      exact_mod_cast List.sum_nonneg (fun x hx => by
        obtain ⟨km', hkm', rfl⟩ := List.mem_map.1 hx
        exact (hmu km' (List.mem_cons_of_mem _ hkm')).2)
    have hm : (0 : ℝ) ≤ (km.2 : ℝ) := by exact_mod_cast hk.2
    have hsplit : castP (combQ Z (km :: mu))
        = (km.2 : ℝ) • castP (Z.getD km.1 0) + castP (combQ Z mu) := by
      simp only [castP, combQ, List.foldr_cons]
      push_cast
      ext <;> simp <;> ring
    rw [hsplit, List.map_cons, List.sum_cons, Rat.cast_add,
      (convex_convexHull ℝ _).add_smul hm hs]
    exact Set.add_mem_add (Set.smul_mem_smul_set (subset_convexHull ℝ _ (getD_mem_ZL hk.1))) ih'

theorem domQ_sound {Z : List (ℚ × ℚ)} (hZ : Z ≠ []) {P : ℚ × ℚ} {s : ℚ} (hs : 0 < s)
    {mu : List (ℕ × ℚ)} (h : domQ Z P s mu = true) : castP P ∈ (s : ℝ) • RZ (ZL Z) := by
  simp only [domQ, muOK, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at h
  obtain ⟨⟨⟨hmu, hsum⟩, h1⟩, h2⟩ := h
  have hc := combQ_mem hZ mu (fun km hkm => hmu km hkm)
  rw [hsum, Rat.cast_one, one_smul] at hc
  have hsR : (0 : ℝ) < s := by exact_mod_cast hs
  have e1 : (s : ℝ) * ((combQ Z mu).1 : ℝ) ≤ (P.1 : ℝ) := by exact_mod_cast h1
  have e2 : (s : ℝ) * ((combQ Z mu).2 : ℝ) ≤ (P.2 : ℝ) := by exact_mod_cast h2
  have hd : (0 : ℝ × ℝ) ≤ (s : ℝ)⁻¹ • (castP P - (s : ℝ) • castP (combQ Z mu)) := by
    rw [Prod.le_def]
    simp only [Prod.fst_zero, Prod.snd_zero, Prod.smul_fst, Prod.smul_snd, Prod.fst_sub,
      Prod.snd_sub, castP, smul_eq_mul]
    constructor
    · exact mul_nonneg (inv_nonneg.2 hsR.le) (by linarith)
    · exact mul_nonneg (inv_nonneg.2 hsR.le) (by linarith)
  have key : (s : ℝ) • (castP (combQ Z mu) + (s : ℝ)⁻¹ • (castP P - (s : ℝ) • castP (combQ Z mu)))
      = castP P := by
    rw [smul_add, smul_smul, mul_inv_cancel₀ hsR.ne', one_smul]
    abel
  have hw : castP (combQ Z mu) + (s : ℝ)⁻¹ • (castP P - (s : ℝ) • castP (combQ Z mu))
      ∈ RZ (ZL Z) :=
    Set.mem_add.2 ⟨_, hc, _, hd, rfl⟩
  exact Set.mem_smul_set.2 ⟨_, hw, key⟩

theorem checkZ_nonempty {Z : List (ℚ × ℚ)} (h : checkZ Z = true) : Z ≠ [] := by
  intro hZ; simp [checkZ, hZ] at h

theorem ZL_nonempty {Z : List (ℚ × ℚ)} (hZ : Z ≠ []) : (ZL Z).Nonempty := by
  obtain ⟨z, hz⟩ := List.exists_mem_of_ne_nil Z hZ
  exact ⟨castP z, List.mem_toFinset.2 (List.mem_map_of_mem hz)⟩

theorem checkZ_sound {Z : List (ℚ × ℚ)} (h : checkZ Z = true) :
    ∀ z ∈ ZL Z, 0 ≤ z ∧ 0 < z.1 := by
  intro z hz
  simp only [ZL, List.mem_toFinset, List.mem_map] at hz
  obtain ⟨a, ha, rfl⟩ := hz
  simp only [checkZ, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at h
  obtain ⟨-, hall⟩ := h
  obtain ⟨h1, h2⟩ := hall a ha
  refine ⟨?_, ?_⟩
  · show ((0 : ℝ), (0 : ℝ)) ≤ ((a.1 : ℝ), (a.2 : ℝ))
    exact Prod.mk_le_mk.2 ⟨by exact_mod_cast h1.le, by exact_mod_cast h2⟩
  · show (0 : ℝ) < (a.1 : ℝ)
    exact_mod_cast h1

theorem checkPairs_sound {Z : List (ℚ × ℚ)} (hZ : Z ≠ []) {pairs : List (List (ℕ × ℚ))}
    (h : checkPairs Z pairs = true) :
    ∀ z ∈ ZL Z, ∀ z' ∈ ZL Z, comp z z' ∈ RZ (ZL Z) := by
  intro z hz z' hz'
  simp only [ZL, List.mem_toFinset, List.mem_map] at hz hz'
  obtain ⟨a, ha, rfl⟩ := hz
  obtain ⟨b, hb, rfl⟩ := hz'
  obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem ha
  obtain ⟨j, hj, rfl⟩ := List.getElem_of_mem hb
  simp only [checkPairs, List.all_eq_true, List.mem_range] at h
  have := domQ_sound hZ one_pos (h i hi j hj)
  rw [Rat.cast_one, one_smul, castP_compQ, List.getD_eq_getElem _ _ hi,
    List.getD_eq_getElem _ _ hj] at this
  exact this

theorem checkCert_sound {y e₁ e₂ : ℚ} {Z : List (ℚ × ℚ)} {pairs : List (List (ℕ × ℚ))}
    {c2 : List (ℕ × ℚ)} {c3 : List (List (ℕ × ℚ))}
    (h : checkCert y e₁ e₂ Z pairs c2 c3 = true) :
    CertHyp (y : ℝ) (e₁ : ℝ) (e₂ : ℝ) (ZL Z) := by
  simp only [checkCert, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true,
    List.mem_range] at h
  obtain ⟨⟨⟨⟨⟨⟨hy, he₁⟩, he₂⟩, hZc⟩, hpairs⟩, hc2⟩, hc3⟩ := h
  have hZ := checkZ_nonempty hZc
  have he₁R : (0 : ℝ) < e₁ := by exact_mod_cast he₁
  have he₂R : (0 : ℝ) < e₂ := by exact_mod_cast he₂
  have h2 := domQ_sound hZ he₂ hc2
  have hP2 : castP ((1 : ℚ), (0 : ℚ)) = ((1 : ℝ), (0 : ℝ)) := by simp [castP]
  rw [hP2] at h2
  have h3 : castP ((y : ℚ), (1 : ℚ)) = ((y : ℝ), (1 : ℝ)) := by simp [castP]
  unfold CertHyp
  refine ⟨by exact_mod_cast hy, he₁R, he₂R, checkZ_sound hZc, checkPairs_sound hZ hpairs,
    h2, ?_⟩
  intro z hz
  simp only [ZL, List.mem_toFinset, List.mem_map] at hz
  obtain ⟨w, hw, rfl⟩ := hz
  obtain ⟨a, ha, rfl⟩ := List.getElem_of_mem hw
  have hd := domQ_sound hZ he₁ (hc3 a ha)
  rw [castP_compQ, h3, List.getD_eq_getElem _ _ ha] at hd
  exact hd

theorem checkCZ_sound {Z : List (ℚ × ℚ)} (hZ : Z ≠ []) {e b : ℚ} (he : 0 < e)
    (h : checkCZ Z e b = true) : (b : ℝ) ≤ cZ (ZL Z) (ZL_nonempty hZ) * (e : ℝ) := by
  have hall : ∀ z ∈ Z, b ≤ z.1 * e := by
    intro z hz
    simp only [checkCZ, List.all_eq_true, decide_eq_true_eq] at h
    exact h z hz
  have hR : (0 : ℝ) < e := by exact_mod_cast he
  have hb : (b : ℝ) / (e : ℝ) ≤ cZ (ZL Z) (ZL_nonempty hZ) := by
    unfold cZ
    apply Finset.le_inf'
    intro w hw
    simp only [ZL, List.mem_toFinset, List.mem_map] at hw
    obtain ⟨z, hz, rfl⟩ := hw
    show (b : ℝ) / (e : ℝ) ≤ ((z.1 : ℚ) : ℝ)
    rw [div_le_iff₀ hR]
    exact_mod_cast hall z hz
  exact (div_le_iff₀ hR).1 hb

theorem castP_injective : Function.Injective castP := by
  intro x y hxy
  simp only [castP, Prod.mk.injEq] at hxy
  exact Prod.ext (by exact_mod_cast hxy.1) (by exact_mod_cast hxy.2)

theorem card_ZL {Z : List (ℚ × ℚ)} (h : Z.Nodup) : (ZL Z).card = Z.length := by
  unfold ZL
  rw [List.toFinset_card_of_nodup (List.Nodup.map castP_injective h), List.length_map]

end Sound

/-! ### The data, checked in the kernel -/

theorem cert0_ok : checkCert (y 0) (e₁ 0) (e₂ 0) (Zq 0) (pairs 0) (c2w 0) (c3w 0) = true := by
  decide +kernel
theorem cert1_ok : checkCert (y 1) (e₁ 1) (e₂ 1) (Zq 1) (pairs 1) (c2w 1) (c3w 1) = true := by
  decide +kernel
theorem cert2_ok : checkCert (y 2) (e₁ 2) (e₂ 2) (Zq 2) (pairs 2) (c2w 2) (c3w 2) = true := by
  decide +kernel

theorem cz0_ok : checkCZ (Zq 0) (e₂ 0) (40/100) = true := by decide +kernel
theorem cz1_ok : checkCZ (Zq 1) (e₂ 1) (41/100) = true := by decide +kernel
theorem cz2_ok : checkCZ (Zq 2) (e₂ 2) (11/1000) = true := by decide +kernel

theorem Zq_nodup (j : Fin 3) : (Zq j).Nodup := by
  fin_cases j <;> decide +kernel

theorem Zq_ne_nil (j : Fin 3) : Zq j ≠ [] := by
  fin_cases j <;> decide +kernel

theorem ZR_nonempty (j : Fin 3) : (ZR j).Nonempty := ZL_nonempty (Zq_ne_nil j)

/-- prop:fa-dst-certs, exact part. -/
theorem dst_certs_exact :
    (∀ j, CertHyp (y j) (e₁ j) (e₂ j) (ZR j)) ∧
    (ZR 0).card = 27 ∧ (ZR 1).card = 10 ∧ (ZR 2).card = 28 ∧
    (40/100 : ℝ) ≤ cZ (ZR 0) (ZR_nonempty 0) * e₂ 0 ∧
    (41/100 : ℝ) ≤ cZ (ZR 1) (ZR_nonempty 1) * e₂ 1 ∧
    (11/1000 : ℝ) ≤ cZ (ZR 2) (ZR_nonempty 2) * e₂ 2 ∧
    (∀ j, 0 ≤ lam j) ∧ ∑ j, lam j = 1 := by
  have hC : ∀ j, CertHyp (y j) (e₁ j) (e₂ j) (ZR j) := by
    intro j
    fin_cases j
    · exact checkCert_sound cert0_ok
    · exact checkCert_sound cert1_ok
    · exact checkCert_sound cert2_ok
  have he0 : (0 : ℚ) < e₂ 0 := by norm_num [e₂, q]
  have he1 : (0 : ℚ) < e₂ 1 := by norm_num [e₂, q]
  have he2 : (0 : ℚ) < e₂ 2 := by norm_num [e₂, q]
  have c0 : ((40/100 : ℚ) : ℝ) ≤ cZ (ZR 0) (ZR_nonempty 0) * ((e₂ 0 : ℚ) : ℝ) :=
    checkCZ_sound (Zq_ne_nil 0) he0 cz0_ok
  have c1 : ((41/100 : ℚ) : ℝ) ≤ cZ (ZR 1) (ZR_nonempty 1) * ((e₂ 1 : ℚ) : ℝ) :=
    checkCZ_sound (Zq_ne_nil 1) he1 cz1_ok
  have c2 : ((11/1000 : ℚ) : ℝ) ≤ cZ (ZR 2) (ZR_nonempty 2) * ((e₂ 2 : ℚ) : ℝ) :=
    checkCZ_sound (Zq_ne_nil 2) he2 cz2_ok
  have k0 : ((40/100 : ℚ) : ℝ) = (40/100 : ℝ) := by norm_num
  have k1 : ((41/100 : ℚ) : ℝ) = (41/100 : ℝ) := by norm_num
  have k2 : ((11/1000 : ℚ) : ℝ) = (11/1000 : ℝ) := by norm_num
  rw [k0] at c0
  rw [k1] at c1
  rw [k2] at c2
  refine ⟨hC, ?_, ?_, ?_, c0, c1, c2, ?_, ?_⟩
  · rw [ZR_eq 0, card_ZL (Zq_nodup 0)]; rfl
  · rw [ZR_eq 1, card_ZL (Zq_nodup 1)]; rfl
  · rw [ZR_eq 2, card_ZL (Zq_nodup 2)]; rfl
  · intro j
    fin_cases j <;> norm_num [lam, q]
  · norm_num [lam, q, Fin.sum_univ_three]


/-! ### `lem:fa-dst-cert` for the two-state recursion

The vectors `ψ_v` of the paper on a rooted tree whose nodes are labelled `term` (a vertex of
`K ∪ {r}`) or `steiner` (a vertex of `S`); children are merged in list order. Under `CertHyp`,
`(ψ_r)₁ ≥ c_Z e₁^(count .steiner t) e₂^(count .term t)` for every tree with no Steiner leaf (`dst_tree_bound`).
When the root is labelled `term` (`rootKind t = .term`), as in `lem:fa-dst-cert`, `count .steiner t = s` and
`count .term t = p + 1` (the `p` terminals and the root). With `dst_rec` (below), the identity
`W_A = (ψ_r)₁` (`lem:fa-dst-rec`), this gives `lem:fa-dst-cert` for `W_A`: `dst_tree_bound_WA`. -/

section Recursion

open Antinorm8

/-- The label of a vertex: `term` for `K ∪ {r}`, `steiner` for `S`. -/
inductive Kind
  | term
  | steiner
  deriving DecidableEq

noncomputable section

/-- `Init_v`. -/
def initV (y : ℝ) : Kind → ℝ × ℝ
  | .term => (1, 0)
  | .steiner => (y, 1)

mutual
/-- `ψ_v`, the left fold over the children. -/
def psi (y : ℝ) : RTree Kind → ℝ × ℝ
  | .node k cs => psiFold y (initV y k) cs
/-- Merge the children's vectors one by one, in order. -/
def psiFold (y : ℝ) : ℝ × ℝ → List (RTree Kind) → ℝ × ℝ
  | acc, [] => acc
  | acc, c :: cs => psiFold y (comp acc (psi y c)) cs
end

end

mutual
/-- The number of nodes with label `k`. -/
def count (k : Kind) : RTree Kind → ℕ
  | .node k' cs => (if k' = k then 1 else 0) + countAll k cs
def countAll (k : Kind) : List (RTree Kind) → ℕ
  | [] => 0
  | c :: cs => count k c + countAll k cs
end

mutual
/-- Every node labelled `steiner` has a child. -/
def NoSteinerLeaf : RTree Kind → Prop
  | .node k cs => (k = .steiner → cs ≠ []) ∧ NoSteinerLeafAll cs
def NoSteinerLeafAll : List (RTree Kind) → Prop
  | [] => True
  | c :: cs => NoSteinerLeaf c ∧ NoSteinerLeafAll cs
end

/-- The label of the root. -/
def rootKind : RTree Kind → Kind
  | .node k _ => k

/-! ### Helper lemmas for `dst_tree_bound` -/

theorem rec_comp_smul_smul (c d : ℝ) (x x' : ℝ × ℝ) :
    comp (c • x) (d • x') = (c * d) • comp x x' := by
  ext <;> simp [comp] <;> ring

theorem rec_comp_add_right (x u v : ℝ × ℝ) (a b : ℝ) :
    comp x (a • u + b • v) = a • comp x u + b • comp x v := by
  ext <;> simp [comp] <;> ring

theorem rec_comp_add_left (u v x' : ℝ × ℝ) (a b : ℝ) :
    comp (a • u + b • v) x' = a • comp u x' + b • comp v x' := by
  ext <;> simp [comp] <;> ring

theorem rec_convex_RZ (Z : Finset (ℝ × ℝ)) : Convex ℝ (RZ Z) :=
  (convex_convexHull ℝ _).add (convex_Ici 0)

theorem rec_nonneg_comp {x x' : ℝ × ℝ} (hx : 0 ≤ x) (hx' : 0 ≤ x') : 0 ≤ comp x x' := by
  rw [Prod.le_def] at hx hx' ⊢
  simp only [Prod.fst_zero, Prod.snd_zero, comp] at hx hx' ⊢
  exact ⟨mul_nonneg hx.1 (by linarith [hx'.1, hx'.2]), mul_nonneg hx.2 (by linarith [hx'.1, hx'.2])⟩

theorem rec_nonneg_hull {Z : Finset (ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) {h : ℝ × ℝ}
    (hh : h ∈ convexHull ℝ (Z : Set (ℝ × ℝ))) : 0 ≤ h :=
  convexHull_min (fun z hz => hZ0 z hz) (convex_Ici 0) hh

theorem rec_mem_RZ_of_hull {Z : Finset (ℝ × ℝ)} {h : ℝ × ℝ}
    (hh : h ∈ convexHull ℝ (Z : Set (ℝ × ℝ))) : h ∈ RZ Z := by
  unfold RZ
  rw [Set.mem_add]
  exact ⟨h, hh, 0, le_refl (0 : ℝ × ℝ), add_zero h⟩

theorem rec_add_nonneg {Z : Finset (ℝ × ℝ)} {w r : ℝ × ℝ} (hw : w ∈ RZ Z) (hr : 0 ≤ r) :
    w + r ∈ RZ Z := by
  unfold RZ at *
  rw [Set.mem_add] at hw ⊢
  obtain ⟨h, hh, q, hq, rfl⟩ := hw
  exact ⟨h, hh, q + r, add_nonneg hq hr, by abel⟩

theorem rec_add_mem_smul {Z : Finset (ℝ × ℝ)} {c : ℝ} (hc : 0 < c) {a r : ℝ × ℝ}
    (ha : a ∈ c • RZ Z) (hr : 0 ≤ r) : a + r ∈ c • RZ Z := by
  obtain ⟨w, hw, rfl⟩ := Set.mem_smul_set.mp ha
  refine Set.mem_smul_set.mpr ⟨w + c⁻¹ • r, rec_add_nonneg hw (smul_nonneg (inv_nonneg.mpr hc.le) hr), ?_⟩
  rw [smul_add, smul_smul, mul_inv_cancel₀ hc.ne', one_smul]

theorem rec_comp_mem_of_Z {Z : Finset (ℝ × ℝ)} (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z)
    {z : ℝ × ℝ} (hz : z ∈ Z) {v : ℝ × ℝ} (hv : v ∈ convexHull ℝ (Z : Set (ℝ × ℝ))) :
    comp z v ∈ RZ Z := by
  have key : convexHull ℝ (Z : Set (ℝ × ℝ)) ⊆ {u | comp z u ∈ RZ Z} := by
    refine convexHull_min (fun z' hz' => hC1 z hz z' hz') ?_
    intro u hu w hw a b ha hb hab
    simp only [Set.mem_ofPred_eq] at hu hw ⊢
    rw [rec_comp_add_right]
    exact rec_convex_RZ Z hu hw ha hb hab
  exact key hv

theorem rec_comp_mem_hull {Z : Finset (ℝ × ℝ)} (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z)
    {v v' : ℝ × ℝ} (hv : v ∈ convexHull ℝ (Z : Set (ℝ × ℝ)))
    (hv' : v' ∈ convexHull ℝ (Z : Set (ℝ × ℝ))) : comp v v' ∈ RZ Z := by
  have key : convexHull ℝ (Z : Set (ℝ × ℝ)) ⊆
      {u | ∀ u' ∈ convexHull ℝ (Z : Set (ℝ × ℝ)), comp u u' ∈ RZ Z} := by
    refine convexHull_min ?_ ?_
    · intro z hz u' hu'
      exact rec_comp_mem_of_Z hC1 hz hu'
    · intro u hu w hw a b ha hb hab
      simp only [Set.mem_ofPred_eq] at hu hw ⊢
      intro u' hu'
      rw [rec_comp_add_left]
      exact rec_convex_RZ Z (hu u' hu') (hw u' hu') ha hb hab
  exact key hv v' hv'

theorem rec_comp_mem_RZ {Z : Finset (ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z) {w w' : ℝ × ℝ} (hw : w ∈ RZ Z)
    (hw' : w' ∈ RZ Z) : comp w w' ∈ RZ Z := by
  unfold RZ at hw hw'
  rw [Set.mem_add] at hw hw'
  obtain ⟨h, hh, q, hq, rfl⟩ := hw
  obtain ⟨h', hh', q', hq', rfl⟩ := hw'
  have e : comp (h + q) (h' + q') = comp h h' + (comp h q' + comp q h' + comp q q') := by
    ext <;> simp [comp] <;> ring
  have hr : 0 ≤ comp h q' + comp q h' + comp q q' :=
    add_nonneg (add_nonneg (rec_nonneg_comp (rec_nonneg_hull hZ0 hh) hq')
      (rec_nonneg_comp hq (rec_nonneg_hull hZ0 hh'))) (rec_nonneg_comp hq hq')
  rw [e]
  exact rec_add_nonneg (rec_comp_mem_hull hC1 hh hh') hr

theorem rec_comp_smul_mem {Z : Finset (ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z) {η η' : ℝ} {x x' : ℝ × ℝ}
    (hx : x ∈ η • RZ Z) (hx' : x' ∈ η' • RZ Z) : comp x x' ∈ (η * η') • RZ Z := by
  obtain ⟨w, hw, rfl⟩ := Set.mem_smul_set.mp hx
  obtain ⟨w', hw', rfl⟩ := Set.mem_smul_set.mp hx'
  rw [rec_comp_smul_smul]
  exact Set.smul_mem_smul_set (rec_comp_mem_RZ hZ0 hC1 hw hw')

theorem rec_comp_Y_mem {Z : Finset (ℝ × ℝ)} {y e₁ : ℝ} (hy : 0 ≤ y) (he₁ : 0 < e₁)
    (hC3 : ∀ z ∈ Z, comp (y, 1) z ∈ e₁ • RZ Z) {w : ℝ × ℝ} (hw : w ∈ RZ Z) :
    comp (y, 1) w ∈ e₁ • RZ Z := by
  have hY : (0 : ℝ × ℝ) ≤ (y, 1) := by
    rw [Prod.le_def]
    exact ⟨hy, zero_le_one⟩
  have key : convexHull ℝ (Z : Set (ℝ × ℝ)) ⊆ {u | comp (y, 1) u ∈ e₁ • RZ Z} := by
    refine convexHull_min (fun z hz => hC3 z hz) ?_
    intro u hu v hv a b ha hb hab
    simp only [Set.mem_ofPred_eq] at hu hv ⊢
    rw [rec_comp_add_right]
    exact ((rec_convex_RZ Z).smul e₁) hu hv ha hb hab
  unfold RZ at hw
  rw [Set.mem_add] at hw
  obtain ⟨h, hh, q, hq, rfl⟩ := hw
  have e : comp (y, 1) (h + q) = comp (y, 1) h + comp (y, 1) q := by
    ext <;> simp [comp] <;> ring
  rw [e]
  exact rec_add_mem_smul he₁ (key hh) (rec_nonneg_comp hY hq)

theorem rec_comp_Y_smul_mem {Z : Finset (ℝ × ℝ)} {y e₁ η : ℝ} (hy : 0 ≤ y) (he₁ : 0 < e₁)
    (hC3 : ∀ z ∈ Z, comp (y, 1) z ∈ e₁ • RZ Z) {x' : ℝ × ℝ} (hx' : x' ∈ η • RZ Z) :
    comp (y, 1) x' ∈ (e₁ * η) • RZ Z := by
  obtain ⟨w, hw, rfl⟩ := Set.mem_smul_set.mp hx'
  obtain ⟨u, hu, hue⟩ := Set.mem_smul_set.mp (rec_comp_Y_mem hy he₁ hC3 hw)
  refine Set.mem_smul_set.mpr ⟨u, hu, ?_⟩
  have e : comp (y, 1) (η • w) = η • comp (y, 1) w := by
    ext <;> simp [comp] <;> ring
  rw [e, ← hue, smul_smul, mul_comm]

theorem rec_cZ_le {Z : Finset (ℝ × ℝ)} (hZ : Z.Nonempty) {w : ℝ × ℝ} (hw : w ∈ RZ Z) :
    cZ Z hZ ≤ w.1 := by
  unfold RZ at hw
  rw [Set.mem_add] at hw
  obtain ⟨h, hh, q, hq, rfl⟩ := hw
  have hsub : (Z : Set (ℝ × ℝ)) ⊆ {p : ℝ × ℝ | cZ Z hZ ≤ p.1} := by
    intro z hz
    have := Finset.inf'_le (s := Z) Prod.fst (Finset.mem_coe.mp hz)
    simp only [Set.mem_ofPred_eq]
    unfold cZ
    exact this
  have hconv : Convex ℝ {p : ℝ × ℝ | cZ Z hZ ≤ p.1} := by
    intro x hx y hy a b ha hb hab
    simp only [Set.mem_ofPred_eq, Prod.smul_fst, Prod.fst_add, smul_eq_mul] at hx hy ⊢
    have hsum : a * cZ Z hZ + b * cZ Z hZ = cZ Z hZ := by
      rw [← add_mul, hab, one_mul]
    nlinarith [mul_le_mul_of_nonneg_left hx ha, mul_le_mul_of_nonneg_left hy hb]
  have hc : cZ Z hZ ≤ h.1 := convexHull_min hsub hconv hh
  have hq1 : (0 : ℝ) ≤ q.1 := (Prod.le_def.mp hq).1
  simp only [Prod.fst_add]
  linarith

theorem rec_noLeafAll_iff (cs : List (RTree Kind)) :
    NoSteinerLeafAll cs ↔ ∀ c ∈ cs, NoSteinerLeaf c := by
  induction cs with
  | nil => simp [NoSteinerLeafAll]
  | cons c cs ih => simp [NoSteinerLeafAll, ih]

theorem rec_fold_mem {y e₁ e₂ : ℝ} {Z : Finset (ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z) :
    ∀ (cs : List (RTree Kind)) (acc : ℝ × ℝ) (η : ℝ),
      acc ∈ η • RZ Z →
      (∀ c ∈ cs, psi y c ∈ (e₁ ^ count .steiner c * e₂ ^ count .term c) • RZ Z) →
      psiFold y acc cs ∈ (η * e₁ ^ countAll .steiner cs * e₂ ^ countAll .term cs) • RZ Z := by
  intro cs
  induction cs with
  | nil =>
    intro acc η hacc _
    simpa [psiFold, countAll] using hacc
  | cons c cs ih =>
    intro acc η hacc hT
    have hc := hT c (by simp)
    have hT' : ∀ c' ∈ cs, psi y c' ∈ (e₁ ^ count .steiner c' * e₂ ^ count .term c') • RZ Z :=
      fun c' hc' => hT c' (by simp [hc'])
    have hacc' := rec_comp_smul_mem hZ0 hC1 hacc hc
    have key := ih (comp acc (psi y c)) _ hacc' hT'
    have e : (η * (e₁ ^ count .steiner c * e₂ ^ count .term c)) * e₁ ^ countAll .steiner cs *
        e₂ ^ countAll .term cs =
        η * e₁ ^ countAll .steiner (c :: cs) * e₂ ^ countAll .term (c :: cs) := by
      simp only [countAll]
      ring
    rw [e] at key
    simpa only [psiFold] using key

theorem rec_psi_mem {y e₁ e₂ : ℝ} {Z : Finset (ℝ × ℝ)} (hy : 0 ≤ y) (he₁ : 0 < e₁)
    (_he₂ : 0 < e₂) (hZ0 : ∀ z ∈ Z, 0 ≤ z) (hC1 : ∀ z ∈ Z, ∀ z' ∈ Z, comp z z' ∈ RZ Z)
    (hC2 : ((1, 0) : ℝ × ℝ) ∈ e₂ • RZ Z) (hC3 : ∀ z ∈ Z, comp (y, 1) z ∈ e₁ • RZ Z)
    (t : RTree Kind) :
    NoSteinerLeaf t → psi y t ∈ (e₁ ^ count .steiner t * e₂ ^ count .term t) • RZ Z := by
  refine RTree.ind (fun t => NoSteinerLeaf t →
    psi y t ∈ (e₁ ^ count .steiner t * e₂ ^ count .term t) • RZ Z) ?_ t
  intro a cs ih hl
  have hl' : (a = .steiner → cs ≠ []) ∧ NoSteinerLeafAll cs := hl
  have hT : ∀ c ∈ cs, psi y c ∈ (e₁ ^ count .steiner c * e₂ ^ count .term c) • RZ Z :=
    fun c hc => ih c hc ((rec_noLeafAll_iff cs).1 hl'.2 c hc)
  cases a with
  | term =>
    have hcount : e₁ ^ count .steiner (RTree.node Kind.term cs) *
        e₂ ^ count .term (RTree.node Kind.term cs) =
        e₂ * e₁ ^ countAll .steiner cs * e₂ ^ countAll .term cs := by
      simp [count]
      ring
    simp only [psi, initV]
    rw [hcount]
    exact rec_fold_mem hZ0 hC1 cs (1, 0) e₂ hC2 hT
  | steiner =>
    cases cs with
    | nil => exact absurd rfl (hl'.1 rfl)
    | cons c rest =>
      have hNL := (rec_noLeafAll_iff _).1 hl'.2
      have hc0 : NoSteinerLeaf c := hNL c (by simp)
      have hTc := ih c (by simp) hc0
      have hY := rec_comp_Y_smul_mem hy he₁ hC3 hTc
      have hTr : ∀ c' ∈ rest, psi y c' ∈ (e₁ ^ count .steiner c' * e₂ ^ count .term c') • RZ Z :=
        fun c' hc' => hT c' (by simp [hc'])
      have key := rec_fold_mem hZ0 hC1 rest _ _ hY hTr
      have hpsi : psi y (RTree.node Kind.steiner (c :: rest)) =
          psiFold y (comp (y, 1) (psi y c)) rest := by
        simp only [psi, initV, psiFold]
      have hcount : e₁ ^ count .steiner (RTree.node Kind.steiner (c :: rest)) *
          e₂ ^ count .term (RTree.node Kind.steiner (c :: rest)) =
          e₁ * (e₁ ^ count .steiner c * e₂ ^ count .term c) * e₁ ^ countAll .steiner rest *
            e₂ ^ countAll .term rest := by
        simp [count, countAll]
        ring
      rw [hpsi, hcount]
      exact key

/-- lem:fa-dst-cert for the recursion. -/
theorem dst_tree_bound (y e₁ e₂ : ℝ) (Z : Finset (ℝ × ℝ)) (hZ : Z.Nonempty)
    (h : CertHyp y e₁ e₂ Z) (t : RTree Kind) (hl : NoSteinerLeaf t) :
    cZ Z hZ * e₁ ^ count .steiner t * e₂ ^ count .term t ≤ (psi y t).1 := by
  obtain ⟨hy, he₁, he₂, hZp, hC1, hC2, hC3⟩ := h
  have hZ0 : ∀ z ∈ Z, 0 ≤ z := fun z hz => (hZp z hz).1
  obtain ⟨w, hw, hwe⟩ := Set.mem_smul_set.mp
    (rec_psi_mem hy he₁ he₂ hZ0 hC1 hC2 hC3 t hl)
  have hX : 0 < e₁ ^ count .steiner t * e₂ ^ count .term t :=
    mul_pos (pow_pos he₁ _) (pow_pos he₂ _)
  have hw1 : cZ Z hZ ≤ w.1 := rec_cZ_le hZ hw
  rw [← hwe, Prod.smul_fst, smul_eq_mul]
  nlinarith [mul_le_mul_of_nonneg_left hw1 hX.le]

/-! ### `lem:fa-dst-rec`, `W_A = (ψ_r)₁`

A node is addressed by its position, the list of child indices on the path from the root.
The definitions below model the paper's out-arborescence when the root is labelled `term`, as `r` is
(`rootKind t = .term`, the hypothesis of `dst_rec` and `dst_tree_bound_WA`); then `inKbar` contains
the root, as `\bar K_X` contains `r`. For a `steiner` root they are defined but are not the paper's. -/

/-- The label at a position (`none` off the tree). -/
def labelAt : RTree Kind → List ℕ → Option Kind
  | .node k _, [] => some k
  | .node _ cs, i :: p => (cs[i]?).bind (fun c => labelAt c p)

/-- `List.cons i` as an embedding. -/
def consEmb (i : ℕ) : List ℕ ↪ List ℕ := ⟨List.cons i, List.cons_injective⟩

mutual
/-- Positions of the nodes of `t`. -/
def positions : RTree Kind → Finset (List ℕ)
  | .node _ cs => insert [] (positionsAll 0 cs)
/-- Positions in a list of subtrees, the first of which has child index `i`. -/
def positionsAll : ℕ → List (RTree Kind) → Finset (List ℕ)
  | _, [] => ∅
  | i, c :: cs => (positions c).map (consEmb i) ∪ positionsAll (i + 1) cs
end

/-- The positions of `S`. -/
def steinerPos (t : RTree Kind) : Finset (List ℕ) :=
  (positions t).filter (fun p => labelAt t p = some .steiner)

/-- Membership in `\bar K_X = {r} ∪ K ∪ X`: the positions labelled `term`, and `X`. -/
abbrev inKbar (t : RTree Kind) (X : Finset (List ℕ)) (p : List ℕ) : Prop :=
  labelAt t p = some .term ∨ p ∈ X

/-- `Ψ_A(X)`: non-root nodes in `K ∪ X` whose parent is not in `\bar K_X`. -/
def PsiA (t : RTree Kind) (X : Finset (List ℕ)) : ℕ :=
  ((positions t).filter (fun p => p ≠ [] ∧ inKbar t X p ∧ ¬ inKbar t X p.dropLast)).card

/-- `W_A(y)` (`eq:fa-dst-W`). -/
noncomputable def WA (y : ℝ) (t : RTree Kind) : ℝ :=
  ∑ X ∈ (steinerPos t).powerset, y ^ X.card * (1 / 2 : ℝ) ^ PsiA t X

/-! #### Helpers for `dst_rec` -/

/-- The weight of one sample. -/
noncomputable def wtA (y : ℝ) (t : RTree Kind) (X : Finset (List ℕ)) : ℝ :=
  y ^ X.card * (1 / 2 : ℝ) ^ PsiA t X

/-- The two-coordinate version of `W_A`: the samples putting the root in state 1 (in `\bar K_X`)
and in state 2 (an unsampled Steiner root). -/
noncomputable def WA2 (y : ℝ) (t : RTree Kind) : ℝ × ℝ :=
  (∑ X ∈ (steinerPos t).powerset, if inKbar t X [] then wtA y t X else 0,
   ∑ X ∈ (steinerPos t).powerset, if inKbar t X [] then 0 else wtA y t X)

@[simp] theorem consEmb_apply (i : ℕ) (q : List ℕ) : consEmb i q = i :: q := rfl

theorem labelAt_nil (k : Kind) (cs : List (RTree Kind)) : labelAt (.node k cs) [] = some k := by
  rw [labelAt]

theorem labelAt_cons (k : Kind) (cs : List (RTree Kind)) (i : ℕ) (p : List ℕ) :
    labelAt (.node k cs) (i :: p) = (cs[i]?).bind (fun c => labelAt c p) := by
  rw [labelAt]

theorem positions_node (k : Kind) (cs : List (RTree Kind)) :
    positions (.node k cs) = insert [] (positionsAll 0 cs) := by
  rw [positions]

theorem positionsAll_nil (i : ℕ) : positionsAll i [] = ∅ := by
  rw [positionsAll]

theorem positionsAll_cons (i : ℕ) (c : RTree Kind) (cs : List (RTree Kind)) :
    positionsAll i (c :: cs) = (positions c).map (consEmb i) ∪ positionsAll (i + 1) cs := by
  rw [positionsAll]

theorem mem_positionsAll_aux (cs : List (RTree Kind))
    (hcs : ∀ c ∈ cs, ∀ p, p ∈ positions c ↔ (labelAt c p).isSome) :
    ∀ (i : ℕ) (p : List ℕ), p ∈ positionsAll i cs ↔
      ∃ a q, p = a :: q ∧ i ≤ a ∧ ((cs[a - i]?).bind (fun c => labelAt c q)).isSome := by
  induction cs with
  | nil => intro i p; simp [positionsAll_nil]
  | cons c cs ih =>
    intro i p
    have ih' := ih (fun c' hc' => hcs c' (List.mem_cons_of_mem _ hc'))
    have hc := hcs c (List.mem_cons_self ..)
    rw [positionsAll_cons, Finset.mem_union, Finset.mem_map, ih']
    constructor
    · rintro (⟨q, hq, rfl⟩ | ⟨a, q, rfl, ha, hs⟩)
      · refine ⟨i, q, rfl, le_rfl, ?_⟩
        simpa using (hc q).1 hq
      · refine ⟨a, q, rfl, by omega, ?_⟩
        have e : a - i = (a - (i + 1)) + 1 := by omega
        rw [e, List.getElem?_cons_succ]
        exact hs
    · rintro ⟨a, q, rfl, ha, hs⟩
      rcases Nat.eq_or_lt_of_le ha with rfl | hlt
      · left
        exact ⟨q, (hc q).2 (by simpa using hs), rfl⟩
      · right
        refine ⟨a, q, rfl, hlt, ?_⟩
        have e : a - i = (a - (i + 1)) + 1 := by omega
        rw [e, List.getElem?_cons_succ] at hs
        exact hs

/-- The positions are exactly the addresses with a label. -/
theorem mem_positions_iff {t : RTree Kind} {p : List ℕ} :
    p ∈ positions t ↔ (labelAt t p).isSome := by
  have key : ∀ t : RTree Kind, ∀ p, p ∈ positions t ↔ (labelAt t p).isSome := by
    refine RTree.ind (fun t => ∀ p, p ∈ positions t ↔ (labelAt t p).isSome) ?_
    intro k cs ih p
    rw [positions_node, Finset.mem_insert, mem_positionsAll_aux cs ih]
    cases p with
    | nil => simp [labelAt_nil]
    | cons a q => simp [labelAt_cons]
  exact key t p

theorem nil_mem_positions (t : RTree Kind) : [] ∈ positions t := by
  cases t with
  | node k cs => rw [mem_positions_iff, labelAt_nil]; rfl

/-- All first indices below `n`. -/
def OldPos (n : ℕ) (p : List ℕ) : Prop := ∀ i q, p = i :: q → i < n

theorem OldPos.dropLast {n : ℕ} {p : List ℕ} (hp : OldPos n p) : OldPos n p.dropLast := by
  match p, hp with
  | [], _ => intro i q h; simp at h
  | [_], _ => intro i q h; simp at h
  | a :: b :: r, hp =>
    intro i q h
    have h' : (a :: b :: r).dropLast = a :: (b :: r).dropLast := rfl
    rw [h'] at h
    obtain ⟨h1, -⟩ := List.cons.inj h
    rw [← h1]
    exact hp a (b :: r) rfl

theorem oldPos_nil (n : ℕ) : OldPos n [] := by
  intro i q h
  simp at h

theorem dropLast_cons_ne (j : ℕ) {q : List ℕ} (hq : q ≠ []) : (j :: q).dropLast = j :: q.dropLast := by
  match q, hq with
  | [], h => exact absurd rfl h
  | _ :: _, _ => rfl

theorem old_of_mem {k : Kind} {pre : List (RTree Kind)} {p : List ℕ}
    (hp : p ∈ positions (.node k pre)) : OldPos pre.length p := by
  rintro i q rfl
  rw [mem_positions_iff, labelAt_cons] at hp
  by_contra h
  push Not at h
  rw [List.getElem?_eq_none h] at hp
  simp at hp

theorem labelAt_snoc_old (k : Kind) (pre : List (RTree Kind)) (c : RTree Kind) {p : List ℕ}
    (hp : OldPos pre.length p) :
    labelAt (.node k (pre ++ [c])) p = labelAt (.node k pre) p := by
  cases p with
  | nil => rw [labelAt_nil, labelAt_nil]
  | cons i q => rw [labelAt_cons, labelAt_cons, List.getElem?_append_left (hp i q rfl)]

theorem labelAt_snoc_new (k : Kind) (pre : List (RTree Kind)) (c : RTree Kind) (q : List ℕ) :
    labelAt (.node k (pre ++ [c])) (pre.length :: q) = labelAt c q := by
  rw [labelAt_cons]
  simp

theorem positionsAll_append (c : RTree Kind) :
    ∀ (l : List (RTree Kind)) (i : ℕ),
      positionsAll i (l ++ [c]) = positionsAll i l ∪ (positions c).map (consEmb (i + l.length)) := by
  intro l
  induction l with
  | nil => intro i; simp [positionsAll_cons, positionsAll_nil]
  | cons d l ih =>
    intro i
    rw [List.cons_append, positionsAll_cons, positionsAll_cons, ih (i + 1), Finset.union_assoc,
      List.length_cons, show i + (l.length + 1) = i + 1 + l.length by omega]

theorem positions_snoc (k : Kind) (pre : List (RTree Kind)) (c : RTree Kind) :
    positions (.node k (pre ++ [c])) =
      positions (.node k pre) ∪ (positions c).map (consEmb pre.length) := by
  rw [positions_node, positions_node, positionsAll_append, zero_add, Finset.insert_union]

theorem disjoint_old {A B : Finset (List ℕ)} {n : ℕ} (hA : ∀ p ∈ A, OldPos n p) :
    Disjoint A (B.map (consEmb n)) := by
  rw [Finset.disjoint_left]
  intro p hp hpB
  obtain ⟨q, _, rfl⟩ := Finset.mem_map.1 hpB
  exact lt_irrefl _ (hA _ hp n q rfl)

theorem steinerPos_subset (t : RTree Kind) : steinerPos t ⊆ positions t :=
  Finset.filter_subset _ _

theorem steinerPos_snoc (k : Kind) (pre : List (RTree Kind)) (c : RTree Kind) :
    steinerPos (.node k (pre ++ [c])) =
      steinerPos (.node k pre) ∪ (steinerPos c).map (consEmb pre.length) := by
  ext p
  simp only [steinerPos, Finset.mem_union, Finset.mem_filter, Finset.mem_map, positions_snoc]
  constructor
  · rintro ⟨hp | ⟨q, hq, rfl⟩, hl⟩
    · exact Or.inl ⟨hp, by rwa [labelAt_snoc_old k pre c (old_of_mem hp)] at hl⟩
    · exact Or.inr ⟨q, ⟨hq, by rwa [consEmb_apply, labelAt_snoc_new] at hl⟩, rfl⟩
  · rintro (⟨hp, hl⟩ | ⟨q, ⟨hq, hl⟩, rfl⟩)
    · exact ⟨Or.inl hp, by rwa [labelAt_snoc_old k pre c (old_of_mem hp)]⟩
    · exact ⟨Or.inr ⟨q, hq, rfl⟩, by rwa [consEmb_apply, labelAt_snoc_new]⟩

/-- Sums over the subsets of a disjoint union `s ∪ e(t)`. -/
theorem sum_powerset_union_map {α β : Type} [DecidableEq α] [DecidableEq β] (e : α ↪ β)
    (s : Finset β) :
    ∀ (t : Finset α), Disjoint s (t.map e) → ∀ f : Finset β → ℝ,
      ∑ X ∈ (s ∪ t.map e).powerset, f X =
        ∑ U ∈ s.powerset, ∑ V ∈ t.powerset, f (U ∪ V.map e) := by
  intro t
  induction t using Finset.induction_on with
  | empty => intro _ f; simp
  | insert a t ha ih =>
    intro hd f
    rw [Finset.map_insert, Finset.disjoint_insert_right] at hd
    have hnot : e a ∉ s ∪ t.map e := by
      rw [Finset.mem_union, not_or]
      exact ⟨hd.1, fun h => ha (Finset.mem_map' e |>.1 h)⟩
    rw [Finset.map_insert, Finset.union_insert, Finset.sum_powerset_insert hnot, ih hd.2 f,
      ih hd.2 (fun X => f (insert (e a) X)), ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl (fun U _ => ?_)
    rw [Finset.sum_powerset_insert ha]
    congr 1
    refine Finset.sum_congr rfl (fun V _ => ?_)
    rw [Finset.map_insert, Finset.union_insert]

theorem PsiA_eq_sum (t : RTree Kind) (X : Finset (List ℕ)) :
    PsiA t X = ∑ p ∈ positions t,
      if (p ≠ [] ∧ inKbar t X p ∧ ¬ inKbar t X p.dropLast) then 1 else 0 := by
  rw [PsiA, Finset.card_filter]

section Snoc

variable (k : Kind) (pre : List (RTree Kind)) (c : RTree Kind)
  {U V : Finset (List ℕ)}

theorem inKbar_snoc_old {p : List ℕ}
    (hp : OldPos pre.length p) :
    inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) p ↔
      inKbar (.node k pre) U p := by
  have hnot : p ∉ V.map (consEmb pre.length) := by
    intro h
    obtain ⟨q, _, rfl⟩ := Finset.mem_map.1 h
    exact lt_irrefl _ (hp _ q rfl)
  simp only [inKbar, labelAt_snoc_old k pre c hp, Finset.mem_union, hnot, or_false]

theorem inKbar_snoc_new (hU : U ⊆ steinerPos (.node k pre)) (q : List ℕ) :
    inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) (pre.length :: q) ↔
      inKbar c V q := by
  have hnot : pre.length :: q ∉ U := by
    intro h
    exact lt_irrefl _ (old_of_mem (steinerPos_subset _ (hU h)) _ q rfl)
  simp [inKbar, labelAt_snoc_new, hnot]

theorem PsiA_snoc (hU : U ⊆ steinerPos (.node k pre)) :
    PsiA (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) =
      PsiA (.node k pre) U + PsiA c V +
        (if inKbar c V [] ∧ ¬ inKbar (.node k pre) U [] then 1 else 0) := by
  have hold : ∀ p ∈ positions (.node k pre), OldPos pre.length p := fun p hp => old_of_mem hp
  rw [PsiA_eq_sum (.node k (pre ++ [c])), positions_snoc, Finset.sum_union (disjoint_old hold),
    Finset.sum_map, PsiA_eq_sum (.node k pre) U, PsiA_eq_sum c V, add_assoc]
  congr 1
  · refine Finset.sum_congr rfl (fun p hp => if_congr ?_ rfl rfl)
    rw [inKbar_snoc_old k pre c (hold p hp), inKbar_snoc_old k pre c (hold p hp).dropLast]
  · have hsplit : ∀ q ∈ positions c,
        (if (consEmb pre.length q ≠ [] ∧
            inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) (consEmb pre.length q) ∧
            ¬ inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length))
              (consEmb pre.length q).dropLast) then 1 else 0) =
        (if (q ≠ [] ∧ inKbar c V q ∧ ¬ inKbar c V q.dropLast) then 1 else 0) +
          (if q = [] then
            (if inKbar c V [] ∧ ¬ inKbar (.node k pre) U [] then 1 else 0) else 0) := by
      intro q _
      by_cases hq : q = []
      · subst hq
        have hiff : (consEmb pre.length [] ≠ [] ∧
            inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) (consEmb pre.length []) ∧
            ¬ inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length))
              (consEmb pre.length []).dropLast) ↔
            (inKbar c V [] ∧ ¬ inKbar (.node k pre) U []) := by
          rw [consEmb_apply, inKbar_snoc_new k pre c hU,
            show ([pre.length] : List ℕ).dropLast = [] from rfl,
            inKbar_snoc_old k pre c (oldPos_nil _)]
          simp
        have e1 : ¬ (([] : List ℕ) ≠ [] ∧ inKbar c V [] ∧ ¬ inKbar c V ([] : List ℕ).dropLast) := by
          simp
        rw [if_congr hiff rfl rfl, ite_eq_right e1, ite_eq_left rfl, zero_add]
      · have hiff : (consEmb pre.length q ≠ [] ∧
            inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) (consEmb pre.length q) ∧
            ¬ inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length))
              (consEmb pre.length q).dropLast) ↔
            (q ≠ [] ∧ inKbar c V q ∧ ¬ inKbar c V q.dropLast) := by
          rw [consEmb_apply, inKbar_snoc_new k pre c hU, dropLast_cons_ne _ hq,
            inKbar_snoc_new k pre c hU]
          simp [hq]
        rw [if_congr hiff rfl rfl, ite_eq_right hq, add_zero]
    rw [Finset.sum_congr rfl hsplit, Finset.sum_add_distrib, Finset.sum_ite_eq',
      ite_eq_left (nil_mem_positions c)]

theorem card_snoc (hU : U ⊆ steinerPos (.node k pre)) :
    (U ∪ V.map (consEmb pre.length)).card = U.card + V.card := by
  rw [Finset.card_union_of_disjoint
    (disjoint_old (fun p hp => old_of_mem (steinerPos_subset _ (hU hp)))), Finset.card_map]

theorem WA2_snoc (y : ℝ) :
    WA2 y (.node k (pre ++ [c])) = comp (WA2 y (.node k pre)) (WA2 y c) := by
  have hold : ∀ p ∈ steinerPos (.node k pre), OldPos pre.length p :=
    fun p hp => old_of_mem (steinerPos_subset _ hp)
  have hsum : ∀ g : Finset (List ℕ) → ℝ,
      ∑ X ∈ (steinerPos (.node k (pre ++ [c]))).powerset, g X =
        ∑ U ∈ (steinerPos (.node k pre)).powerset, ∑ V ∈ (steinerPos c).powerset,
          g (U ∪ V.map (consEmb pre.length)) := by
    intro g
    rw [steinerPos_snoc]
    exact sum_powerset_union_map _ _ _ (disjoint_old hold) g
  -- the weight of a combined sample
  have hw : ∀ U ∈ (steinerPos (.node k pre)).powerset, ∀ V : Finset (List ℕ),
      wtA y (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) =
        wtA y (.node k pre) U * wtA y c V *
          (1 / 2 : ℝ) ^ (if inKbar c V [] ∧ ¬ inKbar (.node k pre) U [] then 1 else 0) := by
    intro U hU V
    have hU' := Finset.mem_powerset.1 hU
    rw [wtA, wtA, wtA, card_snoc k pre hU', PsiA_snoc k pre c hU', pow_add, pow_add, pow_add]
    ring
  have hroot : ∀ U ∈ (steinerPos (.node k pre)).powerset, ∀ V : Finset (List ℕ),
      (inKbar (.node k (pre ++ [c])) (U ∪ V.map (consEmb pre.length)) [] ↔
        inKbar (.node k pre) U []) := fun U _ V =>
    inKbar_snoc_old k pre c (oldPos_nil _)
  refine Prod.ext ?_ ?_
  · simp only [WA2, comp]
    rw [hsum, ← Finset.sum_add_distrib, Finset.sum_mul]
    refine Finset.sum_congr rfl (fun U hU => ?_)
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun V _ => ?_)
    rw [if_congr (hroot U hU V) rfl rfl, hw U hU V]
    by_cases h1 : inKbar (.node k pre) U [] <;> by_cases h2 : inKbar c V [] <;>
      simp [h1, h2]
  · simp only [WA2, comp]
    rw [hsum, Finset.sum_div, ← Finset.sum_add_distrib, Finset.sum_mul]
    refine Finset.sum_congr rfl (fun U hU => ?_)
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl (fun V _ => ?_)
    rw [if_congr (hroot U hU V) rfl rfl, hw U hU V]
    by_cases h1 : inKbar (.node k pre) U [] <;> by_cases h2 : inKbar c V [] <;>
      simp [h1, h2, div_eq_mul_inv, mul_assoc]

end Snoc

theorem WA2_leaf (y : ℝ) (k : Kind) : WA2 y (.node k []) = initV y k := by
  have hpos : positions (.node k []) = {[]} := by
    rw [positions_node, positionsAll_nil]
    rfl
  have hpsi : ∀ X, PsiA (.node k []) X = 0 := by
    intro X
    rw [PsiA_eq_sum, hpos, Finset.sum_singleton]
    simp
  cases k with
  | term =>
    have hs : steinerPos (.node .term []) = ∅ := by
      rw [steinerPos, hpos, Finset.filter_singleton, labelAt_nil]
      simp
    simp [WA2, hs, wtA, hpsi, labelAt_nil, initV]
  | steiner =>
    have hs : steinerPos (.node .steiner []) = {[]} := by
      rw [steinerPos, hpos, Finset.filter_singleton, labelAt_nil]
      simp
    have hP : (({[]} : Finset (List ℕ)).powerset) = insert ∅ {{[]}} := by decide
    rw [WA2, hs, hP, Finset.sum_pair (show (∅ : Finset (List ℕ)) ≠ {[]} by decide),
      Finset.sum_pair (show (∅ : Finset (List ℕ)) ≠ {[]} by decide)]
    simp [wtA, hpsi, inKbar, labelAt_nil, initV]

theorem psiFold_WA2 (y : ℝ) (k : Kind) :
    ∀ (rest pre : List (RTree Kind)), (∀ c ∈ rest, psi y c = WA2 y c) →
      psiFold y (WA2 y (.node k pre)) rest = WA2 y (.node k (pre ++ rest)) := by
  intro rest
  induction rest with
  | nil => intro pre _; simp only [psiFold, List.append_nil]
  | cons c rest ih =>
    intro pre h
    simp only [psiFold]
    rw [h c (List.mem_cons_self ..), ← WA2_snoc,
      ih (pre ++ [c]) (fun c' hc' => h c' (List.mem_cons_of_mem _ hc')), List.append_assoc,
      List.singleton_append]

theorem psi_eq_WA2 (y : ℝ) (t : RTree Kind) : psi y t = WA2 y t := by
  refine RTree.ind (fun t => psi y t = WA2 y t) ?_ t
  intro k cs ih
  simp only [psi]
  rw [← WA2_leaf, psiFold_WA2 y k cs [] ih, List.nil_append]

/-- lem:fa-dst-rec. -/
theorem dst_rec (y : ℝ) (t : RTree Kind) (hr : rootKind t = .term) :
    WA y t = (psi y t).1 := by
  rw [psi_eq_WA2]
  cases t with
  | node k cs =>
    have hk : k = .term := hr
    subst hk
    simp only [WA, WA2]
    refine Finset.sum_congr rfl (fun X _ => ?_)
    have hroot : inKbar (.node .term cs) X [] := Or.inl (labelAt_nil _ _)
    rw [ite_eq_left hroot, wtA]

/-- lem:fa-dst-cert as stated in the paper, for `W_A`. -/
theorem dst_tree_bound_WA (y e₁ e₂ : ℝ) (Z : Finset (ℝ × ℝ)) (hZ : Z.Nonempty)
    (h : CertHyp y e₁ e₂ Z) (t : RTree Kind)
    (hr : rootKind t = .term) (hl : NoSteinerLeaf t) :
    cZ Z hZ * e₁ ^ count .steiner t * e₂ ^ count .term t ≤ WA y t := by
  rw [dst_rec y t hr]
  exact dst_tree_bound y e₁ e₂ Z hZ h t hl

/-! #### Sanity checks against hand values (directly from the definitions) -/

example : positions (.node .term [.node .steiner [.node .term []]]) = {[], [0], [0, 0]} := by
  decide
example : labelAt (.node .term [.node .steiner [.node .term []]]) [] = some .term := rfl
example : labelAt (.node .term [.node .steiner [.node .term []]]) [0] = some .steiner := rfl
example : labelAt (.node .term [.node .steiner [.node .term []]]) [0, 0] = some .term := rfl
example : PsiA (.node .term [.node .steiner [.node .term []]]) ∅ = 1 := by decide
example : PsiA (.node .term [.node .steiner [.node .term []]]) {[0]} = 0 := by decide

example : positions (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
    = {[], [0], [0, 0], [0, 0, 0], [0, 1]} := by decide
example : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
    ∅ = 2 := by decide
example : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
    {[0]} = 1 := by decide
example : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
    {[0, 0]} = 2 := by decide
example : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
    {[0], [0, 0]} = 0 := by decide

example (y : ℝ) : WA y (.node .term [.node .steiner [.node .term []]]) = y + 1/2 := by
  have hs : steinerPos (.node .term [.node .steiner [.node .term []]]) = {[0]} := by decide
  have hP : (({[0]} : Finset (List ℕ)).powerset) = insert ∅ {{[0]}} := by decide
  have h0 : PsiA (.node .term [.node .steiner [.node .term []]]) ∅ = 1 := by decide
  have h1 : PsiA (.node .term [.node .steiner [.node .term []]]) {[0]} = 0 := by decide
  rw [WA, hs, hP, Finset.sum_pair (show (∅ : Finset (List ℕ)) ≠ {[0]} by decide), h0, h1]
  simp only [Finset.card_empty, Finset.card_singleton, pow_zero, pow_one]
  ring

example (y : ℝ) : WA y (.node .term [.node .steiner [.node .term [], .node .term []]]) = y + 1/4 := by
  have hs : steinerPos (.node .term [.node .steiner [.node .term [], .node .term []]]) = {[0]} := by
    decide
  have hP : (({[0]} : Finset (List ℕ)).powerset) = insert ∅ {{[0]}} := by decide
  have h0 : PsiA (.node .term [.node .steiner [.node .term [], .node .term []]]) ∅ = 2 := by decide
  have h1 : PsiA (.node .term [.node .steiner [.node .term [], .node .term []]]) {[0]} = 0 := by
    decide
  rw [WA, hs, hP, Finset.sum_pair (show (∅ : Finset (List ℕ)) ≠ {[0]} by decide), h0, h1]
  simp only [Finset.card_empty, Finset.card_singleton, pow_zero, pow_one]
  ring

example (y : ℝ) :
    WA y (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]]) =
      y ^ 2 + 3/4 * y + 1/4 := by
  have hs : steinerPos
      (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]]) =
      {[0], [0, 0]} := by decide
  have hP : (({[0], [0, 0]} : Finset (List ℕ)).powerset) =
      {∅, {[0]}, {[0, 0]}, {[0], [0, 0]}} := by decide
  rw [WA, hs, hP]
  rw [Finset.sum_insert (by decide), Finset.sum_insert (by decide), Finset.sum_pair (by decide)]
  have h0 : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
      ∅ = 2 := by decide
  have h1 : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
      {[0]} = 1 := by decide
  have h2 : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
      {[0, 0]} = 2 := by decide
  have h3 : PsiA (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])
      {[0], [0, 0]} = 0 := by decide
  have c3 : ({[0], [0, 0]} : Finset (List ℕ)).card = 2 := by decide
  rw [h0, h1, h2, h3, c3]
  simp only [Finset.card_empty, Finset.card_singleton, pow_zero, pow_one]
  ring

example (y : ℝ) :
    (psi y (.node .term [.node .steiner [.node .steiner [.node .term []], .node .term []]])).1 =
      y ^ 2 + 3/4 * y + 1/4 := by
  simp only [psi, psiFold, initV, comp]
  ring

end Recursion


/-! ### The rates

`prop:fa-dst-certs`: `α_j = (log(1+y_j) - log e_{1,j}, -log e_{2,j}, log(1+y_j))`, and
`max_i ∑_j λ_j α_{j,i} ∈ [0.4569669, 0.4569670)`, `< 0.457 < log₂ 1.3727`, with
`2^0.457 = 1.37268…`. -/

section Rates

open Enclose

/-- The rate vector of certificate `j`. -/
noncomputable def alpha (j : Fin 3) : Fin 3 → ℝ :=
  ![Real.logb 2 (1 + y j) - Real.logb 2 (e₁ j), -Real.logb 2 (e₂ j), Real.logb 2 (1 + y j)]

/-- Rational enclosure of `alpha j i` (logarithms by `log2Q`, precision 60/80). -/
def alphaI (j : Fin 3) : Fin 3 → QI := ![
  (log2Q (1 + y j) 60 80).sub (log2Q (e₁ j) 60 80),
  (log2Q (e₂ j) 60 80).neg,
  log2Q (1 + y j) 60 80]

/-- Rational enclosure of `∑_j λ_j α_{j,i}`. -/
def sumI (i : Fin 3) : QI :=
  ((alphaI 0 i).smul (lam 0)).add (((alphaI 1 i).smul (lam 1)).add ((alphaI 2 i).smul (lam 2)))

theorem alphaI_mem (j : Fin 3) (hy : 0 < 1 + y j) (he₁ : 0 < e₁ j) (he₂ : 0 < e₂ j)
    (i : Fin 3) : (alphaI j i).Contains (alpha j i) := by
  have hY : (log2Q (1 + y j) 60 80).Contains (Real.logb 2 (1 + (y j : ℝ))) := by
    have h := log2Q_sound hy 60 80
    push_cast at h
    exact h
  have hE1 : (log2Q (e₁ j) 60 80).Contains (Real.logb 2 (e₁ j : ℝ)) := log2Q_sound he₁ 60 80
  have hE2 : (log2Q (e₂ j) 60 80).Contains (Real.logb 2 (e₂ j : ℝ)) := log2Q_sound he₂ 60 80
  fin_cases i
  · exact QI.sub_sound hY hE1
  · exact QI.neg_sound hE2
  · exact hY

theorem sumI_mem (i : Fin 3) : (sumI i).Contains (∑ j, (lam j : ℝ) * alpha j i) := by
  have hpos : ∀ j : Fin 3, 0 < 1 + y j ∧ 0 < e₁ j ∧ 0 < e₂ j := by decide +kernel
  obtain ⟨a0, b0, c0⟩ := hpos 0
  obtain ⟨a1, b1, c1⟩ := hpos 1
  obtain ⟨a2, b2, c2⟩ := hpos 2
  rw [Fin.sum_univ_three, add_assoc]
  exact QI.add_sound (QI.smul_sound (lam 0) (alphaI_mem 0 a0 b0 c0 i))
    (QI.add_sound (QI.smul_sound (lam 1) (alphaI_mem 1 a1 b1 c1 i))
      (QI.smul_sound (lam 2) (alphaI_mem 2 a2 b2 c2 i)))

theorem dst_rates :
    (∀ i, ∑ j, (lam j : ℝ) * alpha j i < 4569670/10^7) ∧
    (∃ i, (4569669/10^7 : ℝ) ≤ ∑ j, (lam j : ℝ) * alpha j i) ∧
    (457/1000 : ℝ) < Real.logb 2 (13727/10000) ∧
    (137268/10^5 : ℝ) ≤ (2:ℝ) ^ (457/1000 : ℝ) ∧ (2:ℝ) ^ (457/1000 : ℝ) < 137269/10^5 := by
  have hU : ∀ i : Fin 3, (sumI i).hi < 4569670/10^7 := by decide +kernel
  have hL : (4569669/10^7 : ℚ) ≤ (sumI 0).lo := by decide +kernel
  have hq : (0:ℚ) < 13727/10000 := by norm_num
  have hlog : (457/1000 : ℚ) < (log2Q (13727/10000) 60 80).lo := by decide +kernel
  have hpow : (137268/10^5 : ℚ) ≤ (pow2Q (457/1000) 60 80).lo := by decide +kernel
  have hpow' : (pow2Q (457/1000) 60 80).hi < 137269/10^5 := by decide +kernel
  refine ⟨?_, ⟨0, ?_⟩, ?_, ?_, ?_⟩
  · intro i
    have h := sumI_mem i
    unfold QI.Contains at h
    have h2 := (Rat.cast_lt (K := ℝ)).mpr (hU i)
    push_cast at h2
    linarith [h.2]
  · have h := sumI_mem 0
    unfold QI.Contains at h
    have h2 := (Rat.cast_le (K := ℝ)).mpr hL
    push_cast at h2
    linarith [h.1]
  · have h := log2Q_sound hq 60 80
    unfold QI.Contains at h
    push_cast at h
    have h2 := (Rat.cast_lt (K := ℝ)).mpr hlog
    push_cast at h2
    linarith [h.1]
  · have h := pow2Q_sound (457/1000) 60 80
    unfold QI.Contains at h
    have hc : ((457/1000 : ℚ) : ℝ) = 457/1000 := by norm_num
    rw [hc] at h
    have h2 := (Rat.cast_le (K := ℝ)).mpr hpow
    push_cast at h2
    linarith [h.1]
  · have h := pow2Q_sound (457/1000) 60 80
    unfold QI.Contains at h
    have hc : ((457/1000 : ℚ) : ℝ) = 457/1000 := by norm_num
    rw [hc] at h
    have h2 := (Rat.cast_lt (K := ℝ)).mpr hpow'
    push_cast at h2
    linarith [h.2]

end Rates

end MaxLeafFormal.DSTCert