MaxLeafFormal.Antinorm3

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

Statements of the paper formalised here: Lemma 7.4, Lemma D.4.1, Lemma 7.5, Proposition 7.7.

import Mathlib
import MaxLeafFormal.Rooted
import MaxLeafFormal.RSThetaCert

/-!
# The antinorm certificates for RS-θ
-/

namespace MaxLeafFormal

open Finset

variable {V : Type*} [Fintype V] [DecidableEq V]

open Classical in
/-- The potential Π_{F,ν}(X) of `eq:rst-Phi`. -/
noncomputable def treePotential (T : SimpleGraph V) (ν : V → ℕ) (X : Finset V) : ℕ :=
  (∑ v ∈ univ \ X, ν v)
  + (univ.filter (fun v => v ∉ X ∧ ∀ u, T.Adj v u → u ∉ X)).card
  + Nat.card (T.induce (X : Set V)).ConnectedComponent

/-- W_{F,ν}(y). -/
noncomputable def treeW (T : SimpleGraph V) (ν : V → ℕ) (y : ℝ) : ℝ :=
  ∑ X ∈ (univ : Finset V).powerset, y ^ X.card * (1/2 : ℝ) ^ treePotential T ν X

namespace Antinorm3

open Pointwise

noncomputable section

/-! ### Messages, the cumulative cone and `𝒫_Z` -/

/-- The merge `P ∘ Q` of `eq:rst-merge`. -/
def merge (P Q : ℝ × ℝ × ℝ) : ℝ × ℝ × ℝ :=
  (P.1 * (2 * Q.1 + Q.2.1 + Q.2.2), P.2.1 * (Q.1 + Q.2.1 + Q.2.2 / 2) + P.2.2 * Q.1,
    P.2.2 * (Q.2.1 + Q.2.2 / 2))

def fin (P : ℝ × ℝ × ℝ) : ℝ := P.1 + P.2.1 + P.2.2 / 2

def init (y : ℝ) (j : ℕ) : ℝ × ℝ × ℝ := (y / 2, 0, (1/2 : ℝ) ^ j)

def Kcum : Set (ℝ × ℝ × ℝ) := {P | 0 ≤ P.1 ∧ 0 ≤ P.1 + P.2.1 ∧ 0 ≤ P.1 + P.2.1 + P.2.2}

def PZ (Z : Finset (ℝ × ℝ × ℝ)) : Set (ℝ × ℝ × ℝ) := convexHull ℝ (Z : Set _) + Kcum

noncomputable def cZ (Z : Finset (ℝ × ℝ × ℝ)) (hZ : Z.Nonempty) : ℝ := Z.inf' hZ fin

theorem merge_add_left (P P' Q : ℝ × ℝ × ℝ) : merge (P + P') Q = merge P Q + merge P' Q := by
  simp only [merge, Prod.fst_add, Prod.snd_add, Prod.mk_add_mk]; ext <;> simp <;> ring

theorem merge_add_right (P Q Q' : ℝ × ℝ × ℝ) : merge P (Q + Q') = merge P Q + merge P Q' := by
  simp only [merge, Prod.fst_add, Prod.snd_add, Prod.mk_add_mk]; ext <;> simp <;> ring

theorem merge_smul_left (a : ℝ) (P Q : ℝ × ℝ × ℝ) : merge (a • P) Q = a • merge P Q := by
  simp only [merge, Prod.smul_fst, Prod.smul_snd, Prod.smul_mk, smul_eq_mul]; ext <;> simp <;> ring

theorem merge_smul_right (a : ℝ) (P Q : ℝ × ℝ × ℝ) : merge P (a • Q) = a • merge P Q := by
  simp only [merge, Prod.smul_fst, Prod.smul_snd, Prod.smul_mk, smul_eq_mul]; ext <;> simp <;> ring

theorem merge_zero_left (Q : ℝ × ℝ × ℝ) : merge 0 Q = 0 := by
  simpa using merge_smul_left 0 0 Q

theorem merge_zero_right (P : ℝ × ℝ × ℝ) : merge P 0 = 0 := by
  simpa using merge_smul_right 0 P 0

theorem merge_sum_left {ι : Type*} (s : Finset ι) (f : ι → ℝ × ℝ × ℝ) (Q : ℝ × ℝ × ℝ) :
    merge (∑ i ∈ s, f i) Q = ∑ i ∈ s, merge (f i) Q := by
  classical
  induction s using Finset.induction_on with
  | empty => simp [merge_zero_left]
  | insert a s ha ih => rw [sum_insert ha, sum_insert ha, merge_add_left, ih]

theorem merge_sum_right {ι : Type*} (s : Finset ι) (P : ℝ × ℝ × ℝ) (f : ι → ℝ × ℝ × ℝ) :
    merge P (∑ i ∈ s, f i) = ∑ i ∈ s, merge P (f i) := by
  classical
  induction s using Finset.induction_on with
  | empty => simp [merge_zero_right]
  | insert a s ha ih => rw [sum_insert ha, sum_insert ha, merge_add_right, ih]

theorem fin_add (P Q : ℝ × ℝ × ℝ) : fin (P + Q) = fin P + fin Q := by
  simp only [fin, Prod.fst_add, Prod.snd_add]; ring

theorem fin_smul (a : ℝ) (P : ℝ × ℝ × ℝ) : fin (a • P) = a * fin P := by
  simp only [fin, Prod.smul_fst, Prod.smul_snd, smul_eq_mul]; ring

theorem nonneg_iff (P : ℝ × ℝ × ℝ) : 0 ≤ P ↔ 0 ≤ P.1 ∧ 0 ≤ P.2.1 ∧ 0 ≤ P.2.2 := by
  rw [Prod.le_def, Prod.le_def]; rfl

theorem merge_nonneg {P Q : ℝ × ℝ × ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q) : 0 ≤ merge P Q := by
  rw [nonneg_iff] at *
  obtain ⟨a, b, c⟩ := hP; obtain ⟨d, e, f⟩ := hQ
  simp only [merge]
  refine ⟨by positivity, by positivity, by positivity⟩

/-! ### `lem:rst-closure` -/

theorem Kcum_add {P Q : ℝ × ℝ × ℝ} (hP : P ∈ Kcum) (hQ : Q ∈ Kcum) : P + Q ∈ Kcum := by
  obtain ⟨a, b, c⟩ := hP; obtain ⟨d, e, f⟩ := hQ
  simp only [Kcum, Set.mem_ofPred_eq, Prod.fst_add, Prod.snd_add]
  exact ⟨by linarith, by linarith, by linarith⟩

theorem Kcum_smul {a : ℝ} (ha : 0 ≤ a) {P : ℝ × ℝ × ℝ} (hP : P ∈ Kcum) : a • P ∈ Kcum := by
  obtain ⟨b, c, d⟩ := hP
  simp only [Kcum, Set.mem_ofPred_eq, Prod.smul_fst, Prod.smul_snd, smul_eq_mul]
  refine ⟨by positivity, by nlinarith, by nlinarith⟩

theorem Kcum_of_nonneg {P : ℝ × ℝ × ℝ} (hP : 0 ≤ P) : P ∈ Kcum := by
  rw [nonneg_iff] at hP
  obtain ⟨a, b, c⟩ := hP
  exact ⟨a, by linarith, by linarith⟩

theorem zero_mem_Kcum : (0 : ℝ × ℝ × ℝ) ∈ Kcum := Kcum_of_nonneg le_rfl

/-- `lem:rst-closure` (a), first half. -/
theorem merge_Kcum_left {Δ Q : ℝ × ℝ × ℝ} (hΔ : Δ ∈ Kcum) (hQ : 0 ≤ Q) : merge Δ Q ∈ Kcum := by
  obtain ⟨a, b, c⟩ := hΔ
  rw [nonneg_iff] at hQ
  obtain ⟨d, e, f⟩ := hQ
  simp only [Kcum, merge, Set.mem_ofPred_eq]
  refine ⟨by positivity, ?_, ?_⟩
  · nlinarith [mul_nonneg b d, mul_nonneg a d, mul_nonneg a f,
      mul_nonneg c (add_nonneg e (div_nonneg f (by norm_num : (0:ℝ) ≤ 2))) ]
  · nlinarith [mul_nonneg c d, mul_nonneg a d, mul_nonneg a f,
      mul_nonneg c (add_nonneg e (div_nonneg f (by norm_num : (0:ℝ) ≤ 2))) ]

