MaxLeafFormal.Antinorm8

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

import Mathlib

/-!
# The abstract RSC certificate lemma

Transcribes `sec:rsc-rec` (states, merge, `Init`), the order and cone of `sec:rsc-cert`, `def:rsc-light`
and the admissible triples of the paper, and proves `lem:rsc-cone` (b), (c) and
`lem:rsc-cert`.
-/

namespace MaxLeafFormal.Antinorm8

open Finset Pointwise

/-- Ordered rooted trees with a label at each node. -/
inductive RTree (α : Type) where
  | node : α → List (RTree α) → RTree α

noncomputable section

/-! ### States `A, C₀, C₁, C₂, O₀₀, O₀₁, O₁, O₂` (indices `0, …, 7`), merge and `fin` -/

/-- `χ_S(Q)`. -/
def chiS (p : ℝ) (Q : Fin 8 → ℝ) : ℝ :=
  2 * Q 0 + 2 * Q 2 + 2 * Q 3 + Q 4 + Q 5 + (1 - p) * (Q 6 + Q 7)

/-- `χ^s_C(Q)`. -/
def chiCs (Q : Fin 8 → ℝ) : ℝ := 2 * Q 0

/-- `χ^u_C(Q)`. -/
def chiCu (p : ℝ) (Q : Fin 8 → ℝ) : ℝ := 2 * Q 3 + Q 4 + Q 5 + Q 6 + (1 - p) * Q 7

/-- `χ^s_O(Q)`. -/
def chiOs (Q : Fin 8 → ℝ) : ℝ := Q 0

/-- `χ^x_O(Q)`. -/
def chiOx (Q : Fin 8 → ℝ) : ℝ := Q 3

/-- `χ^u_O(Q)`. -/
def chiOu (p : ℝ) (Q : Fin 8 → ℝ) : ℝ := Q 4 / 2 + Q 5 + Q 6 + (1 - p) * Q 7

/-- The merge `P ∘ Q` of `sec:rsc-rec`. -/
def merge (p : ℝ) (P Q : Fin 8 → ℝ) : Fin 8 → ℝ :=
  ![P 0 * chiS p Q,
    P 1 * chiCu p Q,
    P 2 * chiCu p Q + P 1 * chiCs Q,
    P 3 * (chiCu p Q + chiCs Q) + P 2 * chiCs Q,
    P 4 * chiOu p Q,
    P 5 * (chiOu p Q + chiOx Q) + P 4 * chiOx Q,
    P 6 * (chiOu p Q + chiOx Q) + (P 4 + P 5) * chiOs Q,
    P 7 * (chiOu p Q + chiOx Q + chiOs Q) + P 6 * chiOs Q]

def fin (p : ℝ) (P : Fin 8 → ℝ) : ℝ := P 0 + P 3 + P 4 / 2 + P 5 + P 6 + (1 - p) * P 7