/-- `lem:rst-closure` (a), second half. -/
theorem merge_Kcum_right {Q Δ : ℝ × ℝ × ℝ} (hQ : 0 ≤ Q) (hΔ : Δ ∈ Kcum) : merge Q Δ ∈ Kcum := by
  obtain ⟨a, b, c⟩ := hΔ
  rw [nonneg_iff] at hQ
  obtain ⟨d, e, f⟩ := hQ
  simp only [Kcum, merge, Set.mem_ofPred_eq]
  refine ⟨by nlinarith, by nlinarith, by nlinarith⟩

/-- `lem:rst-closure` (b). -/
theorem fin_nonneg_of_Kcum {Δ : ℝ × ℝ × ℝ} (hΔ : Δ ∈ Kcum) : 0 ≤ fin Δ := by
  obtain ⟨a, b, c⟩ := hΔ
  simp only [fin]; linarith

theorem convexHull_nonneg {Z : Finset (ℝ × ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) {z : ℝ × ℝ × ℝ}
    (hz : z ∈ convexHull ℝ (Z : Set _)) : 0 ≤ z := by
  have : convexHull ℝ (Z : Set (ℝ × ℝ × ℝ)) ⊆ Set.Ici 0 :=
    convexHull_min (fun z hz => hZ0 z hz) (convex_Ici 0)
  exact this hz

/-- `lem:rst-abstract` (a) for the cone `K_cum`, first half (used with `lem:rst-closure`). -/
theorem PZ_add_Kcum {Z : Finset (ℝ × ℝ × ℝ)} {P Δ : ℝ × ℝ × ℝ} (hP : P ∈ PZ Z) (hΔ : Δ ∈ Kcum) :
    P + Δ ∈ PZ Z := by
  obtain ⟨z, hz, Δ', hΔ', rfl⟩ := hP
  exact ⟨z, hz, Δ' + Δ, Kcum_add hΔ' hΔ, by rw [add_assoc]⟩

theorem smul_PZ_add_Kcum {Z : Finset (ℝ × ℝ × ℝ)} {η : ℝ} (hη : 0 < η) {P Δ : ℝ × ℝ × ℝ}
    (hP : P ∈ η • PZ Z) (hΔ : Δ ∈ Kcum) : P + Δ ∈ η • PZ Z := by
  obtain ⟨P', hP', rfl⟩ := hP
  refine ⟨P' + η⁻¹ • Δ, PZ_add_Kcum hP' (Kcum_smul (inv_nonneg.2 hη.le) hΔ), ?_⟩
  simp only [smul_add, smul_smul, mul_inv_cancel₀ hη.ne', one_smul]

/-- `lem:rst-abstract` (a) for the cone `K_cum`, second half (used with `lem:rst-closure`). -/
theorem smul_PZ_mono {Z : Finset (ℝ × ℝ × ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) {η η' : ℝ} (hη' : 0 < η')
    (hle : η' ≤ η) {P : ℝ × ℝ × ℝ} (hP : P ∈ η • PZ Z) : P ∈ η' • PZ Z := by
  obtain ⟨_, ⟨z, hz, Δ, hΔ, rfl⟩, rfl⟩ := hP
  refine ⟨z + (((η - η') / η') • z + (η / η') • Δ), ⟨z, hz, _, Kcum_add
    (Kcum_of_nonneg (smul_nonneg (div_nonneg (by linarith) hη'.le) (convexHull_nonneg hZ0 hz)))
    (Kcum_smul (div_nonneg (by linarith) hη'.le) hΔ), rfl⟩, ?_⟩
  simp only [smul_add, smul_smul]
  rw [mul_div_cancel₀ _ hη'.ne', mul_div_cancel₀ _ hη'.ne', sub_smul]
  abel

theorem convex_PZ (Z : Finset (ℝ × ℝ × ℝ)) : Convex ℝ (PZ Z) :=
  (convex_convexHull ℝ _).add (by
    intro P hP Q hQ a b ha hb _
    exact Kcum_add (Kcum_smul ha hP) (Kcum_smul hb hQ))

/-! ### Rooted trees: descendants and tops -/

section Rooted

open CDS SimpleGraph

variable {F : SimpleGraph V} (hF : F.IsTree) (r : V)

theorem par_root : par hF r r = r := by
  unfold par; rw [dif_pos rfl]

theorem dist_par (x : V) : F.dist r (par hF r x) = F.dist r x - 1 := by
  by_cases hx : x = r
  · subst hx; rw [par_root]; simp
  · have := (par_spec hF r hx).2; omega

theorem dist_iter (k : ℕ) (u : V) : F.dist r ((par hF r)^[k] u) = F.dist r u - k := by
  induction k with
  | zero => simp
  | succ k ih => rw [Function.iterate_succ_apply', dist_par, ih]; omega

include hF in

theorem eq_root_of_dist {x : V} (h : F.dist r x = 0) : x = r :=
  ((hF.connected.preconnected r x).dist_eq_zero_iff.1 h).symm

include hF in

theorem dist_pos_of_ne {x : V} (h : x ≠ r) : 0 < F.dist r x :=
  Nat.pos_of_ne_zero (fun h' => h (eq_root_of_dist hF r h'))

/-- `u` is a descendant of `c` (inclusive). -/
def desc (c u : V) : Prop := ∃ k, (par hF r)^[k] u = c

open Classical in
/-- The vertex set of the subtree `F_c`. -/
noncomputable def D (c : V) : Finset V := univ.filter (desc hF r c)

theorem mem_D {c u : V} : u ∈ D hF r c ↔ desc hF r c u := by
  simp [D]

/-- The children of `v`. -/
noncomputable def children (v : V) : Finset V := univ.filter (fun w => w ≠ r ∧ par hF r w = v)

theorem mem_children {v w : V} : w ∈ children hF r v ↔ w ≠ r ∧ par hF r w = v := by
  simp [children]

theorem desc_dist {c u : V} (h : desc hF r c u) : F.dist r c ≤ F.dist r u := by
  obtain ⟨k, rfl⟩ := h; rw [dist_iter]; omega

theorem desc_eq_of_dist {c c' u : V} (h : desc hF r c u) (h' : desc hF r c' u) (hc : c ≠ r)
    (hd : F.dist r c = F.dist r c') : c = c' := by
  obtain ⟨k, hk⟩ := h; obtain ⟨k', hk'⟩ := h'
  have h1 := dist_iter hF r k u; have h2 := dist_iter hF r k' u
  rw [hk] at h1; rw [hk'] at h2
  have := dist_pos_of_ne hF r hc
  rw [show k = k' by omega] at hk
  exact hk.symm.trans hk'

theorem iter_root (k : ℕ) : (par hF r)^[k] r = r :=
  Function.iterate_fixed (par_root hF r) k

theorem self_mem_D (v : V) : v ∈ D hF r v := (mem_D hF r).2 ⟨0, rfl⟩

theorem dist_child {v w : V} (hw : w ∈ children hF r v) : F.dist r w = F.dist r v + 1 := by
  obtain ⟨hwr, rfl⟩ := (mem_children hF r).1 hw
  have := (par_spec hF r hwr).2; omega

theorem mem_D_iff {v u : V} : u ∈ D hF r v ↔ u = v ∨ ∃ w ∈ children hF r v, u ∈ D hF r w := by
  constructor
  · intro h
    have hex : ∃ k, (par hF r)^[k] u = v := (mem_D hF r).1 h
    classical
    rcases hk : Nat.find hex with _ | m
    · left; have := Nat.find_spec hex; rw [hk] at this; exact this
    · right
      have hspec := Nat.find_spec hex
      rw [hk, Function.iterate_succ_apply'] at hspec
      have hne : (par hF r)^[m] u ≠ v := Nat.find_min hex (by omega)
      have hner : (par hF r)^[m] u ≠ r := by
        intro h'; rw [h', par_root] at hspec; exact hne (h'.trans hspec)
      exact ⟨_, (mem_children hF r).2 ⟨hner, hspec⟩, (mem_D hF r).2 ⟨m, rfl⟩⟩
  · rintro (rfl | ⟨w, hw, hu⟩)
    · exact self_mem_D hF r u
    · obtain ⟨k, hk⟩ := (mem_D hF r).1 hu
      obtain ⟨-, hpw⟩ := (mem_children hF r).1 hw
      exact (mem_D hF r).2 ⟨k + 1, by rw [Function.iterate_succ_apply', hk, hpw]⟩

theorem D_eq (v : V) : D hF r v = insert v ((children hF r v).biUnion (D hF r)) := by
  ext u; rw [mem_D_iff, mem_insert, mem_biUnion]

theorem D_sub_of_child {v w : V} (hw : w ∈ children hF r v) : D hF r w ⊆ D hF r v :=
  fun u hu => (mem_D_iff hF r).2 (Or.inr ⟨w, hw, hu⟩)

theorem not_mem_D_child {v w : V} (hw : w ∈ children hF r v) : v ∉ D hF r w := by
  intro h
  have := desc_dist hF r ((mem_D hF r).1 h)
  have := dist_child hF r hw
  omega

theorem card_D_child_lt {v w : V} (hw : w ∈ children hF r v) :
    (D hF r w).card < (D hF r v).card :=
  card_lt_card ((ssubset_iff_of_subset (D_sub_of_child hF r hw)).2
    ⟨v, self_mem_D hF r v, not_mem_D_child hF r hw⟩)

theorem D_disjoint {v w w' : V} (hw : w ∈ children hF r v) (hw' : w' ∈ children hF r v)
    (hne : w ≠ w') : Disjoint (D hF r w) (D hF r w') := by
  rw [Finset.disjoint_left]
  intro u hu hu'
  exact hne (desc_eq_of_dist hF r ((mem_D hF r).1 hu) ((mem_D hF r).1 hu')
    ((mem_children hF r).1 hw).1 (by rw [dist_child hF r hw, dist_child hF r hw']))

theorem D_par_mem {w u : V} (hwr : w ≠ r) (hu : u ∈ D hF r w) (huw : u ≠ w) :
    u ≠ r ∧ par hF r u ∈ D hF r w := by
  obtain ⟨k, hk⟩ := (mem_D hF r).1 hu
  have hur : u ≠ r := by rintro rfl; rw [iter_root] at hk; exact hwr hk.symm
  refine ⟨hur, ?_⟩
  rcases k with _ | m
  · exact absurd hk huw
  · exact (mem_D hF r).2 ⟨m, by rw [← Function.iterate_succ_apply]; exact hk⟩

theorem D_edge {w a b : V} (hwr : w ≠ r) (hb : b ∈ D hF r w) (ha : a ∉ D hF r w)
    (hab : F.Adj a b) : b = w ∧ a = par hF r w := by
  rcases (adj_iff_par hF r).1 hab with ⟨har, hpa⟩ | ⟨hbr, hpb⟩
  · exfalso; apply ha
    obtain ⟨k, hk⟩ := (mem_D hF r).1 hb
    exact (mem_D hF r).2 ⟨k + 1, by rw [Function.iterate_succ_apply, hpa, hk]⟩
  · by_cases hbw : b = w
    · exact ⟨hbw, by rw [← hpb, hbw]⟩
    · exfalso; apply ha
      rw [← hpb]; exact (D_par_mem hF r hwr hb hbw).2

theorem D_root : D hF r r = univ := by
  ext u
  simp only [mem_univ, iff_true]
  refine (mem_D hF r).2 ⟨F.dist r u, eq_root_of_dist hF r ?_⟩
  rw [dist_iter]; omega

/-- The tops of `X`: its vertices whose parent is not in `X`, and the root. -/
def tops (X : Finset V) : Finset V := X.filter (fun t => ¬ (t ≠ r ∧ par hF r t ∈ X))

/-- The top of the component of `x` in `F[X]`, found by following parents. -/
noncomputable def topOf (X : Finset V) (x : V) : V :=
  if h : x ≠ r ∧ par hF r x ∈ X then topOf X (par hF r x) else x
termination_by F.dist r x
decreasing_by have := (par_spec hF r h.1).2; omega

theorem topOf_par {X : Finset V} {x : V} (h : x ≠ r ∧ par hF r x ∈ X) :
    topOf hF r X x = topOf hF r X (par hF r x) := by
  rw [topOf]; exact dite_cond_eq_true (eq_true h)

theorem topOf_top {X : Finset V} {x : V} (h : ¬ (x ≠ r ∧ par hF r x ∈ X)) :
    topOf hF r X x = x := by
  rw [topOf]; exact dite_cond_eq_false (eq_false h)

theorem topOf_adj {X : Finset V} {x x' : V} (hx : x ∈ X) (hx' : x' ∈ X) (h : F.Adj x x') :
    topOf hF r X x = topOf hF r X x' := by
  rcases (adj_iff_par hF r).1 h with ⟨hxr, hp⟩ | ⟨hxr, hp⟩
  · rw [topOf_par hF r ⟨hxr, hp ▸ hx'⟩, hp]
  · rw [topOf_par hF r ⟨hxr, hp ▸ hx⟩, hp]

theorem topOf_reach {X : Finset V} {x x' : (X : Set V)}
    (h : (F.induce (X : Set V)).Reachable x x') : topOf hF r X x.1 = topOf hF r X x'.1 := by
  obtain ⟨p⟩ := h
  induction p with
  | nil => rfl
  | cons hadj _ ih =>
    rw [← ih]
    exact topOf_adj hF r (Subtype.prop _) (Subtype.prop _) (by simpa using hadj)

/-- In a tree, the components of `F[X]` correspond to the tops of `X`. -/
theorem comp_eq_tops (X : Finset V) : comp F X = (tops hF r X).card := by
  apply le_antisymm (comp_le_tops hF r X)
  show (tops hF r X).card ≤ _
  unfold comp
  rw [← Fintype.card_coe (tops hF r X), ← Nat.card_eq_fintype_card]
  apply Nat.card_le_card_of_injective
    (fun t : (tops hF r X : Set V) => (F.induce (X : Set V)).connectedComponentMk
      ⟨t.1, (mem_filter.1 t.2).1⟩)
  intro t t' h
  have := topOf_reach hF r (ConnectedComponent.exact h)
  simp only at this
  rw [topOf_top hF r (mem_filter.1 t.2).2, topOf_top hF r (mem_filter.1 t'.2).2] at this
  exact Subtype.ext this

end Rooted

/-! ### `lem:rst-treerec`: the three-state recursion -/

section Recursion

open CDS SimpleGraph

/-- The vertices `u ∈ S`, `u ≠ v`, with `N_F[u] ∩ X = ∅`. -/
def dom (F : SimpleGraph V) [DecidableRel F.Adj] (S : Finset V) (v : V) (X : Finset V) :
    Finset V :=
  (S.erase v).filter (fun u => u ∉ X ∧ ∀ x, F.Adj u x → x ∉ X)

/-- The state of `v` for `X`, as a unit vector: `v ∈ X`; `v ∉ X` with a neighbour in `X`;
`v ∉ X` with no neighbour in `X`. -/
def sv (F : SimpleGraph V) [DecidableRel F.Adj] (v : V) (X : Finset V) : ℝ × ℝ × ℝ :=
  if v ∈ X then (1, 0, 0) else if ∀ u, F.Adj v u → u ∉ X then (0, 0, 1) else (0, 1, 0)

variable {F : SimpleGraph V} [DecidableRel F.Adj] (hF : F.IsTree) (r : V) (ν : V → ℕ) (y : ℝ)

/-- The inner potential `Π^in` of a partial subtree `S` with top `v`. -/
def Pin (S : Finset V) (v : V) (X : Finset V) : ℕ :=
  (∑ u ∈ S \ X, ν u) + (dom F S v X).card + (tops hF r X).card

/-- The message (triple) of a partial subtree `S` with top `v`. -/
def triple (S : Finset V) (v : V) : ℝ × ℝ × ℝ :=
  ∑ X ∈ S.powerset, (y ^ X.card * (1/2 : ℝ) ^ Pin hF r ν S v X) • sv F v X

theorem sv_nonneg (v : V) (X : Finset V) : 0 ≤ sv F v X := by
  unfold sv; split_ifs <;> simp [nonneg_iff]

theorem triple_nonneg (hy : 0 ≤ y) (S : Finset V) (v : V) : 0 ≤ triple hF r ν y S v :=
  sum_nonneg fun X _ => smul_nonneg (by positivity) (sv_nonneg v X)

theorem tops_singleton (v : V) : tops hF r {v} = {v} := by
  ext u
  simp only [tops, mem_filter, mem_singleton]
  constructor
  · exact fun h => h.1
  · rintro rfl
    refine ⟨rfl, fun ⟨hv, hp⟩ => ?_⟩
    exact F.loopless.irrefl _ (hp ▸ (par_spec hF r hv).1)

/-- Base case of `lem:rst-treerec`: one vertex. -/
theorem triple_single (v : V) : triple hF r ν y {v} v = init y (ν v) := by
  unfold triple
  have hP : ({v} : Finset V).powerset = {∅, {v}} := by
    ext X; simp [subset_singleton_iff]
  rw [hP, sum_pair (by simp)]
  have h0 : Pin hF r ν {v} v ∅ = ν v := by simp [Pin, dom, tops]
  have h1 : Pin hF r ν {v} v {v} = 1 := by simp [Pin, dom, tops_singleton]
  rw [h0, h1]
  simp only [sv, card_empty, card_singleton, pow_zero, one_mul, pow_one, mem_singleton,
    if_true, notMem_empty, not_false_eq_true, implies_true, if_false]
  ext <;> simp [init] <;> ring

theorem sum_powerset_union {M : Type*} [AddCommMonoid M] {A B : Finset V} (hAB : Disjoint A B)
    (f : Finset V → M) :
    ∑ X ∈ (A ∪ B).powerset, f X = ∑ Y ∈ A.powerset, ∑ Z ∈ B.powerset, f (Y ∪ Z) := by
  rw [← sum_product']
  refine sum_nbij' (fun X => (X ∩ A, X ∩ B)) (fun p => p.1 ∪ p.2) ?_ ?_ ?_ ?_ ?_
  · intro X _; simp [mem_product, mem_powerset, inter_subset_right]
  · intro p hp
    simp only [mem_product, mem_powerset, coe_product, Set.mem_prod, mem_coe] at hp ⊢
    exact union_subset_union hp.1 hp.2
  · intro X hX
    simp only [mem_coe, mem_powerset] at hX
    simp only [← inter_union_distrib_left, inter_eq_left.2 hX]
  · intro p hp
    simp only [mem_coe, mem_product, mem_powerset] at hp
    have h1 : p.2 ∩ A = ∅ := disjoint_iff_inter_eq_empty.1
      (disjoint_of_subset_left hp.2 hAB.symm)
    have h2 : p.1 ∩ B = ∅ := disjoint_iff_inter_eq_empty.1 (disjoint_of_subset_left hp.1 hAB)
    ext1
    · simp [union_inter_distrib_right, h1, inter_eq_left.2 hp.1]
    · simp [union_inter_distrib_right, h2, inter_eq_left.2 hp.2]
  · intro X hX
    simp only [mem_powerset] at hX
    simp only [← inter_union_distrib_left, inter_eq_left.2 hX]

section Split

variable {A B : Finset V} {v w : V} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
  (hwr : w ≠ r) (hpw : par hF r w = v)
  (hedge : ∀ a ∈ A, ∀ b ∈ B, F.Adj a b → a = v ∧ b = w)
  (hB : ∀ u ∈ B, u ≠ w → u ≠ r ∧ par hF r u ∈ B)
  (hA : ∀ u ∈ A, u ≠ r → par hF r u ∉ B)
  {Y Z : Finset V} (hY : Y ⊆ A) (hZ : Z ⊆ B)

include hAB hY hZ in

theorem nu_split :
    ∑ u ∈ (A ∪ B) \ (Y ∪ Z), ν u = (∑ u ∈ A \ Y, ν u) + ∑ u ∈ B \ Z, ν u := by
  rw [← sum_union (disjoint_of_subset_left sdiff_subset (disjoint_of_subset_right sdiff_subset hAB))]
  congr 1
  ext u
  simp only [mem_sdiff, mem_union, not_or]
  constructor
  · rintro ⟨hu | hu, h1, h2⟩
    · exact Or.inl ⟨hu, h1⟩
    · exact Or.inr ⟨hu, h2⟩
  · rintro (⟨hu, h1⟩ | ⟨hu, h2⟩)
    · exact ⟨Or.inl hu, h1, fun h => disjoint_left.1 hAB hu (hZ h)⟩
    · exact ⟨Or.inr hu, fun h => disjoint_left.1 hAB (hY h) hu, h2⟩

include hAB hv hw hwr hpw hedge hY hZ in

theorem dom_split :
    (dom F (A ∪ B) v (Y ∪ Z)).card + 0 = (dom F A v Y).card + (dom F B w Z).card
      + (if (w ∉ Z ∧ ∀ x, F.Adj w x → x ∉ Z) ∧ v ∉ Y then 1 else 0) := by
  have hvB : v ∉ B := fun h => disjoint_left.1 hAB hv h
  have hadj : F.Adj w v := by rw [← hpw]; exact (par_spec hF r hwr).1
  simp only [dom, card_filter, add_zero]
  rw [erase_union_distrib, erase_eq_of_notMem hvB, sum_union (disjoint_of_subset_left
    (erase_subset _ _) hAB), ← add_sum_erase B _ hw]
  have h1 : (∑ u ∈ A.erase v, if u ∉ Y ∪ Z ∧ ∀ x, F.Adj u x → x ∉ Y ∪ Z then 1 else 0)
      = ∑ u ∈ A.erase v, if u ∉ Y ∧ ∀ x, F.Adj u x → x ∉ Y then 1 else 0 := by
    apply sum_congr rfl
    intro u hu
    have huA : u ∈ A := mem_of_mem_erase hu
    have huv : u ≠ v := ne_of_mem_erase hu
    have huZ : u ∉ Z := fun h => disjoint_left.1 hAB huA (hZ h)
    congr 1
    apply propext
    simp only [mem_union, not_or]
    constructor
    · exact fun ⟨⟨h1, _⟩, h2⟩ => ⟨h1, fun x hx => (h2 x hx).1⟩
    · refine fun ⟨h1, h2⟩ => ⟨⟨h1, huZ⟩, fun x hx => ⟨h2 x hx, fun hxZ => huv ?_⟩⟩
      exact (hedge u huA x (hZ hxZ) hx).1
  have h2 : (∑ u ∈ B.erase w, if u ∉ Y ∪ Z ∧ ∀ x, F.Adj u x → x ∉ Y ∪ Z then 1 else 0)
      = ∑ u ∈ B.erase w, if u ∉ Z ∧ ∀ x, F.Adj u x → x ∉ Z then 1 else 0 := by
    apply sum_congr rfl
    intro u hu
    have huB : u ∈ B := mem_of_mem_erase hu
    have huw : u ≠ w := ne_of_mem_erase hu
    have huY : u ∉ Y := fun h => disjoint_left.1 hAB (hY h) huB
    congr 1
    apply propext
    simp only [mem_union, not_or]
    constructor
    · exact fun ⟨⟨_, h1⟩, h2⟩ => ⟨h1, fun x hx => (h2 x hx).2⟩
    · refine fun ⟨h1, h2⟩ => ⟨⟨huY, h1⟩, fun x hx => ⟨fun hxY => huw ?_, h2 x hx⟩⟩
      exact (hedge x (hY hxY) u huB hx.symm).2
  have h3 : (if w ∉ Y ∪ Z ∧ ∀ x, F.Adj w x → x ∉ Y ∪ Z then 1 else 0)
      = if (w ∉ Z ∧ ∀ x, F.Adj w x → x ∉ Z) ∧ v ∉ Y then 1 else 0 := by
    have hwY : w ∉ Y := fun h => disjoint_left.1 hAB (hY h) hw
    congr 1
    apply propext
    simp only [mem_union, not_or]
    constructor
    · exact fun ⟨⟨_, h1⟩, h2⟩ => ⟨⟨h1, fun x hx => (h2 x hx).2⟩, (h2 v hadj).1⟩
    · refine fun ⟨⟨h1, h2⟩, h3⟩ => ⟨⟨hwY, h1⟩, fun x hx => ⟨fun hxY => ?_, h2 x hx⟩⟩
      obtain ⟨rfl, -⟩ := hedge x (hY hxY) w hw hx.symm
      exact h3 hxY
  rw [h1, h2, h3]
  ring

include hAB hv hw hwr hpw hB hA hY hZ in

theorem tops_split :
    (tops hF r (Y ∪ Z)).card + (if v ∈ Y ∧ w ∈ Z then 1 else 0)
      = (tops hF r Y).card + (tops hF r Z).card := by
  have hYZ : Disjoint Y Z := disjoint_of_subset_left hY (disjoint_of_subset_right hZ hAB)
  have hvB : v ∉ B := fun h => disjoint_left.1 hAB hv h
  simp only [tops, card_filter]
  rw [sum_union hYZ]
  have h1 : (∑ u ∈ Y, if ¬ (u ≠ r ∧ par hF r u ∈ Y ∪ Z) then 1 else 0)
      = ∑ u ∈ Y, if ¬ (u ≠ r ∧ par hF r u ∈ Y) then 1 else 0 := by
    apply sum_congr rfl
    intro u hu
    congr 1
    apply propext
    simp only [mem_union]
    constructor
    · exact fun h h' => h ⟨h'.1, Or.inl h'.2⟩
    · rintro h ⟨hur, hp | hp⟩
      · exact h ⟨hur, hp⟩
      · exact hA u (hY hu) hur (hZ hp)
  have h2 : (∑ u ∈ Z, if ¬ (u ≠ r ∧ par hF r u ∈ Y ∪ Z) then 1 else 0)
      + (if v ∈ Y ∧ w ∈ Z then 1 else 0)
      = ∑ u ∈ Z, if ¬ (u ≠ r ∧ par hF r u ∈ Z) then 1 else 0 := by
    have key : ∀ u ∈ Z, u ≠ w → ((¬ (u ≠ r ∧ par hF r u ∈ Y ∪ Z)) ↔ ¬ (u ≠ r ∧ par hF r u ∈ Z)) := by
      intro u hu huw
      obtain ⟨hur, hpB⟩ := hB u (hZ hu) huw
      have : par hF r u ∉ Y := fun h => disjoint_left.1 hAB (hY h) hpB
      simp [mem_union, this]
    by_cases hwZ : w ∈ Z
    · rw [← add_sum_erase Z _ hwZ, ← add_sum_erase Z _ hwZ,
        sum_congr rfl (fun u hu => by rw [if_congr (key u (mem_of_mem_erase hu)
          (ne_of_mem_erase hu)) rfl rfl])]
      have hvZ : v ∉ Z := fun h => hvB (hZ h)
      by_cases hvY : v ∈ Y <;> simp [hpw, hwr, hvY, hvZ, hwZ] <;> ring
    · simp only [hwZ, and_false, if_false, add_zero]
      exact sum_congr rfl (fun u hu => by
        rw [if_congr (key u hu (fun h => hwZ (h ▸ hu))) rfl rfl])
  omega

include hAB hv hw hwr hpw hedge hZ in

theorem sv_split :
    sv F v (Y ∪ Z) = if v ∈ Y then (1, 0, 0)
      else if (∀ u, F.Adj v u → u ∉ Y) ∧ w ∉ Z then (0, 0, 1) else (0, 1, 0) := by
  have hvZ : v ∉ Z := fun h => disjoint_left.1 hAB hv (hZ h)
  have hadj : F.Adj v w := by rw [← hpw]; exact (par_spec hF r hwr).1.symm
  have e1 : v ∈ Y ∪ Z ↔ v ∈ Y := by simp [hvZ]
  have e2 : (∀ u, F.Adj v u → u ∉ Y ∪ Z) ↔ (∀ u, F.Adj v u → u ∉ Y) ∧ w ∉ Z := by
    simp only [mem_union, not_or]
    constructor
    · exact fun h => ⟨fun u hu => (h u hu).1, (h w hadj).2⟩
    · refine fun ⟨h, hwZ⟩ u hu => ⟨h u hu, fun huZ => hwZ ?_⟩
      obtain ⟨-, rfl⟩ := hedge v hv u (hZ huZ) hu
      exact huZ
  unfold sv
  simp only [e1, e2]

include hAB hv hw hwr hpw hedge hB hA hY hZ in

theorem term_split :
    (y ^ (Y ∪ Z).card * (1/2 : ℝ) ^ Pin hF r ν (A ∪ B) v (Y ∪ Z)) • sv F v (Y ∪ Z)
      = merge ((y ^ Y.card * (1/2 : ℝ) ^ Pin hF r ν A v Y) • sv F v Y)
          ((y ^ Z.card * (1/2 : ℝ) ^ Pin hF r ν B w Z) • sv F w Z) := by
  have hYZ : Disjoint Y Z := disjoint_of_subset_left hY (disjoint_of_subset_right hZ hAB)
  have hPin : Pin hF r ν (A ∪ B) v (Y ∪ Z) + (if v ∈ Y ∧ w ∈ Z then 1 else 0)
      = Pin hF r ν A v Y + Pin hF r ν B w Z
        + (if (w ∉ Z ∧ ∀ x, F.Adj w x → x ∉ Z) ∧ v ∉ Y then 1 else 0) := by
    unfold Pin
    rw [nu_split ν hAB hY hZ]
    have := dom_split hF r hAB hv hw hwr hpw hedge hY hZ
    have := tops_split hF r hAB hv hw hwr hpw hB hA hY hZ
    omega
  have hc : (1/2 : ℝ) ^ Pin hF r ν (A ∪ B) v (Y ∪ Z) * (1/2) ^ (if v ∈ Y ∧ w ∈ Z then 1 else 0)
      = (1/2) ^ Pin hF r ν A v Y * (1/2) ^ Pin hF r ν B w Z
        * (1/2) ^ (if (w ∉ Z ∧ ∀ x, F.Adj w x → x ∉ Z) ∧ v ∉ Y then 1 else 0) := by
    rw [← pow_add, ← pow_add, ← pow_add, hPin]
  rw [merge_smul_left, merge_smul_right, smul_smul, card_union_of_disjoint hYZ, pow_add,
    sv_split hF r hAB hv hw hwr hpw hedge hZ]
  generalize (1/2 : ℝ) ^ Pin hF r ν (A ∪ B) v (Y ∪ Z) = c at hc ⊢
  generalize (1/2 : ℝ) ^ Pin hF r ν A v Y = a at hc ⊢
  generalize (1/2 : ℝ) ^ Pin hF r ν B w Z = b at hc ⊢
  unfold sv
  split_ifs at hc ⊢ <;> simp only [pow_zero, pow_one, mul_one] at hc <;> ext <;>
    simp [merge] <;>
    first
    | linear_combination (y ^ Y.card * y ^ Z.card) * hc
    | linear_combination (2 * y ^ Y.card * y ^ Z.card) * hc
    | (exfalso; tauto)

include hAB hv hw hwr hpw hedge hB hA in

/-- The step of `lem:rst-treerec`: adding the subtree `B` of the child `w` to the partial
subtree `A` of `v`. -/
theorem triple_split :
    triple hF r ν y (A ∪ B) v = merge (triple hF r ν y A v) (triple hF r ν y B w) := by
  unfold triple
  rw [sum_powerset_union hAB, merge_sum_left]
  apply sum_congr rfl
  intro Y hY
  rw [merge_sum_right]
  apply sum_congr rfl
  intro Z hZ
  exact term_split hF r ν y hAB hv hw hwr hpw hedge hB hA (mem_powerset.1 hY) (mem_powerset.1 hZ)

end Split

theorem fin_zero : fin 0 = 0 := by simp [fin]

theorem fin_sum {ι : Type*} (s : Finset ι) (f : ι → ℝ × ℝ × ℝ) :
    fin (∑ i ∈ s, f i) = ∑ i ∈ s, fin (f i) := by
  classical
  induction s using Finset.induction_on with
  | empty => simp [fin_zero]
  | insert a s ha ih => rw [sum_insert ha, sum_insert ha, fin_add, ih]

/-- The root step of `lem:rst-treerec`: `W_{F,ν}(y) = fin(ψ_r)`. -/
theorem treeW_eq_fin : treeW F ν y = fin (triple hF r ν y univ r) := by
  unfold triple treeW
  rw [fin_sum]
  apply sum_congr rfl
  intro X _
  rw [fin_smul]
  have hTP : treePotential F ν X = Pin hF r ν univ r X
      + (if r ∉ X ∧ ∀ u, F.Adj r u → u ∉ X then 1 else 0) := by
    unfold treePotential Pin
    rw [show Nat.card (F.induce (X : Set V)).ConnectedComponent = (tops hF r X).card from
      comp_eq_tops hF r X]
    have key : ∀ (inst : DecidablePred fun v => v ∉ X ∧ ∀ u, F.Adj v u → u ∉ X),
        (@filter V (fun v => v ∉ X ∧ ∀ u, F.Adj v u → u ∉ X) inst univ).card
        = (dom F univ r X).card + (if r ∉ X ∧ ∀ u, F.Adj r u → u ∉ X then 1 else 0) := by
      intro inst
      unfold dom
      rw [card_filter, card_filter, ← add_sum_erase univ _ (mem_univ r), add_comm]
      congr 1
      refine sum_congr rfl (fun u _ => ?_)
      by_cases h : u ∉ X ∧ ∀ x, F.Adj u x → x ∉ X
      · rw [if_pos h, if_pos h]
      · rw [if_neg h, if_neg h]
    rw [key]
    ring_nf
  rw [hTP, pow_add, mul_assoc]
  congr 2
  by_cases h1 : r ∈ X
  · rw [if_neg (fun h => h.1 h1)]; unfold sv; rw [if_pos h1]; simp [fin]
  · by_cases h2 : ∀ u, F.Adj r u → u ∉ X
    · rw [if_pos ⟨h1, h2⟩]; unfold sv; rw [if_neg h1, if_pos h2]; simp [fin]
    · rw [if_neg (fun h => h2 h.2)]; unfold sv; rw [if_neg h1, if_neg h2]; simp [fin]

end Recursion

/-! ### `lem:rst-F` -/

section Certificate

variable {Z : Finset (ℝ × ℝ × ℝ)}

theorem merge_hull (ha : ∀ z ∈ Z, ∀ z' ∈ Z, merge z z' ∈ PZ Z) {z z' : ℝ × ℝ × ℝ}
    (hz : z ∈ convexHull ℝ (Z : Set _)) (hz' : z' ∈ convexHull ℝ (Z : Set _)) :
    merge z z' ∈ PZ Z := by
  have step1 : ∀ z' ∈ Z, ∀ z ∈ convexHull ℝ (Z : Set (ℝ × ℝ × ℝ)), merge z z' ∈ PZ Z := by
    intro z' hz' z hz
    refine (convexHull_min (fun x hx => ha x hx z' hz') ?_ :
      convexHull ℝ (Z : Set (ℝ × ℝ × ℝ)) ⊆ {x | merge x z' ∈ PZ Z}) hz
    intro a ha' b hb s t hs ht hst
    show merge (s • a + t • b) z' ∈ PZ Z
    rw [merge_add_left, merge_smul_left, merge_smul_left]
    exact convex_PZ Z ha' hb hs ht hst
  refine (convexHull_min (fun x hx => step1 x hx z hz) ?_ :
    convexHull ℝ (Z : Set (ℝ × ℝ × ℝ)) ⊆ {x | merge z x ∈ PZ Z}) hz'
  intro a ha' b hb s t hs ht hst
  show merge z (s • a + t • b) ∈ PZ Z
  rw [merge_add_right, merge_smul_right, merge_smul_right]
  exact convex_PZ Z ha' hb hs ht hst

/-- The merge step of the proof of `lem:rst-F` (`lem:rst-abstract` (b) with `Y = Y' = Z`). -/
theorem merge_mem_smul_PZ (hZ0 : ∀ z ∈ Z, 0 ≤ z) (ha : ∀ z ∈ Z, ∀ z' ∈ Z, merge z z' ∈ PZ Z)
    {η η' : ℝ} (hη' : 0 < η') {P Q : ℝ × ℝ × ℝ} (hP : P ∈ η • PZ Z) (hQ : Q ∈ η' • PZ Z)
    (hQ0 : 0 ≤ Q) : merge P Q ∈ (η * η') • PZ Z := by
  obtain ⟨_, ⟨z, hz, Δ, hΔ, rfl⟩, rfl⟩ := hP
  obtain ⟨Qh, hQh, rfl⟩ := hQ
  have hQh0 : 0 ≤ Qh := by
    have := smul_nonneg (inv_nonneg.2 hη'.le) hQ0
    rwa [smul_smul, inv_mul_cancel₀ hη'.ne', one_smul] at this
  obtain ⟨z', hz', Δ', hΔ', rfl⟩ := hQh
  refine ⟨merge z z' + merge z Δ' + merge Δ (z' + Δ'),
    PZ_add_Kcum (PZ_add_Kcum (merge_hull ha hz hz')
      (merge_Kcum_right (convexHull_nonneg hZ0 hz) hΔ')) (merge_Kcum_left hΔ hQh0), ?_⟩
  simp only [merge_smul_left, merge_smul_right, merge_add_left, merge_add_right]
  module

/-- The tail claim of `lem:rst-F`: if `e₂ ≤ 1`, condition (b) for `j ≤ j₀` and the vector
`(y/2, 0, 0)` at scale `e₁ e₂^(j₀+1)` give (b) for every `j`. -/
theorem init_all (hZ0 : ∀ z ∈ Z, 0 ≤ z) {y e₁ e₂ : ℝ} (he₁ : 0 < e₁) (he₂ : 0 < e₂)
    (he₂1 : e₂ ≤ 1) (j₀ : ℕ) (hb : ∀ j ≤ j₀, init y j ∈ (e₁ * e₂ ^ j) • PZ Z)
    (htail : ((y / 2, 0, 0) : ℝ × ℝ × ℝ) ∈ (e₁ * e₂ ^ (j₀ + 1)) • PZ Z) :
    ∀ j, init y j ∈ (e₁ * e₂ ^ j) • PZ Z := by
  intro j
  by_cases hj : j ≤ j₀
  · exact hb j hj
  · have h1 : init y j = ((y / 2, 0, 0) : ℝ × ℝ × ℝ) + (0, 0, (1/2 : ℝ) ^ j) := by
      simp [init]
    rw [h1]
    refine smul_PZ_mono hZ0 (by positivity) ?_
      (smul_PZ_add_Kcum (by positivity) htail (Kcum_of_nonneg ?_))
    · exact mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one he₂.le he₂1 (by omega)) he₁.le
    · rw [nonneg_iff]; exact ⟨le_rfl, le_rfl, by positivity⟩

theorem cZ_le_fin (hZ : Z.Nonempty) {z : ℝ × ℝ × ℝ} (hz : z ∈ convexHull ℝ (Z : Set _)) :
    cZ Z hZ ≤ fin z := by
  refine (convexHull_min (fun x hx => inf'_le fin hx) ?_ :
    convexHull ℝ (Z : Set (ℝ × ℝ × ℝ)) ⊆ {x | cZ Z hZ ≤ fin x}) hz
  intro a ha b hb s t hs ht hst
  show cZ Z hZ ≤ fin (s • a + t • b)
  rw [fin_add, fin_smul, fin_smul]
  have ha' : cZ Z hZ ≤ fin a := ha
  have hb' : cZ Z hZ ≤ fin b := hb
  have h1 := mul_le_mul_of_nonneg_left ha' hs
  have h2 := mul_le_mul_of_nonneg_left hb' ht
  have h3 : (s + t) * cZ Z hZ = cZ Z hZ := by rw [hst, one_mul]
  linarith

open CDS SimpleGraph in
/-- The induction in the proof of `lem:rst-F`: every subtree message lies in its scaled `𝒫_Z`. -/
theorem triple_D_mem {F : SimpleGraph V} [DecidableRel F.Adj] (hF : F.IsTree) (r : V)
    (ν : V → ℕ) {y e₁ e₂ : ℝ} (hy : 0 ≤ y) (he₁ : 0 < e₁) (he₂ : 0 < e₂)
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (ha : ∀ z ∈ Z, ∀ z' ∈ Z, merge z z' ∈ PZ Z)
    (hb : ∀ j : ℕ, init y j ∈ (e₁ * e₂ ^ j) • PZ Z) (v : V) :
    triple hF r ν y (D hF r v) v
      ∈ (e₁ ^ (D hF r v).card * e₂ ^ (∑ u ∈ D hF r v, ν u)) • PZ Z := by
  induction hn : (D hF r v).card using Nat.strong_induction_on generalizing v with
  | _ n ih =>
    subst hn
    have key : ∀ C ⊆ children hF r v,
        triple hF r ν y (insert v (C.biUnion (D hF r))) v
          ∈ (e₁ ^ (insert v (C.biUnion (D hF r))).card
              * e₂ ^ (∑ u ∈ insert v (C.biUnion (D hF r)), ν u)) • PZ Z := by
      intro C
      induction C using Finset.induction_on with
      | empty =>
        intro _
        simp only [biUnion_empty, insert_empty, card_singleton, pow_one, sum_singleton]
        rw [triple_single]
        exact hb _
      | insert w C hwC ihC =>
        intro hC
        have hw : w ∈ children hF r v := hC (mem_insert_self w C)
        have hCv : C ⊆ children hF r v := fun c hc => hC (mem_insert_of_mem hc)
        obtain ⟨hwr, hpw⟩ := (mem_children hF r).1 hw
        set A := insert v (C.biUnion (D hF r)) with hAdef
        have hAB : Disjoint A (D hF r w) := by
          rw [hAdef, disjoint_insert_left, disjoint_biUnion_left]
          refine ⟨not_mem_D_child hF r hw, fun c hc => D_disjoint hF r (hCv hc) hw ?_⟩
          rintro rfl; exact hwC hc
        have hU : insert v ((insert w C).biUnion (D hF r)) = A ∪ D hF r w := by
          rw [biUnion_insert, hAdef]
          ext u; simp only [mem_insert, mem_union]; tauto
        have hedge : ∀ a ∈ A, ∀ b ∈ D hF r w, F.Adj a b → a = v ∧ b = w := by
          intro a ha b hb hab
          obtain ⟨h1, h2⟩ := D_edge hF r hwr hb (fun h => disjoint_left.1 hAB ha h) hab
          exact ⟨h2.trans hpw, h1⟩
        have hBp : ∀ u ∈ D hF r w, u ≠ w → u ≠ r ∧ par hF r u ∈ D hF r w :=
          fun u hu huw => D_par_mem hF r hwr hu huw
        have hAp : ∀ u ∈ A, u ≠ r → par hF r u ∉ D hF r w := by
          intro u hu hur hp
          have huD : u ∉ D hF r w := fun h => disjoint_left.1 hAB hu h
          obtain ⟨h1, h2⟩ := D_edge hF r hwr hp huD (par_spec hF r hur).1
          rw [hpw] at h2
          subst h2
          have := (par_spec hF r hur).2
          have := dist_child hF r hw
          rw [h1] at *
          omega
        rw [hU, triple_split hF r ν y hAB (mem_insert_self v _) (self_mem_D hF r w) hwr hpw
          hedge hBp hAp, card_union_of_disjoint hAB, sum_union hAB, pow_add, pow_add,
          show e₁ ^ A.card * e₁ ^ (D hF r w).card * (e₂ ^ (∑ u ∈ A, ν u)
              * e₂ ^ (∑ u ∈ D hF r w, ν u))
            = (e₁ ^ A.card * e₂ ^ (∑ u ∈ A, ν u))
              * (e₁ ^ (D hF r w).card * e₂ ^ (∑ u ∈ D hF r w, ν u)) by ring]
        exact merge_mem_smul_PZ hZ0 ha (by positivity) (ihC hCv)
          (ih _ (card_D_child_lt hF r hw) w rfl) (triple_nonneg hF r ν y hy _ w)
    have := key (children hF r v) subset_rfl
    rwa [← D_eq] at this

open CDS in
/-- `lem:rst-F`, for an arbitrary certificate. -/
theorem tree_bound_of_certificate (y e₁ e₂ : ℝ) (hy : 0 ≤ y) (he₁ : 0 < e₁) (he₂ : 0 < e₂)
    (Z : Finset (ℝ × ℝ × ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (ha : ∀ z ∈ Z, ∀ z' ∈ Z, merge z z' ∈ PZ Z)
    (hb : ∀ j : ℕ, init y j ∈ (e₁ * e₂ ^ j) • PZ Z)
    (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) (ν : V → ℕ) :
    cZ Z hZ * e₁ ^ Fintype.card V * e₂ ^ (∑ v, ν v) ≤ treeW T ν y := by
  obtain ⟨r⟩ := hT.connected.nonempty
  have hm := triple_D_mem hT r ν hy he₁ he₂ hZ0 ha hb r
  rw [D_root] at hm
  rw [treeW_eq_fin hT r ν y]
  obtain ⟨_, ⟨z, hz, Δ, hΔ, rfl⟩, heq⟩ := hm
  rw [← heq, fin_smul, fin_add, card_univ]
  have hη : 0 < e₁ ^ Fintype.card V * e₂ ^ (∑ v, ν v) := by positivity
  have h1 := cZ_le_fin hZ hz
  have h2 := fin_nonneg_of_Kcum hΔ
  calc cZ Z hZ * e₁ ^ Fintype.card V * e₂ ^ (∑ v, ν v)
      = (e₁ ^ Fintype.card V * e₂ ^ (∑ v, ν v)) * cZ Z hZ := by ring
    _ ≤ (e₁ ^ Fintype.card V * e₂ ^ (∑ v, ν v)) * (fin z + fin Δ) :=
        mul_le_mul_of_nonneg_left (by linarith) hη.le

end Certificate

/-! ### Exact rational checks of certificate data -/

section Check

/-- The merge over `ℚ`. -/
def mergeQ (P Q : ℚ × ℚ × ℚ) : ℚ × ℚ × ℚ :=
  (P.1 * (2 * Q.1 + Q.2.1 + Q.2.2), P.2.1 * (Q.1 + Q.2.1 + Q.2.2 / 2) + P.2.2 * Q.1,
    P.2.2 * (Q.2.1 + Q.2.2 / 2))

/-- `P ∈ 𝒦_cum`, decided over `ℚ`. -/
def cumOK (P : ℚ × ℚ × ℚ) : Bool :=
  decide (0 ≤ P.1) && decide (0 ≤ P.1 + P.2.1) && decide (0 ≤ P.1 + P.2.1 + P.2.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.1 + km.2 * (Z.getD km.1 0).2.1, acc.2.2 + km.2 * (Z.getD km.1 0).2.2)) (0, 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)

/-- `P - s ∑ μ_k z_k ∈ 𝒦_cum`, the check of `verify_cert.dominated`. -/
def domQ (Z : List (ℚ × ℚ × ℚ)) (P : ℚ × ℚ × ℚ) (s : ℚ) (mu : List (ℕ × ℚ)) : Bool :=
  muOK Z.length mu &&
    cumOK (P.1 - s * (combQ Z mu).1, P.2.1 - s * (combQ Z mu).2.1, P.2.2 - s * (combQ Z mu).2.2)

/-- Condition (a) for every ordered pair. -/
def checkPairs (Z : List (ℚ × ℚ × ℚ)) (pairs : List (List (ℕ × ℚ))) : Bool :=
  (List.range Z.length).all fun i => (List.range Z.length).all fun j =>
    domQ Z (mergeQ (Z.getD i 0) (Z.getD j 0)) 1 (pairs.getD (i * Z.length + j) [])

def initQ (y : ℚ) (j : ℕ) : ℚ × ℚ × ℚ := (y / 2, 0, (1/2 : ℚ) ^ j)

/-- Condition (b) for `j ≤ m₀`, and the tail vector at scale `e₁ e₂^(m₀+1)`. -/
def checkInits (Z : List (ℚ × ℚ × ℚ)) (y e₁ e₂ : ℚ) (m₀ : ℕ) (inits : List (List (ℕ × ℚ)))
    (tail : List (ℕ × ℚ)) : Bool :=
  (List.range (m₀ + 1)).all (fun j => domQ Z (initQ y j) (e₁ * e₂ ^ j) (inits.getD j [])) &&
    domQ Z (y / 2, 0, 0) (e₁ * e₂ ^ (m₀ + 1)) tail

/-- `Z ≠ ∅`, `Z ≥ 0` and `fin z ≥ c` on `Z`. -/
def checkZ (Z : List (ℚ × ℚ × ℚ)) (c : ℚ) : Bool :=
  !Z.isEmpty && Z.all (fun z => decide (0 ≤ z.1) && decide (0 ≤ z.2.1) && decide (0 ≤ z.2.2) &&
    decide (c ≤ z.1 + z.2.1 + z.2.2 / 2))

/-- Coordinatewise cast `ℚ³ → ℝ³`. -/
def castT (P : ℚ × ℚ × ℚ) : ℝ × ℝ × ℝ := ((P.1 : ℝ), (P.2.1 : ℝ), (P.2.2 : ℝ))

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

theorem castT_merge (P Q : ℚ × ℚ × ℚ) : castT (mergeQ P Q) = merge (castT P) (castT Q) := by
  simp only [castT, mergeQ, merge]; push_cast; rfl

theorem cumOK_sound {P : ℚ × ℚ × ℚ} (h : cumOK P = true) : castT P ∈ Kcum := by
  simp only [cumOK, Bool.and_eq_true, decide_eq_true_eq] at h
  obtain ⟨⟨h1, h2⟩, h3⟩ := h
  refine ⟨?_, ?_, ?_⟩ <;> simp only [castT]
  · exact_mod_cast h1
  · exact_mod_cast h2
  · exact_mod_cast h3

theorem getD_mem_ZR {Z : List (ℚ × ℚ × ℚ)} {k : ℕ} (hk : k < Z.length) :
    castT (Z.getD k 0) ∈ ZR Z := by
  rw [ZR, 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) →
      castT (combQ Z mu) ∈ (((mu.map Prod.snd).sum : ℚ) : ℝ) • convexHull ℝ (ZR Z : Set _) := by
  have hne : (convexHull ℝ (ZR Z : Set (ℝ × ℝ × ℝ))).Nonempty := by
    obtain ⟨z, hz⟩ := List.exists_mem_of_ne_nil Z hZ
    exact ⟨castT z, subset_convexHull ℝ _
      (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 : castT (combQ Z []) = (0 : ℝ) • z := by simp [castT, 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 : castT (combQ Z (km :: mu))
        = (km.2 : ℝ) • castT (Z.getD km.1 0) + castT (combQ Z mu) := by
      simp only [castT, 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_ZR hk.1))) ih'

theorem domQ_sound {Z : List (ℚ × ℚ × ℚ)} (hZ : Z ≠ []) {P : ℚ × ℚ × ℚ} {s : ℚ} (hs : 0 < s)
    {mu : List (ℕ × ℚ)} (h : domQ Z P s mu = true) : castT P ∈ (s : ℝ) • PZ (ZR Z) := by
  simp only [domQ, muOK, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at h
  obtain ⟨⟨hmu, hsum⟩, hcum⟩ := h
  have hc := combQ_mem hZ mu (fun km hkm => hmu km hkm)
  rw [hsum, Rat.cast_one, one_smul] at hc
  have hΔ := cumOK_sound hcum
  have hsR : (0 : ℝ) < s := by exact_mod_cast hs
  refine ⟨castT (combQ Z mu) + (s : ℝ)⁻¹ • castT (P.1 - s * (combQ Z mu).1,
      P.2.1 - s * (combQ Z mu).2.1, P.2.2 - s * (combQ Z mu).2.2),
    ⟨_, hc, _, Kcum_smul (inv_nonneg.2 hsR.le) hΔ, rfl⟩, ?_⟩
  simp only [castT, smul_add, smul_smul, mul_inv_cancel₀ hsR.ne', one_smul]
  push_cast
  ext <;> simp

theorem checkPairs_sound {Z : List (ℚ × ℚ × ℚ)} (hZ : Z ≠ []) {pairs : List (List (ℕ × ℚ))}
    (h : checkPairs Z pairs = true) :
    ∀ z ∈ ZR Z, ∀ z' ∈ ZR Z, merge z z' ∈ PZ (ZR Z) := by
  intro z hz z' hz'
  simp only [ZR, 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, castT_merge, List.getD_eq_getElem _ _ hi,
    List.getD_eq_getElem _ _ hj] at this
  exact this

theorem castT_initQ (y : ℚ) (j : ℕ) : castT (initQ y j) = init (y : ℝ) j := by
  simp [castT, initQ, init]

theorem checkInits_sound {Z : List (ℚ × ℚ × ℚ)} (hZ : Z ≠ []) (hZ0 : ∀ z ∈ ZR Z, 0 ≤ z)
    {y e₁ e₂ : ℚ} (he₁ : 0 < e₁) (he₂ : 0 < e₂) (he₂1 : e₂ ≤ 1) {m₀ : ℕ}
    {inits : List (List (ℕ × ℚ))} {tail : List (ℕ × ℚ)}
    (h : checkInits Z y e₁ e₂ m₀ inits tail = true) :
    ∀ j : ℕ, init (y : ℝ) j ∈ ((e₁ : ℝ) * (e₂ : ℝ) ^ j) • PZ (ZR Z) := by
  simp only [checkInits, Bool.and_eq_true, List.all_eq_true, List.mem_range] at h
  obtain ⟨h1, h2⟩ := h
  have he₁R : (0 : ℝ) < e₁ := by exact_mod_cast he₁
  have he₂R : (0 : ℝ) < e₂ := by exact_mod_cast he₂
  refine init_all hZ0 he₁R he₂R (by exact_mod_cast he₂1) m₀ (fun j hj => ?_) ?_
  · have := domQ_sound hZ (by positivity) (h1 j (by omega))
    rwa [castT_initQ, Rat.cast_mul, Rat.cast_pow] at this
  · have := domQ_sound hZ (by positivity) h2
    rw [Rat.cast_mul, Rat.cast_pow] at this
    convert this using 1
    simp [castT]

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

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

theorem checkZ_sound {Z : List (ℚ × ℚ × ℚ)} {c : ℚ} (h : checkZ Z c = true) :
    (∀ z ∈ ZR Z, 0 ≤ z) ∧ (c : ℝ) ≤ cZ (ZR Z) (ZR_nonempty (checkZ_nonempty h)) := by
  have h' := h
  simp only [checkZ, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at h'
  obtain ⟨-, hall⟩ := h'
  have key : ∀ z ∈ ZR Z, 0 ≤ z ∧ (c : ℝ) ≤ fin z := by
    intro z hz
    simp only [ZR, List.mem_toFinset, List.mem_map] at hz
    obtain ⟨a, ha, rfl⟩ := hz
    obtain ⟨⟨⟨h1, h2⟩, h3⟩, h4⟩ := hall a ha
    refine ⟨(nonneg_iff _).2 ⟨?_, ?_, ?_⟩, ?_⟩ <;> simp only [castT, fin]
    · exact_mod_cast h1
    · exact_mod_cast h2
    · exact_mod_cast h3
    · exact_mod_cast h4
  exact ⟨fun z hz => (key z hz).1, le_inf' _ _ (fun z hz => (key z hz).2)⟩

/-- Everything `tree_bound_of_certificate` needs, from the Boolean checks. -/
theorem tree_bound_of_checks {Z : List (ℚ × ℚ × ℚ)} {pairs inits : List (List (ℕ × ℚ))}
    {tail : List (ℕ × ℚ)} {y e₁ e₂ c : ℚ} {m₀ : ℕ} (hy : 0 ≤ y) (he₁ : 0 < e₁) (he₂ : 0 < e₂)
    (he₂1 : e₂ ≤ 1) (hZc : checkZ Z c = true) (hpairs : checkPairs Z pairs = true)
    (hinits : checkInits Z y e₁ e₂ m₀ inits tail = true)
    (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) (ν : V → ℕ) :
    (c : ℝ) * (e₁ : ℝ) ^ Fintype.card V * (e₂ : ℝ) ^ (∑ v, ν v) ≤ treeW T ν (y : ℝ) := by
  have hZ := checkZ_nonempty hZc
  obtain ⟨hZ0, hcZ⟩ := checkZ_sound hZc
  have he₁R : (0 : ℝ) < e₁ := by exact_mod_cast he₁
  have he₂R : (0 : ℝ) < e₂ := by exact_mod_cast he₂
  refine le_trans ?_ (tree_bound_of_certificate (y : ℝ) e₁ e₂ (by exact_mod_cast hy) he₁R he₂R
    (ZR Z) (ZR_nonempty hZ) hZ0 (checkPairs_sound hZ hpairs)
    (checkInits_sound hZ hZ0 he₁ he₂ he₂1 hinits) T hT ν)
  have : (0 : ℝ) ≤ (e₁ : ℝ) ^ Fintype.card V * (e₂ : ℝ) ^ (∑ v, ν v) := by positivity
  rw [mul_assoc, mul_assoc]
  exact mul_le_mul_of_nonneg_right hcZ this

end Check

end

end Antinorm3

/-! ### `prop:rst-certs`: the two stored certificates, checked in the kernel -/

namespace RSThetaCert

open Antinorm3

theorem cert0_Z : checkZ Z0 (q 6212 10000) = true := by decide +kernel

theorem cert0_pairs : checkPairs Z0 pairs0 = true := by decide +kernel

theorem cert0_inits : checkInits Z0 y0 e1_0 e2_0 m0_0 inits0 tail0 = true := by decide +kernel

theorem cert1_Z : checkZ Z1 (q 6293 10000) = true := by decide +kernel

theorem cert1_pairs : checkPairs Z1 pairs1 = true := by decide +kernel

theorem cert1_inits : checkInits Z1 y1 e1_1 e2_1 m0_1 inits1 tail1 = true := by decide +kernel

end RSThetaCert

open Antinorm3 RSThetaCert in
/-- `prop:rst-certs` + `lem:rst-F`: the first RS-θ tree bound. -/
theorem rstheta_tree_bound_0 (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree)
    (ν : V → ℕ) :
    (6212/10000 : ℝ) * (747593601/960952792 : ℝ) ^ Fintype.card V
        * (512099210/652701491 : ℝ) ^ (∑ v, ν v)
      ≤ treeW T ν (69/200) := by
  have h := tree_bound_of_checks (by norm_num [y0, q]) (by norm_num [e1_0, q])
    (by norm_num [e2_0, q]) (by norm_num [e2_0, q]) cert0_Z cert0_pairs cert0_inits T hT ν
  convert h using 3 <;> norm_num [y0, e1_0, e2_0, q]

open Antinorm3 RSThetaCert in
/-- `prop:rst-certs` + `lem:rst-F`: the second RS-θ tree bound. -/
theorem rstheta_tree_bound_1 (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree)
    (ν : V → ℕ) :
    (6293/10000 : ℝ) * (248231700/312721579 : ℝ) ^ Fintype.card V
        * (568097827/739289481 : ℝ) ^ (∑ v, ν v)
      ≤ treeW T ν (17/50) := by
  have h := tree_bound_of_checks (by norm_num [y1, q]) (by norm_num [e1_1, q])
    (by norm_num [e2_1, q]) (by norm_num [e2_1, q]) cert1_Z cert1_pairs cert1_inits T hT ν
  convert h using 3 <;> norm_num [y1, e1_1, e2_1, q]

end MaxLeafFormal