/-- `Init(ν, ν')`. -/
def init (p y : ℝ) (ν ν' : ℕ) : Fin 8 → ℝ :=
  ![(1 - p) ^ ν' * y / 2, (1 - p) ^ ν' * p / 2, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0]

/-- `Init(∞)`. -/
def initInf (p y : ℝ) : Fin 8 → ℝ := ![y / 2, p / 2, 0, 0, 0, 0, 0, 0]

/-- `Ex_j`: the first four coordinates multiplied by `q^j`. -/
def ex (p : ℝ) (j : ℕ) (P : Fin 8 → ℝ) : Fin 8 → ℝ :=
  fun i => if i.val < 4 then (1 - p) ^ j * P i else P i

/-! ### The order, `𝒦_pos` and `𝒫_Z` -/

/-- The generating relations `x ≺ x'` of the order: `C₁ ≺ C₂`, `C₀ ≺ C₁`, `O₀₁ ≺ C₂`,
`O₀₀ ≺ O₀₁`, `O₁ ≺ O₀₁`, `O₂ ≺ O₁`. -/
def covers (x x' : Fin 8) : Prop :=
  (x = 2 ∧ x' = 3) ∨ (x = 1 ∧ x' = 2) ∨ (x = 5 ∧ x' = 3) ∨ (x = 4 ∧ x' = 5) ∨
    (x = 6 ∧ x' = 5) ∨ (x = 7 ∧ x' = 6)

/-- `x ≼ x'`: the reflexive and transitive closure. -/
def below (x x' : Fin 8) : Prop := Relation.ReflTransGen covers x x'

def IsUpSet (U : Finset (Fin 8)) : Prop := ∀ x x', below x x' → x ∈ U → x' ∈ U

def Kpos : Set (Fin 8 → ℝ) := {P | ∀ U, IsUpSet U → 0 ≤ ∑ i ∈ U, P i}

def PZ (Z : Finset (Fin 8 → ℝ)) : Set (Fin 8 → ℝ) := convexHull ℝ (Z : Set _) + Kpos

def cZ (p : ℝ) (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) : ℝ := Z.inf' hZ (fin p)

/-- `def:rsc-light`, with `q = 1 - p`, `𝖻 = 2 + 2p/y`, `δ = ln(2q)`, `δ' = -ln q` (`sec:rsc`). -/
def Light (p y : ℝ) (ν d : ℕ) : Prop :=
  (1 - p) * (1/2 : ℝ) ^ ν * ((2 + 2 * p / y) ^ d)⁻¹
    ≥ (1 + p / y) * (-Real.log (1 - p)) * y / Real.log (2 * (1 - p))

/-! ### Trees: messages, admissibility, sizes -/

mutual

/-- `M_v` of `lem:rsc-recursion` with the empty forcing. -/
def message (p y : ℝ) : RTree (ℕ × ℕ) → Fin 8 → ℝ
  | .node (ν, ν') cs => mergeAll p y (init p y ν ν') cs

/-- Merge the children's messages one by one, in order. -/
def mergeAll (p y : ℝ) : (Fin 8 → ℝ) → List (RTree (ℕ × ℕ)) → Fin 8 → ℝ
  | P, [] => P
  | P, c :: cs => mergeAll p y (merge p P (message p y c)) cs
end

mutual

/-- Admissibility at every node, for a lightness predicate `L`; `hasParent` adds `1` to the
degree. -/
def AdmAt (L : ℕ → ℕ → Prop) : Bool → RTree (ℕ × ℕ) → Prop
  | hasParent, .node (ν, ν') cs =>
    (ν' ≤ ν ∧ ((L ν (cs.length + if hasParent then 1 else 0) ∨
        cs.length + (if hasParent then 1 else 0) = 0) → ν' = 0) ∧
      ((cs.length + (if hasParent then 1 else 0) = 1 ∧ 1 ≤ ν') → ν' ≤ ν - 1)) ∧ AdmAll L cs

def AdmAll (L : ℕ → ℕ → Prop) : List (RTree (ℕ × ℕ)) → Prop
  | [] => True
  | c :: cs => AdmAt L true c ∧ AdmAll L cs
end

/-- Admissible triples (for `p`, `y`); the root's degree is its number of children. -/
def Admissible (p y : ℝ) (t : RTree (ℕ × ℕ)) : Prop := AdmAt (Light p y) false t

mutual

def size {α : Type} : RTree α → ℕ
  | .node _ cs => 1 + sizeAll cs

def sizeAll {α : Type} : List (RTree α) → ℕ
  | [] => 0
  | c :: cs => size c + sizeAll cs
end

mutual

def nuSum : RTree (ℕ × ℕ) → ℕ
  | .node (ν, _) cs => ν + nuSumAll cs

def nuSumAll : List (RTree (ℕ × ℕ)) → ℕ
  | [] => 0
  | c :: cs => nuSum c + nuSumAll cs
end

/-! ### Algebra of the merge -/

section Algebra

variable {p : ℝ}

theorem merge_add_left (P P' Q : Fin 8 → ℝ) : merge p (P + P') Q = merge p P Q + merge p P' Q := by
  funext i; fin_cases i <;> simp [merge] <;> ring

theorem merge_add_right (P Q Q' : Fin 8 → ℝ) : merge p P (Q + Q') = merge p P Q + merge p P Q' := by
  funext i; fin_cases i <;> simp [merge, chiS, chiCs, chiCu, chiOs, chiOx, chiOu] <;> ring

theorem merge_smul_left (a : ℝ) (P Q : Fin 8 → ℝ) : merge p (a • P) Q = a • merge p P Q := by
  funext i; fin_cases i <;> simp [merge] <;> ring

theorem merge_smul_right (a : ℝ) (P Q : Fin 8 → ℝ) : merge p P (a • Q) = a • merge p P Q := by
  funext i; fin_cases i <;> simp [merge, chiS, chiCs, chiCu, chiOs, chiOx, chiOu] <;> ring

theorem fin_add (P Q : Fin 8 → ℝ) : fin p (P + Q) = fin p P + fin p Q := by
  simp only [fin, Pi.add_apply]; ring

theorem fin_smul (a : ℝ) (P : Fin 8 → ℝ) : fin p (a • P) = a * fin p P := by
  simp only [fin, Pi.smul_apply, smul_eq_mul]; ring

theorem merge_nonneg (hp1 : p ≤ 1) {P Q : Fin 8 → ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q) :
    0 ≤ merge p P Q := by
  have hq : 0 ≤ 1 - p := by linarith
  have h : ∀ i, 0 ≤ P i := fun i => hP i
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  intro i
  fin_cases i <;> simp [merge, chiS, chiCs, chiCu, chiOs, chiOx, chiOu] <;>
    repeat (first | exact h _ | exact g _ | exact hq | apply add_nonneg | apply mul_nonneg | norm_num)

end Algebra

/-! ### `lem:rsc-cone` -/

section Cone

theorem below_of_covers {x x' : Fin 8} (h : covers x x') : below x x' :=
  Relation.ReflTransGen.single h

theorem mono_below {w : Fin 8 → ℝ} (hw : ∀ x x', covers x x' → w x ≤ w x') {x x' : Fin 8}
    (h : below x x') : w x ≤ w x' := by
  induction h with
  | refl => exact le_rfl
  | tail _ hc ih => exact ih.trans (hw _ _ hc)

/-- `lem:rsc-cone` (a), the direction that is used: a nonnegative functional that is monotone
along the order is nonnegative on `𝒦_pos` (layer-cake decomposition, by induction on the size of
the support). -/
theorem layer_cake : ∀ (n : ℕ) (w : Fin 8 → ℝ), (univ.filter (fun x => w x ≠ 0)).card = n →
    (∀ x, 0 ≤ w x) → (∀ x x', covers x x' → w x ≤ w x') → ∀ Δ ∈ Kpos, 0 ≤ ∑ x, w x * Δ x := by
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih =>
  intro w hn hw0 hwm Δ hΔ
  by_cases hU : (univ.filter (fun x => 0 < w x)).Nonempty
  · set U := univ.filter (fun x => 0 < w x) with hUdef
    set m := U.inf' hU w with hmdef
    have hm : 0 < m := (lt_inf'_iff hU).2 (fun x hx => (mem_filter.1 hx).2)
    have hUup : IsUpSet U := by
      intro x x' hb hx
      simp only [hUdef, mem_filter, mem_univ, true_and] at hx ⊢
      exact lt_of_lt_of_le hx (mono_below hwm hb)
    have hzero : ∀ x, x ∉ U → w x = 0 := fun x hx =>
      le_antisymm (by simpa [hUdef] using hx) (hw0 x)
    obtain ⟨x0, hx0, hx0m⟩ := exists_mem_eq_inf' hU w
    set w'' : Fin 8 → ℝ := fun x => w x - if x ∈ U then m else 0 with hw''
    have h0 : ∀ x, 0 ≤ w'' x := by
      intro x; simp only [hw'']; split_ifs with hx
      · linarith [inf'_le w hx]
      · linarith [hw0 x]
    have hmono : ∀ x x', covers x x' → w'' x ≤ w'' x' := by
      intro x x' hc
      by_cases hx : x ∈ U
      · have hx' : x' ∈ U := hUup x x' (below_of_covers hc) hx
        simp only [hw'', if_pos hx, if_pos hx']; linarith [hwm x x' hc]
      · have : w'' x = 0 := by simp only [hw'', if_neg hx, hzero x hx, sub_zero]
        rw [this]; exact h0 x'
    have hcard : (univ.filter (fun x => w'' x ≠ 0)).card < n := by
      rw [← hn]
      apply card_lt_card
      rw [ssubset_iff_of_subset]
      · refine ⟨x0, ?_, ?_⟩
        · simp only [mem_filter, mem_univ, true_and]
          exact ne_of_gt (mem_filter.1 hx0).2
        · simp only [mem_filter, mem_univ, true_and, not_not, hw'', if_pos hx0, ← hx0m]
          exact sub_eq_zero.2 hmdef.symm
      · intro x hx
        simp only [mem_filter, mem_univ, true_and] at hx ⊢
        intro h; apply hx
        have hxU : x ∉ U := fun hxU => by
          have := (mem_filter.1 hxU).2; rw [h] at this; exact lt_irrefl _ this
        simp only [hw'', if_neg hxU, h, sub_zero]
    have key := ih _ hcard w'' rfl h0 hmono Δ hΔ
    have hpt : ∀ x, w x * Δ x = w'' x * Δ x + (if x ∈ U then m * Δ x else 0) := by
      intro x; simp only [hw'']; split_ifs <;> ring
    rw [sum_congr rfl (fun x _ => hpt x), sum_add_distrib, ← sum_filter, filter_mem_eq_inter,
      univ_inter, ← mul_sum]
    exact add_nonneg key (mul_nonneg hm.le (hΔ U hUup))
  · have : ∀ x, w x = 0 := fun x => le_antisymm
      (by by_contra h; exact hU ⟨x, by simp only [mem_filter, mem_univ, true_and]; linarith⟩)
      (hw0 x)
    simp [this]

theorem func_nonneg (c : Fin 8 → ℝ) (h0 : ∀ x, 0 ≤ c x) (hm : ∀ x x', covers x x' → c x ≤ c x')
    {Δ : Fin 8 → ℝ} (hΔ : Δ ∈ Kpos) : 0 ≤ ∑ x, c x * Δ x :=
  layer_cake _ c rfl h0 hm Δ hΔ

theorem Kpos_of_nonneg {P : Fin 8 → ℝ} (h : 0 ≤ P) : P ∈ Kpos :=
  fun U _ => sum_nonneg (fun i _ => h i)

theorem Kpos_add {P Q : Fin 8 → ℝ} (hP : P ∈ Kpos) (hQ : Q ∈ Kpos) : P + Q ∈ Kpos := by
  intro U hU; simp only [Pi.add_apply, sum_add_distrib]; exact add_nonneg (hP U hU) (hQ U hU)

theorem Kpos_smul {a : ℝ} (ha : 0 ≤ a) {P : Fin 8 → ℝ} (hP : P ∈ Kpos) : a • P ∈ Kpos := by
  intro U hU; simp only [Pi.smul_apply, smul_eq_mul, ← mul_sum]; exact mul_nonneg ha (hP U hU)

theorem sum_upset (U : Finset (Fin 8)) (f : Fin 8 → ℝ) :
    ∑ i ∈ U, f i = ∑ x, (if x ∈ U then 1 else 0) * f x := by
  simp only [boole_mul]
  rw [← sum_filter, filter_mem_eq_inter, univ_inter]

theorem indicator_mono {U : Finset (Fin 8)} (hU : IsUpSet U) :
    ∀ x x', covers x x' → (if x ∈ U then (1 : ℝ) else 0) ≤ if x' ∈ U then 1 else 0 := by
  intro x x' hc
  by_cases hx : x ∈ U
  · rw [if_pos hx, if_pos (hU x x' (below_of_covers hc) hx)]
  · rw [if_neg hx]; split_ifs <;> norm_num

variable {p : ℝ}

/-- The dual functional `w'` with `w(Δ ∘ Q) = w'(Δ)` (proof of `lem:rsc-cone` (b)). -/
def dualL (p : ℝ) (Q w : Fin 8 → ℝ) : Fin 8 → ℝ :=
  ![chiS p Q * w 0,
    chiCu p Q * w 1 + chiCs Q * w 2,
    chiCu p Q * w 2 + chiCs Q * w 3,
    (chiCu p Q + chiCs Q) * w 3,
    chiOu p Q * w 4 + chiOx Q * w 5 + chiOs Q * w 6,
    (chiOu p Q + chiOx Q) * w 5 + chiOs Q * w 6,
    (chiOu p Q + chiOx Q) * w 6 + chiOs Q * w 7,
    (chiOu p Q + chiOx Q + chiOs Q) * w 7]

theorem sum_merge_left (Q w Δ : Fin 8 → ℝ) :
    ∑ x, w x * merge p Δ Q x = ∑ x, dualL p Q w x * Δ x := by
  simp only [Fin.sum_univ_eight, merge, dualL]
  simp
  ring

/-- `lem:rsc-cone` (b), `Δ ∘ Q`. -/
theorem merge_Kpos_left (hp1 : p ≤ 1) {Δ Q : Fin 8 → ℝ} (hΔ : Δ ∈ Kpos) (hQ : 0 ≤ Q) :
    merge p Δ Q ∈ Kpos := by
  intro U hU
  rw [sum_upset, sum_merge_left]
  have hq : 0 ≤ 1 - p := by linarith
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  set w : Fin 8 → ℝ := fun x => if x ∈ U then 1 else 0 with hw
  have hw0 : ∀ x, 0 ≤ w x := fun x => by simp only [hw]; split_ifs <;> norm_num
  have hwm := indicator_mono hU
  have hS : 0 ≤ chiS p Q := by
    simp only [chiS]; have := mul_nonneg hq (add_nonneg (g 6) (g 7)); linarith [g 0, g 2, g 3, g 4, g 5]
  have hCs : 0 ≤ chiCs Q := by simp only [chiCs]; linarith [g 0]
  have hCu : 0 ≤ chiCu p Q := by
    simp only [chiCu]; have := mul_nonneg hq (g 7); linarith [g 3, g 4, g 5, g 6]
  have hOs : 0 ≤ chiOs Q := g 0
  have hOx : 0 ≤ chiOx Q := g 3
  have hOu : 0 ≤ chiOu p Q := by
    simp only [chiOu]; have := mul_nonneg hq (g 7); linarith [g 4, g 5, g 6]
  have hgap : chiOu p Q + chiOx Q + chiOs Q ≤ chiCu p Q + chiCs Q := by
    simp only [chiOu, chiOx, chiOs, chiCu, chiCs]; linarith [g 0, g 3, g 4]
  apply func_nonneg
  · intro x
    fin_cases x <;> simp [dualL] <;> positivity
  · have c23 : w 2 ≤ w 3 := hwm 2 3 (Or.inl ⟨rfl, rfl⟩)
    have c12 : w 1 ≤ w 2 := hwm 1 2 (Or.inr (Or.inl ⟨rfl, rfl⟩))
    have c53 : w 5 ≤ w 3 := hwm 5 3 (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩)))
    have c45 : w 4 ≤ w 5 := hwm 4 5 (Or.inr (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩))))
    have c65 : w 6 ≤ w 5 := hwm 6 5 (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩)))))
    have c76 : w 7 ≤ w 6 := hwm 7 6 (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨rfl, rfl⟩)))))
    clear_value w
    rintro x x' (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;>
      simp [dualL]
    · nlinarith [mul_nonneg hCu (sub_nonneg.2 c23)]
    · nlinarith [mul_nonneg hCu (sub_nonneg.2 c12), mul_nonneg hCs (sub_nonneg.2 c23)]
    · nlinarith [mul_nonneg (sub_nonneg.2 hgap) (hw0 3),
        mul_nonneg (add_nonneg hOu hOx) (sub_nonneg.2 (c53.trans le_rfl)),
        mul_nonneg hOs (sub_nonneg.2 (c65.trans c53)), mul_nonneg hOs (sub_nonneg.2 c65)]
    · nlinarith [mul_nonneg hOu (sub_nonneg.2 c45)]
    · nlinarith [mul_nonneg (add_nonneg hOu hOx) (sub_nonneg.2 c65),
        mul_nonneg hOs (sub_nonneg.2 c76)]
    · nlinarith [mul_nonneg (add_nonneg hOu hOx) (sub_nonneg.2 c76)]
  · exact hΔ

/-- `lem:rsc-cone` (b), `Q ∘ Δ`. -/
theorem merge_Kpos_right (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Q Δ : Fin 8 → ℝ} (hQ : 0 ≤ Q) (hΔ : Δ ∈ Kpos) :
    merge p Q Δ ∈ Kpos := by
  have hq : 0 ≤ 1 - p := by linarith
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  -- the eight functionals of the child message, nonnegative and monotone
  have F : ∀ c : Fin 8 → ℝ, (∀ x, 0 ≤ c x) → c 2 ≤ c 3 → c 1 ≤ c 2 → c 5 ≤ c 3 → c 4 ≤ c 5 →
      c 6 ≤ c 5 → c 7 ≤ c 6 → 0 ≤ ∑ x, c x * Δ x := by
    intro c h0 h23 h12 h53 h45 h65 h76
    refine func_nonneg c h0 ?_ hΔ
    rintro x x' (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;>
      assumption
  have nn : ∀ (a b c d e f g h : ℝ), 0 ≤ a → 0 ≤ b → 0 ≤ c → 0 ≤ d → 0 ≤ e → 0 ≤ f → 0 ≤ g →
      0 ≤ h → ∀ x, 0 ≤ (![a, b, c, d, e, f, g, h] : Fin 8 → ℝ) x := by
    intro a b c d e f g h ha hb hc hd he hf hg hh x
    fin_cases x <;> simpa
  have hS : 0 ≤ chiS p Δ := by
    have := F ![2, 0, 2, 2, 1, 1, 1 - p, 1 - p] (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl
      (by norm_num) (by norm_num) (by norm_num) (by norm_num) hq hq) (by simp) (by simp)
      (by simp) (by simp) (by simp; linarith) (by simp)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiS]; linarith
  have hCs : 0 ≤ chiCs Δ := by
    have := F ![2, 0, 0, 0, 0, 0, 0, 0] (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl le_rfl le_rfl
      le_rfl le_rfl le_rfl le_rfl) (by simp) (by simp) (by simp) (by simp) (by simp) (by simp)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiCs]; linarith
  have hCu : 0 ≤ chiCu p Δ := by
    have := F ![0, 0, 0, 2, 1, 1, 1, 1 - p] (nn _ _ _ _ _ _ _ _ le_rfl le_rfl le_rfl (by norm_num)
      (by norm_num) (by norm_num) (by norm_num) hq) (by simp) (by simp) (by simp) (by simp)
      (by simp) (by simp; linarith)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiCu]; linarith
  have hCuCs : 0 ≤ chiCu p Δ + chiCs Δ := by
    have := F ![2, 0, 0, 2, 1, 1, 1, 1 - p] (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl le_rfl
      (by norm_num) (by norm_num) (by norm_num) (by norm_num) hq) (by simp) (by simp) (by simp)
      (by simp) (by simp) (by simp; linarith)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiCu, chiCs]; linarith
  have hOs : 0 ≤ chiOs Δ := by
    have := F ![1, 0, 0, 0, 0, 0, 0, 0] (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl le_rfl le_rfl
      le_rfl le_rfl le_rfl le_rfl) (by simp) (by simp) (by simp) (by simp) (by simp) (by simp)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiOs]; linarith
  have hOx : 0 ≤ chiOx Δ := by
    have := F ![0, 0, 0, 1, 0, 0, 0, 0] (nn _ _ _ _ _ _ _ _ le_rfl le_rfl le_rfl (by norm_num)
      le_rfl le_rfl le_rfl le_rfl) (by simp) (by simp) (by simp) (by simp) (by simp) (by simp)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiOx]; linarith
  have hOuOx : 0 ≤ chiOu p Δ + chiOx Δ := by
    have := F ![0, 0, 0, 1, 1/2, 1, 1, 1 - p] (nn _ _ _ _ _ _ _ _ le_rfl le_rfl le_rfl
      (by norm_num) (by norm_num) (by norm_num) (by norm_num) hq) (by simp) (by simp) (by simp)
      (by norm_num) (by simp) (by simp; linarith)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiOu, chiOx]; linarith
  have hO : 0 ≤ chiOu p Δ + chiOx Δ + chiOs Δ := by
    have := F ![1, 0, 0, 1, 1/2, 1, 1, 1 - p] (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl le_rfl
      (by norm_num) (by norm_num) (by norm_num) (by norm_num) hq) (by simp) (by simp) (by simp)
      (by norm_num) (by simp) (by simp; linarith)
    simp only [Fin.sum_univ_eight] at this; simp at this
    simp only [chiOu, chiOx, chiOs]; linarith
  -- coordinates of `Q ∘ Δ`
  set M := merge p Q Δ with hM
  have hc : ∀ x, x ≠ 4 → 0 ≤ M x := by
    intro x hx
    fin_cases x <;> simp [hM, merge] at hx ⊢
    · exact mul_nonneg (g 0) hS
    · exact mul_nonneg (g 1) hCu
    · exact add_nonneg (mul_nonneg (g 2) hCu) (mul_nonneg (g 1) hCs)
    · exact add_nonneg (mul_nonneg (g 3) hCuCs) (mul_nonneg (g 2) hCs)
    · exact add_nonneg (mul_nonneg (g 5) hOuOx) (mul_nonneg (g 4) hOx)
    · exact add_nonneg (mul_nonneg (g 6) hOuOx) (mul_nonneg (add_nonneg (g 4) (g 5)) hOs)
    · exact add_nonneg (mul_nonneg (g 7) hO) (mul_nonneg (g 6) hOs)
  have h45 : 0 ≤ M 4 + M 5 := by
    simp only [hM, merge]; simp
    nlinarith [mul_nonneg (add_nonneg (g 4) (g 5)) hOuOx]
  intro U hU
  by_cases h4 : (4 : Fin 8) ∈ U
  · have h5 : (5 : Fin 8) ∈ U := hU 4 5 (below_of_covers (Or.inr (Or.inr (Or.inr (Or.inl
      ⟨rfl, rfl⟩))))) h4
    rw [← add_sum_erase U _ h4, ← add_sum_erase _ _ (mem_erase.2 ⟨by decide, h5⟩)]
    have : 0 ≤ ∑ x ∈ (U.erase 4).erase 5, M x :=
      sum_nonneg (fun x hx => hc x (ne_of_mem_erase (mem_of_mem_erase hx)))
    linarith
  · exact sum_nonneg (fun x hx => hc x (fun h => h4 (h ▸ hx)))

/-- `lem:rsc-cone` (c). -/
theorem fin_nonneg_of_Kpos (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Δ : Fin 8 → ℝ} (hΔ : Δ ∈ Kpos) : 0 ≤ fin p Δ := by
  have hq : 0 ≤ 1 - p := by linarith
  have := func_nonneg ![1, 0, 0, 1, 1/2, 1, 1, 1 - p]
    (by intro x; fin_cases x <;> simp; linarith)
    (by
      rintro x x' (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;>
        simp <;> linarith)
    hΔ
  simp only [Fin.sum_univ_eight] at this; simp at this
  simp only [fin]; linarith

/-! ### `𝒫_Z` -/

theorem convexHull_nonneg {Y : Finset (Fin 8 → ℝ)} (hY0 : ∀ y ∈ Y, 0 ≤ y) {z : Fin 8 → ℝ}
    (hz : z ∈ convexHull ℝ (Y : Set _)) : 0 ≤ z :=
  (convexHull_min (fun z hz => hY0 z hz) (convex_Ici 0) :
    convexHull ℝ (Y : Set (Fin 8 → ℝ)) ⊆ Set.Ici 0) hz

theorem convex_hullKpos (Y : Finset (Fin 8 → ℝ)) : Convex ℝ (convexHull ℝ (Y : Set _) + Kpos) :=
  (convex_convexHull ℝ _).add (by
    intro P hP Q hQ a b ha hb _
    exact Kpos_add (Kpos_smul ha hP) (Kpos_smul hb hQ))

theorem hullKpos_add {Y : Finset (Fin 8 → ℝ)} {P Δ : Fin 8 → ℝ}
    (hP : P ∈ convexHull ℝ (Y : Set _) + Kpos) (hΔ : Δ ∈ Kpos) :
    P + Δ ∈ convexHull ℝ (Y : Set _) + Kpos := by
  obtain ⟨z, hz, Δ', hΔ', rfl⟩ := hP
  exact ⟨z, hz, Δ' + Δ, Kpos_add hΔ' hΔ, by rw [add_assoc]⟩

/-- The closure step behind Step 1 and Step 3 of `lem:rsc-cert`. -/
theorem merge_hull (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Y Y' Z : Finset (Fin 8 → ℝ)} (hY0 : ∀ y ∈ Y, 0 ≤ y)
    (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (h : ∀ y ∈ Y, ∀ z ∈ Z, merge p y z ∈ convexHull ℝ (Y' : Set _) + Kpos)
    {x Q : Fin 8 → ℝ} (hx : x ∈ convexHull ℝ (Y : Set _) + Kpos)
    (hQ : Q ∈ convexHull ℝ (Z : Set _) + Kpos) (hQ0 : 0 ≤ Q) :
    merge p x Q ∈ convexHull ℝ (Y' : Set _) + Kpos := by
  have hconv := convex_hullKpos Y'
  have step1 : ∀ z ∈ Z, ∀ u ∈ convexHull ℝ (Y : Set (Fin 8 → ℝ)),
      merge p u z ∈ convexHull ℝ (Y' : Set _) + Kpos := by
    intro z hz u hu
    refine (convexHull_min (fun y hy => h y hy z hz) ?_ :
      convexHull ℝ (Y : Set (Fin 8 → ℝ)) ⊆ {u | merge p u z ∈ convexHull ℝ (Y' : Set _) + Kpos})
      hu
    intro a ha b hb s t hs ht hst
    show merge p (s • a + t • b) z ∈ convexHull ℝ (Y' : Set (Fin 8 → ℝ)) + Kpos
    rw [merge_add_left, merge_smul_left, merge_smul_left]
    exact hconv ha hb hs ht hst
  have step2 : ∀ u ∈ convexHull ℝ (Y : Set (Fin 8 → ℝ)), ∀ u' ∈ convexHull ℝ (Z : Set (Fin 8 → ℝ)),
      merge p u u' ∈ convexHull ℝ (Y' : Set _) + Kpos := by
    intro u hu u' hu'
    refine (convexHull_min (fun z hz => step1 z hz u hu) ?_ :
      convexHull ℝ (Z : Set (Fin 8 → ℝ)) ⊆ {v | merge p u v ∈ convexHull ℝ (Y' : Set _) + Kpos})
      hu'
    intro a ha b hb s t hs ht hst
    show merge p u (s • a + t • b) ∈ convexHull ℝ (Y' : Set (Fin 8 → ℝ)) + Kpos
    rw [merge_add_right, merge_smul_right, merge_smul_right]
    exact hconv ha hb hs ht hst
  obtain ⟨u, hu, Δ, hΔ, rfl⟩ := hx
  obtain ⟨u', hu', Δ', hΔ', rfl⟩ := hQ
  rw [merge_add_left, merge_add_right, add_assoc]
  exact hullKpos_add (step2 u hu u' hu')
    (Kpos_add (merge_Kpos_right hp0 hp1 (convexHull_nonneg hY0 hu) hΔ')
      (merge_Kpos_left hp1 hΔ hQ0))

/-- Step 1 of `lem:rsc-cert` (supermultiplicativity). -/
theorem merge_mem_smul_PZ (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p z z' ∈ PZ Z) {η η' : ℝ} (hη : 0 < η) (hη' : 0 < η')
    {P Q : Fin 8 → ℝ} (hP : P ∈ η • PZ Z) (hQ : Q ∈ η' • PZ Z) (hQ0 : 0 ≤ Q) :
    merge p P Q ∈ (η * η') • PZ Z := by
  obtain ⟨P', hP', rfl⟩ := hP
  obtain ⟨Q', hQ', rfl⟩ := hQ
  have hQ'0 : 0 ≤ Q' := by
    have := smul_nonneg (inv_nonneg.2 hη'.le) hQ0
    rwa [smul_smul, inv_mul_cancel₀ hη'.ne', one_smul] at this
  refine ⟨merge p P' Q', merge_hull hp0 hp1 hZ0 hZ0 C1 hP' hQ' hQ'0, ?_⟩
  simp only [merge_smul_left, merge_smul_right, smul_smul, mul_comm η' η]

theorem smul_PZ_add_Kpos {Z : Finset (Fin 8 → ℝ)} {η : ℝ} (hη : 0 < η) {P Δ : Fin 8 → ℝ}
    (hP : P ∈ η • PZ Z) (hΔ : Δ ∈ Kpos) : P + Δ ∈ η • PZ Z := by
  obtain ⟨P', hP', rfl⟩ := hP
  refine ⟨P' + η⁻¹ • Δ, hullKpos_add hP' (Kpos_smul (inv_nonneg.2 hη.le) hΔ), ?_⟩
  simp only [smul_add, smul_smul, mul_inv_cancel₀ hη.ne', one_smul]

theorem smul_PZ_mono {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) {η η' : ℝ} (hη' : 0 < η')
    (hle : η' ≤ η) {P : Fin 8 → ℝ} (hP : P ∈ η • PZ Z) : P ∈ η' • PZ Z := by
  obtain ⟨_, ⟨z, hz, Δ, hΔ, rfl⟩, rfl⟩ := hP
  refine ⟨z + (((η - η') / η') • z + (η / η') • Δ), ⟨z, hz, _, Kpos_add
    (Kpos_of_nonneg (smul_nonneg (div_nonneg (by linarith) hη'.le) (convexHull_nonneg hZ0 hz)))
    (Kpos_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 cZ_le_fin {Z : Finset (Fin 8 → ℝ)} (hZ : Z.Nonempty) {z : Fin 8 → ℝ}
    (hz : z ∈ convexHull ℝ (Z : Set _)) : cZ p Z hZ ≤ fin p z := by
  refine (convexHull_min (fun x hx => inf'_le (fin p) hx) ?_ :
    convexHull ℝ (Z : Set (Fin 8 → ℝ)) ⊆ {x | cZ p Z hZ ≤ fin p x}) hz
  intro a ha b hb s t hs ht hst
  show cZ p Z hZ ≤ fin p (s • a + t • b)
  rw [fin_add, fin_smul, fin_smul]
  have ha' : cZ p Z hZ ≤ fin p a := ha
  have hb' : cZ p Z hZ ≤ fin p 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 p Z hZ = cZ p Z hZ := by rw [hst, one_mul]
  linarith

end Cone

/-! ### Trees -/

section Tree

theorem size_node {α : Type} (a : α) (cs : List (RTree α)) :
    size (.node a cs) = 1 + sizeAll cs := by rw [size]

theorem sizeAll_cons {α : Type} (c : RTree α) (cs : List (RTree α)) :
    sizeAll (c :: cs) = size c + sizeAll cs := by rw [sizeAll]

theorem sizeAll_append {α : Type} (l₁ l₂ : List (RTree α)) :
    sizeAll (l₁ ++ l₂) = sizeAll l₁ + sizeAll l₂ := by
  induction l₁ with
  | nil => simp [sizeAll]
  | cons c l ih => rw [List.cons_append, sizeAll_cons, sizeAll_cons, ih]; ring

theorem nuSum_node (ν ν' : ℕ) (cs : List (RTree (ℕ × ℕ))) :
    nuSum (.node (ν, ν') cs) = ν + nuSumAll cs := by rw [nuSum]

theorem nuSumAll_cons (c : RTree (ℕ × ℕ)) (cs : List (RTree (ℕ × ℕ))) :
    nuSumAll (c :: cs) = nuSum c + nuSumAll cs := by rw [nuSumAll]

theorem nuSumAll_append (l₁ l₂ : List (RTree (ℕ × ℕ))) :
    nuSumAll (l₁ ++ l₂) = nuSumAll l₁ + nuSumAll l₂ := by
  induction l₁ with
  | nil => simp [nuSumAll]
  | cons c l ih => rw [List.cons_append, nuSumAll_cons, nuSumAll_cons, ih]; ring

theorem size_le_of_mem {α : Type} {c : RTree α} {cs : List (RTree α)} (h : c ∈ cs) :
    size c ≤ sizeAll cs := by
  induction cs with
  | nil => simp at h
  | cons c' l ih =>
    rw [sizeAll_cons]
    rcases List.mem_cons.1 h with rfl | h
    · omega
    · have := ih h; omega

/-- Induction over `RTree`, with the hypothesis for all children. -/
theorem RTree.ind {α : Type} (P : RTree α → Prop)
    (h : ∀ a cs, (∀ c ∈ cs, P c) → P (.node a cs)) : ∀ t, P t := by
  intro t
  induction hn : size t using Nat.strong_induction_on generalizing t with
  | _ n ih =>
    cases t with
    | node a cs =>
      apply h
      intro c hc
      have := size_le_of_mem hc
      rw [size_node] at hn
      exact ih _ (by omega) c rfl

theorem AdmAll_iff (L : ℕ → ℕ → Prop) (cs : List (RTree (ℕ × ℕ))) :
    AdmAll L cs ↔ ∀ c ∈ cs, AdmAt L true c := by
  induction cs with
  | nil => simp [AdmAll]
  | cons c l ih => rw [AdmAll, ih, List.forall_mem_cons]

variable {p y : ℝ}

theorem message_node (ν ν' : ℕ) (cs : List (RTree (ℕ × ℕ))) :
    message p y (.node (ν, ν') cs) = mergeAll p y (init p y ν ν') cs := by rw [message]

theorem mergeAll_nil (P : Fin 8 → ℝ) : mergeAll p y P [] = P := by rw [mergeAll]

theorem mergeAll_cons (P : Fin 8 → ℝ) (c : RTree (ℕ × ℕ)) (cs : List (RTree (ℕ × ℕ))) :
    mergeAll p y P (c :: cs) = mergeAll p y (merge p P (message p y c)) cs := by rw [mergeAll]

theorem mergeAll_append (P : Fin 8 → ℝ) (l₁ l₂ : List (RTree (ℕ × ℕ))) :
    mergeAll p y P (l₁ ++ l₂) = mergeAll p y (mergeAll p y P l₁) l₂ := by
  induction l₁ generalizing P with
  | nil => rw [List.nil_append, mergeAll_nil]
  | cons c l ih => rw [List.cons_append, mergeAll_cons, mergeAll_cons, ih]

theorem init_nonneg (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hy : 0 ≤ y) (ν ν' : ℕ) :
    0 ≤ init p y ν ν' := by
  have hq : 0 ≤ 1 - p := by linarith
  intro i
  fin_cases i <;> simp [init] <;> positivity

theorem message_nonneg (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hy : 0 ≤ y) :
    ∀ t, 0 ≤ message p y t := by
  refine RTree.ind _ ?_
  rintro ⟨ν, ν'⟩ cs ih
  rw [message_node]
  have key : ∀ (l : List (RTree (ℕ × ℕ))), (∀ c ∈ l, 0 ≤ message p y c) →
      ∀ P, 0 ≤ P → 0 ≤ mergeAll p y P l := by
    intro l
    induction l with
    | nil => intro _ P hP; rwa [mergeAll_nil]
    | cons c l ihl =>
      intro hl P hP
      rw [mergeAll_cons]
      exact ihl (fun c' hc' => hl c' (List.mem_cons_of_mem _ hc')) _
        (merge_nonneg hp1 hP (hl c (List.mem_cons_self ..)))
  exact key cs ih _ (init_nonneg hp0 hp1 hy ν ν')

end Tree

/-! ### `lem:rsc-cert` -/

section Certificate

variable {p y : ℝ}

theorem mem_smul_PZ_iff {Z : Finset (Fin 8 → ℝ)} {η : ℝ} (hη : 0 < η) {P : Fin 8 → ℝ} :
    P ∈ η • PZ Z ↔ η⁻¹ • P ∈ PZ Z := by
  constructor
  · rintro ⟨w, hw, rfl⟩; rwa [smul_smul, inv_mul_cancel₀ hη.ne', one_smul]
  · intro h; exact ⟨_, h, by show η • (η⁻¹ • P) = P; rw [smul_smul, mul_inv_cancel₀ hη.ne', one_smul]⟩

/-- Step 1 along a list of children. -/
theorem mergeAll_mem (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Z : Finset (Fin 8 → ℝ)}
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p z z' ∈ PZ Z) {ê : ℝ} (hê : 0 < ê) :
    ∀ (cs : List (RTree (ℕ × ℕ))) (P : Fin 8 → ℝ) (η : ℝ), 0 < η → P ∈ η • PZ Z →
      (∀ c ∈ cs, message p y c ∈ ê ^ (size c + nuSum c) • PZ Z ∧ 0 ≤ message p y c) →
      mergeAll p y P cs ∈ (η * ê ^ (sizeAll cs + nuSumAll cs)) • PZ Z := by
  intro cs
  induction cs with
  | nil => intro P η _ hP _; simpa [mergeAll_nil, sizeAll, nuSumAll] using hP
  | cons c l ih =>
    intro P η hη hP hl
    rw [mergeAll_cons]
    have hc := hl c (List.mem_cons_self ..)
    have := ih _ _ (mul_pos hη (pow_pos hê _))
      (merge_mem_smul_PZ hp0 hp1 hZ0 C1 hη (pow_pos hê _) hP hc.1 hc.2)
      (fun c' hc' => hl c' (List.mem_cons_of_mem _ hc'))
    convert this using 2
    rw [sizeAll_cons, nuSumAll_cons, mul_assoc, ← pow_add]
    ring_nf

/-- Step 3: the first `j` merges of a vertex with few owned vertices, through `Y₀, …, Y_j`. -/
theorem chain (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    {ê : ℝ} (hê : 0 < ê) (Ys : ℕ → Finset (Fin 8 → ℝ)) (j : ℕ) (hYj : Ys j = Z)
    (hYnn : ∀ i < j, ∀ x ∈ Ys i, 0 ≤ x)
    (hY : ∀ i, 1 ≤ i → i ≤ j → ∀ x ∈ Ys (i - 1), ∀ z ∈ Z,
      merge p x z ∈ convexHull ℝ (Ys i : Set _) + Kpos) :
    ∀ (n i : ℕ) (cs : List (RTree (ℕ × ℕ))) (P : Fin 8 → ℝ) (σ : ℝ), i + n = j →
      n ≤ cs.length → 0 < σ → σ⁻¹ • P ∈ convexHull ℝ (Ys i : Set _) + Kpos →
      (∀ c ∈ cs, message p y c ∈ ê ^ (size c + nuSum c) • PZ Z ∧ 0 ≤ message p y c) →
      mergeAll p y P (cs.take n)
        ∈ (σ * ê ^ (sizeAll (cs.take n) + nuSumAll (cs.take n))) • PZ Z := by
  intro n
  induction n with
  | zero =>
    intro i cs P σ hi _ hσ hP _
    simp only [List.take_zero, mergeAll_nil, sizeAll, nuSumAll, add_zero, pow_zero, mul_one]
    rw [mem_smul_PZ_iff hσ, PZ, ← hYj, ← hi, add_zero]
    exact hP
  | succ n ih =>
    intro i cs P σ hi hlen hσ hP hcs
    obtain ⟨c, cs', rfl⟩ : ∃ c cs', cs = c :: cs' := by
      cases cs with
      | nil => simp at hlen
      | cons c cs' => exact ⟨c, cs', rfl⟩
    have hc := hcs c (List.mem_cons_self ..)
    set η := ê ^ (size c + nuSum c) with hη
    have hηpos : 0 < η := pow_pos hê _
    rw [List.take_succ_cons, mergeAll_cons]
    have hstep : (σ * η)⁻¹ • merge p P (message p y c)
        ∈ convexHull ℝ (Ys (i + 1) : Set _) + Kpos := by
      rw [show (σ * η)⁻¹ • merge p P (message p y c)
          = merge p (σ⁻¹ • P) (η⁻¹ • message p y c) by
        rw [merge_smul_left, merge_smul_right, smul_smul, mul_inv]]
      refine merge_hull hp0 hp1 (hYnn i (by omega)) hZ0 ?_ hP ((mem_smul_PZ_iff hηpos).1 hc.1)
        (smul_nonneg (inv_nonneg.2 hηpos.le) hc.2)
      have := hY (i + 1) (by omega) (by omega)
      simpa using this
    have := ih (i + 1) cs' _ (σ * η) (by omega) (by simp at hlen; omega) (mul_pos hσ hηpos)
      hstep (fun c' hc' => hcs c' (List.mem_cons_of_mem _ hc'))
    convert this using 2
    rw [sizeAll_cons, nuSumAll_cons, hη, mul_assoc, ← pow_add]
    ring_nf

/-- Step 2 of `lem:rsc-cert`: the initial message of a vertex that needs no Step 3. -/
theorem init_mem (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hy : 0 ≤ y) {ê : ℝ} (hê : 0 < ê)
    (hêq : ê < 1 - p) {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) (ν₀ νE : ℕ)
    (dmin : ℕ → ℕ)
    (C2 : (∀ ν ≤ ν₀, init p y ν 0 ∈ ê ^ (1 + ν) • PZ Z) ∧ initInf p y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C4 : ∀ ν, 1 ≤ ν → ν ≤ νE → dmin ν ≤ 1 → ex p (ν - 1) (init p y ν 0) ∈ ê ^ (1 + ν) • PZ Z)
    (C6 : ((1 - p) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    {ν ν' : ℕ} (hνν : ν' ≤ ν)
    (hcase : ν' = 0 ∨ νE < ν ∨ (1 ≤ ν ∧ ν ≤ νE ∧ dmin ν ≤ 1 ∧ ν' ≤ ν - 1)) :
    init p y ν ν' ∈ ê ^ (1 + ν) • PZ Z := by
  have hq : 0 ≤ 1 - p := by linarith
  have hq1 : 1 - p ≤ 1 := by linarith
  have hê1 : ê ≤ 1 := by linarith
  rcases hcase with rfl | hνE | ⟨h1, h2, h3, h4⟩
  · by_cases hν : ν ≤ ν₀
    · exact C2.1 ν hν
    · have hsplit : init p y ν 0 = initInf p y + ![0, 0, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0] := by
        funext i; fin_cases i <;> simp [init, initInf]
      rw [hsplit]
      refine smul_PZ_mono hZ0 (pow_pos hê _) ?_
        (smul_PZ_add_Kpos (pow_pos hê _) C2.2 (Kpos_of_nonneg ?_))
      · exact pow_le_pow_of_le_one hê.le hê1 (by omega)
      · intro i; fin_cases i <;> simp
  · have hpow : (1 - p) ^ ν ≤ (1 - p) ^ ν' := pow_le_pow_of_le_one hq hq1 hνν
    have hqpos : 0 < (1 - p) ^ ν := pow_pos (by linarith) _
    have hsplit : init p y ν ν' = (1 - p) ^ ν • initInf p y
        + ![((1 - p) ^ ν' - (1 - p) ^ ν) * y / 2, ((1 - p) ^ ν' - (1 - p) ^ ν) * p / 2, 0, 0,
            (1/2 : ℝ) ^ ν, 0, 0, 0] := by
      funext i; fin_cases i <;> simp [init, initInf] <;> ring
    have hInf : (1 - p) ^ ν • initInf p y ∈ ((1 - p) ^ ν * ê ^ (ν₀ + 2)) • PZ Z := by
      obtain ⟨w, hw, hw'⟩ := C2.2
      refine ⟨w, hw, ?_⟩
      show ((1 - p) ^ ν * ê ^ (ν₀ + 2)) • w = (1 - p) ^ ν • initInf p y
      rw [← hw']
      show ((1 - p) ^ ν * ê ^ (ν₀ + 2)) • w = (1 - p) ^ ν • (ê ^ (ν₀ + 2) • w)
      rw [smul_smul]
    have hscale : ê ^ (1 + ν) ≤ (1 - p) ^ ν * ê ^ (ν₀ + 2) := by
      have hr : 1 ≤ (1 - p) / ê := by rw [le_div_iff₀ hê]; linarith
      have h1 : ((1 - p) / ê) ^ (νE + 1) ≤ ((1 - p) / ê) ^ ν := pow_le_pow_right₀ hr (by omega)
      have h2 : ê⁻¹ ^ (ν₀ + 1) ≤ ((1 - p) / ê) ^ ν := C6.le.trans h1
      rw [div_pow, inv_pow, le_div_iff₀ (pow_pos hê _)] at h2
      have hB : 0 < ê ^ (ν₀ + 1) := pow_pos hê _
      have h3 : ê ^ ν ≤ (1 - p) ^ ν * ê ^ (ν₀ + 1) := by
        have := mul_le_mul_of_nonneg_left h2 hB.le
        rwa [← mul_assoc, mul_inv_cancel₀ hB.ne', one_mul, mul_comm (ê ^ (ν₀ + 1))] at this
      calc ê ^ (1 + ν) = ê * ê ^ ν := by ring
        _ ≤ ê * ((1 - p) ^ ν * ê ^ (ν₀ + 1)) := mul_le_mul_of_nonneg_left h3 hê.le
        _ = (1 - p) ^ ν * ê ^ (ν₀ + 2) := by ring
    rw [hsplit]
    refine smul_PZ_mono hZ0 (pow_pos hê _) hscale
      (smul_PZ_add_Kpos (by positivity) hInf (Kpos_of_nonneg ?_))
    have e1 := mul_nonneg (sub_nonneg.2 hpow) hy
    have e2 := mul_nonneg (sub_nonneg.2 hpow) hp0
    intro i; fin_cases i <;> simp <;> positivity
  · have hpow : (1 - p) ^ (ν - 1) ≤ (1 - p) ^ ν' := pow_le_pow_of_le_one hq hq1 h4
    have hsplit : init p y ν ν' = ex p (ν - 1) (init p y ν 0)
        + ![((1 - p) ^ ν' - (1 - p) ^ (ν - 1)) * y / 2,
            ((1 - p) ^ ν' - (1 - p) ^ (ν - 1)) * p / 2, 0, 0, 0, 0, 0, 0] := by
      funext i; fin_cases i <;> simp [init, ex] <;> ring
    rw [hsplit]
    refine smul_PZ_add_Kpos (pow_pos hê _) (C4 ν h1 h2 h3) (Kpos_of_nonneg ?_)
    have e1 := mul_nonneg (sub_nonneg.2 hpow) hy
    have e2 := mul_nonneg (sub_nonneg.2 hpow) hp0
    intro i; fin_cases i <;> simp <;> positivity

/-- Steps 1–4 of `lem:rsc-cert`, for an arbitrary lightness predicate `L`: every message of an
`L`-admissible tree lies in `ê ^ (size + Σ ν) • 𝒫_Z`. -/
theorem message_mem (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hy : 0 ≤ y) {ê : ℝ} (hê : 0 < ê)
    (hêq : ê < 1 - p) {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) (L : ℕ → ℕ → Prop)
    (ν₀ νE : ℕ) (dmin : ℕ → ℕ)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p y ν 0 ∈ ê ^ (1 + ν) • PZ Z) ∧ initInf p y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ d, 1 ≤ d → d < dmin ν → L ν d)
    (C4 : ∀ ν, 1 ≤ ν → ν ≤ νE → dmin ν ≤ 1 → ex p (ν - 1) (init p y ν 0) ∈ ê ^ (1 + ν) • PZ Z)
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∃ Ys : ℕ → Finset (Fin 8 → ℝ),
      let j := max 1 (dmin ν - 1)
      Ys 0 = {(ê ^ (1 + ν))⁻¹ • ex p ν (init p y ν 0)} ∧ Ys j = Z ∧
      (∀ i < j, ∀ x ∈ Ys i, 0 ≤ x) ∧
      ∀ i, 1 ≤ i → i ≤ j → ∀ x ∈ Ys (i - 1), ∀ z ∈ Z,
        merge p x z ∈ convexHull ℝ (Ys i : Set _) + Kpos)
    (C6 : ((1 - p) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1)) :
    ∀ t (b : Bool), AdmAt L b t → message p y t ∈ ê ^ (size t + nuSum t) • PZ Z := by
  have hq : 0 ≤ 1 - p := by linarith
  have hq1 : 1 - p ≤ 1 := by linarith
  refine RTree.ind _ ?_
  rintro ⟨ν, ν'⟩ cs ih b hadm
  rw [AdmAt] at hadm
  obtain ⟨⟨hνν, hL, h1⟩, hcs⟩ := hadm
  rw [AdmAll_iff] at hcs
  have hch : ∀ c ∈ cs, message p y c ∈ ê ^ (size c + nuSum c) • PZ Z ∧ 0 ≤ message p y c :=
    fun c hc => ⟨ih c hc true (hcs c hc), message_nonneg hp0 hp1 hy c⟩
  rw [message_node, size_node, nuSum_node]
  set d := cs.length + (if b then 1 else 0) with hd
  by_cases hcase : ν' = 0 ∨ νE < ν ∨ (1 ≤ ν ∧ ν ≤ νE ∧ dmin ν ≤ 1 ∧ ν' ≤ ν - 1)
  · have hi := init_mem hp0 hp1 hy hê hêq hZ0 ν₀ νE dmin C2 C4 C6 hνν hcase
    have := mergeAll_mem hp0 hp1 hZ0 C1 hê cs _ _ (pow_pos hê _) hi hch
    convert this using 2
    rw [← pow_add]; congr 1; ring
  · have hν'0 : ν' ≠ 0 := fun h => hcase (Or.inl h)
    have hννE : ν ≤ νE := by
      by_contra h; exact hcase (Or.inr (Or.inl (by omega)))
    have hν1 : 1 ≤ ν := by omega
    have hnot : ¬ (dmin ν ≤ 1 ∧ ν' ≤ ν - 1) :=
      fun h => hcase (Or.inr (Or.inr ⟨hν1, hννE, h.1, h.2⟩))
    have hnL : ¬ L ν d := fun h => hν'0 (hL (Or.inl h))
    have hd0 : d ≠ 0 := fun h => hν'0 (hL (Or.inr h))
    have hdmin : dmin ν ≤ d := by
      by_contra hlt
      exact hnL (C3 ν hν1 hννE d (by omega) (by omega))
    have hd2 : 2 ≤ d := by
      by_contra h2
      have hd1 : d = 1 := by omega
      have := h1 ⟨hd1, by omega⟩
      have : 1 < dmin ν := by
        by_contra h; exact hnot ⟨by omega, this⟩
      omega
    have hlen : d ≤ cs.length + 1 := by rw [hd]; split <;> omega
    obtain ⟨Ys, hYs⟩ := C5 ν hν1 hννE
    dsimp only at hYs
    obtain ⟨hY0, hYj, hYnn, hYstep⟩ := hYs
    set j := max 1 (dmin ν - 1) with hj
    have hjlen : j ≤ cs.length := by omega
    set σ := ê ^ (1 + ν) with hσ
    have hσpos : 0 < σ := pow_pos hê _
    have hpow : (1 - p) ^ ν ≤ (1 - p) ^ ν' := pow_le_pow_of_le_one hq hq1 hνν
    have hsplit : init p y ν ν' = ex p ν (init p y ν 0)
        + ![((1 - p) ^ ν' - (1 - p) ^ ν) * y / 2,
            ((1 - p) ^ ν' - (1 - p) ^ ν) * p / 2, 0, 0, 0, 0, 0, 0] := by
      funext i; fin_cases i <;> simp [init, ex] <;> ring
    have hD : (0 : Fin 8 → ℝ) ≤ ![((1 - p) ^ ν' - (1 - p) ^ ν) * y / 2,
        ((1 - p) ^ ν' - (1 - p) ^ ν) * p / 2, 0, 0, 0, 0, 0, 0] := by
      have e1 := mul_nonneg (sub_nonneg.2 hpow) hy
      have e2 := mul_nonneg (sub_nonneg.2 hpow) hp0
      intro i; fin_cases i <;> simp <;> positivity
    have hP : σ⁻¹ • init p y ν ν' ∈ convexHull ℝ (Ys 0 : Set _) + Kpos := by
      rw [hsplit, smul_add]
      refine Set.add_mem_add (subset_convexHull ℝ _ ?_)
        (Kpos_of_nonneg (smul_nonneg (inv_nonneg.2 hσpos.le) hD))
      rw [hY0]; simp
    have htake := chain hp0 hp1 hZ0 hê Ys j hYj hYnn hYstep j 0 cs _ σ (by omega) hjlen hσpos
      hP hch
    have hdrop := mergeAll_mem hp0 hp1 hZ0 C1 hê (cs.drop j) _ _ (by positivity) htake
      (fun c hc => hch c (List.mem_of_mem_drop hc))
    have e1 : mergeAll p y (init p y ν ν') cs
        = mergeAll p y (mergeAll p y (init p y ν ν') (cs.take j)) (cs.drop j) := by
      rw [← mergeAll_append, List.take_append_drop]
    have e2 : sizeAll cs = sizeAll (cs.take j) + sizeAll (cs.drop j) := by
      rw [← sizeAll_append, List.take_append_drop]
    have e3 : nuSumAll cs = nuSumAll (cs.take j) + nuSumAll (cs.drop j) := by
      rw [← nuSumAll_append, List.take_append_drop]
    rw [e1]
    convert hdrop using 2
    rw [e2, e3, hσ, ← pow_add, ← pow_add]; congr 1; ring

/-- `lem:rsc-cert` for an arbitrary lightness predicate `L`. -/
theorem certificate_conditions_of (p y ê : ℝ) (hp : 0 < p ∧ p < 1/2) (hy : 0 < y)
    (hê : 0 < ê ∧ ê < 1 - p)
    (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (L : ℕ → ℕ → Prop) (ν₀ νE : ℕ) (dmin : ℕ → ℕ)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p y ν 0 ∈ ê ^ (1 + ν) • PZ Z) ∧ initInf p y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ d, 1 ≤ d → d < dmin ν → L ν d)
    (C4 : ∀ ν, 1 ≤ ν → ν ≤ νE → dmin ν ≤ 1 → ex p (ν - 1) (init p y ν 0) ∈ ê ^ (1 + ν) • PZ Z)
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∃ Ys : ℕ → Finset (Fin 8 → ℝ),
            let j := max 1 (dmin ν - 1)
            Ys 0 = {(ê ^ (1 + ν))⁻¹ • ex p ν (init p y ν 0)} ∧ Ys j = Z ∧
            (∀ i < j, ∀ x ∈ Ys i, 0 ≤ x) ∧
            ∀ i, 1 ≤ i → i ≤ j → ∀ x ∈ Ys (i - 1), ∀ z ∈ Z,
              merge p x z ∈ convexHull ℝ (Ys i : Set _) + Kpos)
    (C6 : ((1 - p) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    (t : RTree (ℕ × ℕ)) (ht : AdmAt L false t) :
    cZ p Z hZ * ê ^ (size t + nuSum t) ≤ fin p (message p y t) := by
  have hp0 : 0 ≤ p := hp.1.le
  have hp1 : p ≤ 1 := by linarith [hp.2]
  have hm := message_mem hp0 hp1 hy.le hê.1 hê.2 hZ0 L ν₀ νE dmin C1 C2 C3 C4 C5 C6 t false ht
  obtain ⟨w, ⟨a, ha, k, hk, rfl⟩, hw⟩ := hm
  have hw' : message p y t = ê ^ (size t + nuSum t) • (a + k) := hw.symm
  rw [hw', fin_smul, fin_add, mul_comm]
  have hη : 0 ≤ ê ^ (size t + nuSum t) := pow_nonneg hê.1.le _
  have := cZ_le_fin (p := p) hZ ha
  have := fin_nonneg_of_Kpos hp0 hp1 hk
  nlinarith

/-- `lem:rsc-cert`. -/
theorem certificate_conditions (p y ê : ℝ) (hp : 0 < p ∧ p < 1/2) (hy : 0 < y)
    (hê : 0 < ê ∧ ê < 1 - p)
    (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z) (hc : 0 < cZ p Z hZ)
    (ν₀ νE : ℕ) (hνE : 1 ≤ νE) (dmin : ℕ → ℕ) (hdmin : ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ dmin ν)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p y ν 0 ∈ ê ^ (1 + ν) • PZ Z) ∧ initInf p y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ d, 1 ≤ d → d < dmin ν → Light p y ν d)
    (C4 : ∀ ν, 1 ≤ ν → ν ≤ νE → dmin ν ≤ 1 → ex p (ν - 1) (init p y ν 0) ∈ ê ^ (1 + ν) • PZ Z)
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∃ Ys : ℕ → Finset (Fin 8 → ℝ),
            let j := max 1 (dmin ν - 1)
            Ys 0 = {(ê ^ (1 + ν))⁻¹ • ex p ν (init p y ν 0)} ∧ Ys j = Z ∧
            (∀ i < j, ∀ x ∈ Ys i, 0 ≤ x) ∧
            ∀ i, 1 ≤ i → i ≤ j → ∀ x ∈ Ys (i - 1), ∀ z ∈ Z,
              merge p x z ∈ convexHull ℝ (Ys i : Set _) + Kpos)
    (C6 : ((1 - p) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    (t : RTree (ℕ × ℕ)) (ht : Admissible p y t) :
    cZ p Z hZ * ê ^ (size t + nuSum t) ≤ fin p (message p y t) :=
  certificate_conditions_of p y ê hp hy hê Z hZ hZ0 (Light p y) ν₀ νE dmin C1 C2 C3 C4 C5 C6 t ht

end Certificate

end

end MaxLeafFormal.Antinorm8