MaxLeafFormal.RSCCert

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

Statements of the paper formalised here: Lemma D.5.19, Lemma D.5.20.

import Mathlib
import MaxLeafFormal.Antinorm8

/-!
# The graded RSC certificate lemma

Transcribes the graded eight-state relaxation of the paper (the merge `∘̃`, `Init~`,
lightness, admissibility with typed exposures) and proves `lem:rsc-cone`, `lem:rsc-cert` (for the
root relaxed message, every root and every order of the children) and the staged-chain criterion
for (C5). The order, `𝒦_pos`, `𝒫_Z`, `fin`, `c_Z` and the tree type are reused from
`MaxLeafFormal.Antinorm8`, which is imported and not edited.
-/

namespace MaxLeafFormal.RSCCert

open Finset Pointwise
-- Reused unchanged from Antinorm8 (selective open, to avoid clashes with the new `merge`, `init`, …):
open MaxLeafFormal.Antinorm8 (RTree size sizeAll Kpos PZ fin cZ initInf chiCs chiCu chiOs chiOx
  chiOu covers below IsUpSet below_of_covers mono_below func_nonneg Kpos_of_nonneg Kpos_add
  Kpos_smul sum_upset indicator_mono fin_add fin_smul fin_nonneg_of_Kpos convexHull_nonneg
  convex_hullKpos hullKpos_add smul_PZ_add_Kpos smul_PZ_mono cZ_le_fin size_node sizeAll_cons
  sizeAll_append size_le_of_mem mem_smul_PZ_iff)

noncomputable section
-- indices 0..7 = A, C₀, C₁, C₂, O₀₀, O₀₁, O₁, O₂

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

/-- The eight-state merge P ∘̃ Q. -/
def merge (p₂ p₃ : ℝ) (P Q : Fin 8 → ℝ) : Fin 8 → ℝ :=
  ![P 0 * chiS p₂ 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]

/-- Init~(ν; c₂, c₃). -/
def init (p₂ p₃ y ϖ₂ ϖ₃ : ℝ) (ν c₂ c₃ : ℕ) : Fin 8 → ℝ :=
  ![(1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * (y / 2), (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * (p₂ / 2), 0, 0,
    (1/2 : ℝ) ^ ν * ϖ₂ ^ c₂ * ϖ₃ ^ c₃, 0, 0, 0]

/-- ε, δ, 𝖻, lightness (def:rsc-light). -/
def eps (p : ℝ) : ℝ := -Real.log (1 - p)

def delta₂ : ℝ := Real.log 2

def delta₃ (p₃ : ℝ) : ℝ := Real.log (2 * (1 - p₃))

def bconst (p₂ p₃ y : ℝ) : ℝ := 2 + 2 * max p₂ (p₃ - p₂) / y

def Light₃ (p₂ p₃ y : ℝ) (ν d : ℕ) : Prop :=
  (1/2 : ℝ) ^ ν * (bconst p₂ p₃ y ^ d)⁻¹ ≥ (1 + p₃ / y) * (eps p₃ * y / delta₃ p₃)

def Light₂ (p₂ p₃ y : ℝ) (ν d : ℕ) : Prop :=
  (1/2 : ℝ) ^ ν * (bconst p₂ p₃ y ^ d)⁻¹ ≥ eps p₂ * y / delta₂

/-- θ, ρ₁ and eq:rsc-credits. -/
def rho₁ (p₃ y : ℝ) : ℝ := (1 + y / 2 * (1 - p₃))⁻¹

def Credits (p₃ y ϖ₂ ϖ₃ : ℝ) : Prop :=
  Real.log ϖ₂ ≤ (1 - rho₁ p₃ y) * delta₂ ∧ Real.log ϖ₃ ≤ (1 - rho₁ p₃ y ^ 2) * delta₃ p₃

/-- Labels (ν_v, c_{v,2}, c_{v,3}). -/
abbrev Label := ℕ × ℕ × ℕ

mutual

/-- Relaxed message M̃_v: children merged left to right, no forcing. -/
def message (p₂ p₃ y ϖ₂ ϖ₃ : ℝ) : RTree Label → Fin 8 → ℝ
  | .node (ν, c₂, c₃) cs => mergeAll p₂ p₃ y ϖ₂ ϖ₃ (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) cs

def mergeAll (p₂ p₃ y ϖ₂ ϖ₃ : ℝ) : (Fin 8 → ℝ) → List (RTree Label) → Fin 8 → ℝ
  | P, [] => P
  | P, c :: cs => mergeAll p₂ p₃ y ϖ₂ ϖ₃ (merge p₂ p₃ P (message p₂ p₃ y ϖ₂ ϖ₃ c)) cs
end

/-- d_F(v) of a node with children `cs`; `hasParent = false` only at the root. -/
def deg (hasParent : Bool) (cs : List (RTree Label)) : ℕ :=
  cs.length + if hasParent then 1 else 0

mutual

/-- def:rsc-admissible at every node, for lightness predicates L₂, L₃. -/
def AdmAt (L₂ L₃ : ℕ → ℕ → Prop) : Bool → RTree Label → Prop
  | b, .node (ν, c₂, c₃) cs =>
    (c₂ + c₃ ≤ ν ∧
      ((L₂ ν (deg b cs) ∨ deg b cs = 0) → c₂ = 0) ∧
      ((L₃ ν (deg b cs) ∨ deg b cs = 0) → c₃ = 0) ∧
      ((deg b cs = 1 ∧ 1 ≤ c₂ + c₃) → c₂ + c₃ ≤ ν - 1)) ∧ AdmAll L₂ L₃ cs

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

def Admissible (p₂ p₃ y : ℝ) (t : RTree Label) : Prop :=
  AdmAt (Light₂ p₂ p₃ y) (Light₃ p₂ p₃ y) false t

mutual

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

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

/-- j_τ(ν) = max(1, d_min^(τ)(ν) − 1). -/
def jOf (dmin : ℕ → ℕ) (ν : ℕ) : ℕ := max 1 (dmin ν - 1)

/-- e_x and the 14 generators of lem:rsc-cone (a): the unit vectors, then e_{x'} − e_x for
C₂≻C₁, C₁≻C₀, C₂≻O₀₁, O₀₁≻O₀₀, O₀₁≻O₁, O₁≻O₂. -/
def unitVec (x : Fin 8) : Fin 8 → ℝ := Pi.single x 1

def gen : Fin 14 → Fin 8 → ℝ :=
  ![unitVec 0, unitVec 1, unitVec 2, unitVec 3, unitVec 4, unitVec 5, unitVec 6, unitVec 7,
    unitVec 3 - unitVec 2, unitVec 2 - unitVec 1, unitVec 3 - unitVec 5,
    unitVec 5 - unitVec 4, unitVec 5 - unitVec 6, unitVec 6 - unitVec 7]

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

section Algebra

variable {p₂ p₃ : ℝ}

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

theorem merge_add_right (P Q Q' : Fin 8 → ℝ) :
    merge p₂ p₃ P (Q + Q') = merge p₂ p₃ P Q + merge p₂ 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₂ p₃ (a • P) Q = a • merge p₂ p₃ P Q := by
  funext i; fin_cases i <;> simp [merge] <;> ring

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

theorem chiS_nonneg (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {Q : Fin 8 → ℝ} (hQ : 0 ≤ Q) :
    0 ≤ chiS p₂ p₃ Q := by
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  have hlam : 0 ≤ p₃ / p₂ := div_nonneg (by linarith) hp.1.le
  have h6 := mul_nonneg (by linarith : (0 : ℝ) ≤ 1 - p₂) (g 6)
  have h7 := mul_nonneg (by linarith : (0 : ℝ) ≤ 1 - p₃) (g 7)
  have h3 := mul_nonneg (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hlam) (g 3)
  simp only [chiS]; linarith [g 0, g 2, g 4, g 5]

theorem merge_nonneg (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {P Q : Fin 8 → ℝ} (hP : 0 ≤ P)
    (hQ : 0 ≤ Q) : 0 ≤ merge p₂ p₃ P Q := by
  have hq : 0 ≤ 1 - p₂ := by linarith
  have hS := chiS_nonneg hp hQ
  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 only [merge, chiCs, chiCu, chiOs, chiOx, chiOu] <;> simp <;>
    repeat (first | exact hS | exact h _ | exact g _ | exact hq | apply add_nonneg |
      apply mul_nonneg | apply div_nonneg | norm_num)

/-- For `p₂ = p₃ = p` the graded merge is `Antinorm8.merge p`. -/
theorem merge_eq_antinorm8 {p : ℝ} (hp : p ≠ 0) : merge p p = Antinorm8.merge p := by
  funext P Q i
  fin_cases i <;> simp [merge, Antinorm8.merge, chiS, Antinorm8.chiS, div_self hp] <;> (try ring_nf) <;> simp

end Algebra

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

section Cone

variable {p₂ p₃ : ℝ}

/-- The dual functional `w'` with `w(Δ ∘̃ Q) = w'(Δ)` (proof of `lem:rsc-cone` (b)). -/
def dualL (p₂ p₃ : ℝ) (Q w : Fin 8 → ℝ) : Fin 8 → ℝ :=
  ![chiS p₂ 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₂ p₃ Δ Q x = ∑ x, dualL p₂ 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 (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {Δ Q : Fin 8 → ℝ} (hΔ : Δ ∈ Kpos)
    (hQ : 0 ≤ Q) : merge p₂ 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₂ p₃ Q := chiS_nonneg hp hQ
  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 ∘̃ Δ`. The only new coefficient vector is
`χ̃_S = (2, 0, 2, 2λ, 1, 1, q₂, q₃)`, monotone along the covers since `λ ≥ 1`, `q₃ ≤ q₂ ≤ 1`. -/
theorem merge_Kpos_right (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {Q Δ : Fin 8 → ℝ} (hQ : 0 ≤ Q)
    (hΔ : Δ ∈ Kpos) : merge p₂ p₃ Q Δ ∈ Kpos := by
  have hq : 0 ≤ 1 - p₂ := by linarith
  have hq3 : 0 ≤ 1 - p₃ := by linarith
  have hlam : 1 ≤ p₃ / p₂ := by rw [le_div_iff₀ hp.1]; linarith
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  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₂ p₃ Δ := by
    have := F ![2, 0, 2, 2 * (p₃ / p₂), 1, 1, 1 - p₂, 1 - p₃]
      (nn _ _ _ _ _ _ _ _ (by norm_num) le_rfl (by norm_num) (by linarith) (by norm_num)
        (by norm_num) hq hq3) (by simp; linarith) (by simp) (by simp; linarith) (by simp)
      (by simp; linarith) (by simp; linarith)
    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
  set M := merge p₂ 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)))

theorem c1_unitVec_nonneg (x : Fin 8) : 0 ≤ unitVec x := by
  intro j
  simp only [unitVec, Pi.single_apply]
  split_ifs <;> norm_num

theorem c1_sum_unitVec (U : Finset (Fin 8)) (x : Fin 8) :
    ∑ i ∈ U, unitVec x i = if x ∈ U then 1 else 0 := by
  simp [unitVec, Pi.single_apply, Finset.sum_ite_eq']

theorem c1_gen_diff_mem {x x' : Fin 8} (h : covers x x') : unitVec x' - unitVec x ∈ Kpos := by
  intro U hU
  have hx : x ∈ U → x' ∈ U := fun hxU => hU x x' (below_of_covers h) hxU
  simp only [Pi.sub_apply, Finset.sum_sub_distrib, c1_sum_unitVec]
  by_cases h1 : x ∈ U
  · have h2 := hx h1
    simp [h1, h2]
  · by_cases h2 : x' ∈ U <;> simp [h1, h2]

theorem Kpos_isClosed : IsClosed Kpos := by
  have h : Kpos = ⋂ (U : Finset (Fin 8)), ⋂ (_ : IsUpSet U),
      {P : Fin 8 → ℝ | 0 ≤ ∑ i ∈ U, P i} := by
    ext P; simp [Kpos]
  rw [h]
  refine isClosed_iInter (fun U => isClosed_iInter (fun hU => isClosed_le continuous_const ?_))
  fun_prop

theorem Kpos_convex : Convex ℝ Kpos :=
  fun P hP Q hQ a b ha hb _ => Kpos_add (Kpos_smul ha hP) (Kpos_smul hb hQ)

theorem gen_mem_Kpos (i : Fin 14) : gen i ∈ Kpos := by
  fin_cases i
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 0)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 1)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 2)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 3)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 4)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 5)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 6)
  · exact Kpos_of_nonneg (c1_unitVec_nonneg 7)
  · exact c1_gen_diff_mem (Or.inl ⟨rfl, rfl⟩)
  · exact c1_gen_diff_mem (Or.inr (Or.inl ⟨rfl, rfl⟩))
  · exact c1_gen_diff_mem (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩)))
  · exact c1_gen_diff_mem (Or.inr (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩))))
  · exact c1_gen_diff_mem (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨rfl, rfl⟩)))))
  · exact c1_gen_diff_mem (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨rfl, rfl⟩)))))

theorem Kpos_of_gen (P : Fin 8 → ℝ)
    (h : ∃ c : Fin 14 → ℝ, (∀ i, 0 ≤ c i) ∧ P = ∑ i, c i • gen i) : P ∈ Kpos := by
  obtain ⟨c, hc, rfl⟩ := h
  exact Finset.sum_induction _ (· ∈ Kpos) (fun _ _ ha hb => Kpos_add ha hb)
    (Kpos_of_nonneg le_rfl) (fun i _ => Kpos_smul (hc i) (gen_mem_Kpos i))

/-- Helper: `s₂ = P₂ + min(0, P₁)` in the peeling construction. -/
def cgS2 (P : Fin 8 → ℝ) : ℝ := P 2 + min 0 (P 1)

/-- Helper: `s₆ = P₆ + min(0, P₇)`. -/
def cgS6 (P : Fin 8 → ℝ) : ℝ := P 6 + min 0 (P 7)

/-- Helper: `s₅ = P₅ + min(0, P₄) + min(0, s₆)`. -/
def cgS5 (P : Fin 8 → ℝ) : ℝ := P 5 + min 0 (P 4) + min 0 (cgS6 P)

theorem upset_of_covers (U : Finset (Fin 8))
    (h : ∀ x x' : Fin 8, covers x x' → x ∈ U → x' ∈ U) : IsUpSet U := by
  intro x x' hb hx
  have hb' : Relation.ReflTransGen covers x x' := hb
  clear hb
  induction hb' with
  | refl => exact hx
  | tail _ hc ih => exact h _ _ hc ih

/-- The generator decomposition (the `→` direction of `lem:rsc-cone` (a)). -/
theorem gen_of_Kpos (P : Fin 8 → ℝ) (hP : P ∈ Kpos) :
    ∃ c : Fin 14 → ℝ, (∀ i, 0 ≤ c i) ∧ P = ∑ i, c i • gen i := by
  have A : ∀ U : Finset (Fin 8), (∀ x x' : Fin 8, covers x x' → x ∈ U → x' ∈ U) →
      0 ≤ ∑ i ∈ U, P i :=
    fun U h => hP U (upset_of_covers U h)
  have hS2 : cgS2 P = P 2 + min 0 (P 1) := rfl
  have hS6 : cgS6 P = P 6 + min 0 (P 7) := rfl
  have hS5 : cgS5 P = P 5 + min 0 (P 4) + min 0 (cgS6 P) := rfl
  have kA : ∀ x : ℝ, max 0 x - max 0 (-x) = x := by
    intro x
    rcases le_total 0 x with h | h
    · rw [max_eq_right h, max_eq_left (by linarith)]; ring
    · rw [max_eq_left h, max_eq_right (by linarith)]; ring
  have kB : ∀ x : ℝ, min 0 x + max 0 (-x) = 0 := by
    intro x
    rcases le_total 0 x with h | h
    · rw [min_eq_left h, max_eq_left (by linarith)]; ring
    · rw [min_eq_right h, max_eq_right (by linarith)]; ring
  -- sign-free lower bound for the coefficient of e₃
  have h0 : 0 ≤ P 0 := by
    have := A {0} (by unfold covers; decide)
    simpa using this
  have f1 := A {3} (by unfold covers; decide)
  have f2 := A {3, 5} (by unfold covers; decide)
  have f3 := A {3, 4, 5} (by unfold covers; decide)
  have f4 := A {3, 5, 6} (by unfold covers; decide)
  have f5 := A {3, 4, 5, 6} (by unfold covers; decide)
  have f6 := A {3, 5, 6, 7} (by unfold covers; decide)
  have f7 := A {3, 4, 5, 6, 7} (by unfold covers; decide)
  have g1 := A {2, 3} (by unfold covers; decide)
  have g2 := A {2, 3, 5} (by unfold covers; decide)
  have g3 := A {2, 3, 4, 5} (by unfold covers; decide)
  have g4 := A {2, 3, 5, 6} (by unfold covers; decide)
  have g5 := A {2, 3, 4, 5, 6} (by unfold covers; decide)
  have g6 := A {2, 3, 5, 6, 7} (by unfold covers; decide)
  have g7 := A {2, 3, 4, 5, 6, 7} (by unfold covers; decide)
  have k1 := A {1, 2, 3} (by unfold covers; decide)
  have k2 := A {1, 2, 3, 5} (by unfold covers; decide)
  have k3 := A {1, 2, 3, 4, 5} (by unfold covers; decide)
  have k4 := A {1, 2, 3, 5, 6} (by unfold covers; decide)
  have k5 := A {1, 2, 3, 4, 5, 6} (by unfold covers; decide)
  have k6 := A {1, 2, 3, 5, 6, 7} (by unfold covers; decide)
  have k7 := A {1, 2, 3, 4, 5, 6, 7} (by unfold covers; decide)
  simp [Finset.sum_insert] at f1 f2 f3 f4 f5 f6 f7 g1 g2 g3 g4 g5 g6 g7 k1 k2 k3 k4 k5 k6 k7
  have hc3 : 0 ≤ P 3 + min 0 (cgS2 P) + min 0 (cgS5 P) := by
    rcases min_choice (0 : ℝ) (P 1) with h1 | h1 <;>
    rcases min_choice (0 : ℝ) (P 7) with h7 | h7 <;>
    rcases min_choice (0 : ℝ) (P 4) with h4 | h4 <;>
    rcases min_choice (0 : ℝ) (cgS2 P) with h2 | h2 <;>
    rcases min_choice (0 : ℝ) (cgS6 P) with h6 | h6 <;>
    rcases min_choice (0 : ℝ) (cgS5 P) with h5 | h5 <;>
    linarith
  refine ⟨![P 0, max 0 (P 1), max 0 (cgS2 P), P 3 + min 0 (cgS2 P) + min 0 (cgS5 P),
    max 0 (P 4), max 0 (cgS5 P), max 0 (cgS6 P), max 0 (P 7), max 0 (-cgS2 P), max 0 (-P 1),
    max 0 (-cgS5 P), max 0 (-P 4), max 0 (-cgS6 P), max 0 (-P 7)], ?_, ?_⟩
  · intro i
    fin_cases i <;> first | exact h0 | exact le_max_left _ _ | exact hc3
  · funext k
    fin_cases k <;> simp [Fin.sum_univ_succ, gen, unitVec] <;>
      linarith [kA (cgS2 P), kA (P 1), kA (P 4), kA (cgS5 P), kA (cgS6 P), kA (P 7),
        kB (cgS2 P), kB (P 1), kB (cgS5 P), kB (P 4), kB (cgS6 P), kB (P 7), hS2, hS5, hS6]

/-- `lem:rsc-cone` (a). -/
theorem rsc_cone_a :
    IsClosed Kpos ∧ Convex ℝ Kpos ∧ (∀ P ∈ Kpos, ∀ Q ∈ Kpos, P + Q ∈ Kpos) ∧
    (∀ a : ℝ, 0 ≤ a → ∀ P ∈ Kpos, a • P ∈ Kpos) ∧ (∀ P : Fin 8 → ℝ, 0 ≤ P → P ∈ Kpos) ∧
    ∀ P : Fin 8 → ℝ, P ∈ Kpos ↔ ∃ c : Fin 14 → ℝ, (∀ i, 0 ≤ c i) ∧ P = ∑ i, c i • gen i :=
  ⟨Kpos_isClosed, Kpos_convex, fun _ hP _ hQ => Kpos_add hP hQ, fun _ ha _ hP => Kpos_smul ha hP,
    fun _ hP => Kpos_of_nonneg hP, fun P => ⟨gen_of_Kpos P, Kpos_of_gen P⟩⟩

/-- `lem:rsc-cone` (b). -/
theorem rsc_cone_b {p₂ p₃ : ℝ} (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1) {Δ Q : Fin 8 → ℝ}
    (hQ : 0 ≤ Q) (hΔ : Δ ∈ Kpos) :
    merge p₂ p₃ Δ Q ∈ Kpos ∧ merge p₂ p₃ Q Δ ∈ Kpos :=
  have hp' : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 := ⟨hp.1, hp.2.1, hp.2.2.le⟩
  ⟨merge_Kpos_left hp' hΔ hQ, merge_Kpos_right hp' hQ hΔ⟩

/-- `lem:rsc-cone` (c). -/
theorem rsc_cone_c {p₂ p₃ : ℝ} (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1) {Δ : Fin 8 → ℝ}
    (hΔ : Δ ∈ Kpos) : 0 ≤ fin p₂ Δ :=
  fin_nonneg_of_Kpos hp.1.le (by linarith [hp.2.1, hp.2.2]) hΔ

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

/-- The closure step behind Steps 1 and 3 of `lem:rsc-cert` (`lem:rst-abstract` (b)). -/
theorem merge_hull (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ 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₂ 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₂ 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₂ 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₂ p₃ u z ∈ convexHull ℝ (Y' : Set _) + Kpos}) hu
    intro a ha b hb s t hs ht hst
    show merge p₂ 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₂ 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₂ p₃ u v ∈ convexHull ℝ (Y' : Set _) + Kpos}) hu'
    intro a ha b hb s t hs ht hst
    show merge p₂ 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 hp (convexHull_nonneg hY0 hu) hΔ')
      (merge_Kpos_left hp hΔ hQ0))

/-- Step 1 of `lem:rsc-cert` (supermultiplicativity). -/
theorem merge_mem_smul_PZ (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {Z : Finset (Fin 8 → ℝ)}
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ 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₃ 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₃ P' Q', merge_hull hp hZ0 hZ0 C1 hP' hQ' hQ'0, ?_⟩
  simp only [merge_smul_left, merge_smul_right, smul_smul, mul_comm η' η]

end Cone

/-! ### Trees -/

section Tree

variable {p₂ p₃ y ϖ₂ ϖ₃ : ℝ}

theorem nuSum_node (ν c₂ c₃ : ℕ) (cs : List (RTree Label)) :
    nuSum (.node (ν, c₂, c₃) cs) = ν + nuSumAll cs := by rw [nuSum]

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

theorem nuSumAll_append (l₁ l₂ : List (RTree Label)) :
    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 AdmAll_iff (L₂ L₃ : ℕ → ℕ → Prop) (cs : List (RTree Label)) :
    AdmAll L₂ L₃ cs ↔ ∀ c ∈ cs, AdmAt L₂ L₃ true c := by
  induction cs with
  | nil => simp [AdmAll]
  | cons c l ih => rw [AdmAll, ih, List.forall_mem_cons]

theorem message_node (ν c₂ c₃ : ℕ) (cs : List (RTree Label)) :
    message p₂ p₃ y ϖ₂ ϖ₃ (.node (ν, c₂, c₃) cs)
      = mergeAll p₂ p₃ y ϖ₂ ϖ₃ (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) cs := by rw [message]

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

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

theorem mergeAll_append (P : Fin 8 → ℝ) (l₁ l₂ : List (RTree Label)) :
    mergeAll p₂ p₃ y ϖ₂ ϖ₃ P (l₁ ++ l₂)
      = mergeAll p₂ p₃ y ϖ₂ ϖ₃ (mergeAll p₂ 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 (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (hy : 0 ≤ y) (hϖ₂ : 0 ≤ ϖ₂)
    (hϖ₃ : 0 ≤ ϖ₃) (ν c₂ c₃ : ℕ) : 0 ≤ init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ := by
  have hq2 : 0 ≤ 1 - p₂ := by linarith
  have hq3 : 0 ≤ 1 - p₃ := by linarith
  have hp2 : 0 ≤ p₂ := hp.1.le
  intro i
  fin_cases i <;> simp [init] <;> positivity

theorem message_nonneg (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (hy : 0 ≤ y) (hϖ₂ : 0 ≤ ϖ₂)
    (hϖ₃ : 0 ≤ ϖ₃) : ∀ t, 0 ≤ message p₂ p₃ y ϖ₂ ϖ₃ t := by
  refine MaxLeafFormal.Antinorm8.RTree.ind _ ?_
  rintro ⟨ν, c₂, c₃⟩ cs ih
  rw [message_node]
  have key : ∀ (l : List (RTree Label)), (∀ c ∈ l, 0 ≤ message p₂ p₃ y ϖ₂ ϖ₃ c) →
      ∀ P, 0 ≤ P → 0 ≤ mergeAll p₂ 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 hp hP (hl c (List.mem_cons_self ..)))
  exact key cs ih _ (init_nonneg hp hy hϖ₂ hϖ₃ ν c₂ c₃)

/-- Step 1 along a list of children. -/
theorem mergeAll_mem (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) {Z : Finset (Fin 8 → ℝ)}
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z) {ê : ℝ}
    (hê : 0 < ê) :
    ∀ (cs : List (RTree Label)) (P : Fin 8 → ℝ) (η : ℝ), 0 < η → P ∈ η • PZ Z →
      (∀ c ∈ cs, message p₂ p₃ y ϖ₂ ϖ₃ c ∈ ê ^ (size c + nuSum c) • PZ Z ∧
        0 ≤ message p₂ p₃ y ϖ₂ ϖ₃ c) →
      mergeAll p₂ 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 hp 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

/-- Scalars out of a fold: merging the children one by one equals the scaled left fold of the
rescaled child messages (Step 3, used with the semantic (C5)). -/
theorem mergeAll_eq_smul_foldl {ê : ℝ} (hê : ê ≠ 0) :
    ∀ (cs : List (RTree Label)) (P : Fin 8 → ℝ) (σ : ℝ), σ ≠ 0 →
      mergeAll p₂ p₃ y ϖ₂ ϖ₃ P cs
        = (σ * ê ^ (sizeAll cs + nuSumAll cs)) •
          (cs.map (fun c => (ê ^ (size c + nuSum c))⁻¹ • message p₂ p₃ y ϖ₂ ϖ₃ c)).foldl
            (merge p₂ p₃) (σ⁻¹ • P) := by
  intro cs
  induction cs with
  | nil =>
    intro P σ hσ
    simp [sizeAll, nuSumAll, mergeAll_nil, smul_smul, mul_inv_cancel₀ hσ]
  | cons c l ih =>
    intro P σ hσ
    have hη : ê ^ (size c + nuSum c) ≠ 0 := pow_ne_zero _ hê
    have hση : σ * ê ^ (size c + nuSum c) ≠ 0 := mul_ne_zero hσ hη
    have key : merge p₂ p₃ (σ⁻¹ • P) ((ê ^ (size c + nuSum c))⁻¹ • message p₂ p₃ y ϖ₂ ϖ₃ c)
        = (σ * ê ^ (size c + nuSum c))⁻¹ • merge p₂ p₃ P (message p₂ p₃ y ϖ₂ ϖ₃ c) := by
      rw [merge_smul_right, merge_smul_left, smul_smul, mul_inv, mul_comm]
    have hexp : σ * ê ^ (size c + sizeAll l + (nuSum c + nuSumAll l))
        = σ * ê ^ (size c + nuSum c) * ê ^ (sizeAll l + nuSumAll l) := by
      rw [mul_assoc, ← pow_add]
      congr 2
      ring
    rw [mergeAll_cons, ih _ _ hση]
    simp only [List.map_cons, List.foldl_cons]
    rw [key, sizeAll_cons, nuSumAll_cons, hexp]

end Tree

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

section Certificate

variable {p₂ p₃ y ϖ₂ ϖ₃ : ℝ}

/-- Step 2 of `lem:rsc-cert`: the initial message of a vertex that needs no Step 3, in the
four cases `c = 0`, `ν > ν_E`, and `d ≤ 1` with `c₂ = 0` or `c₂ ≥ 1`. -/
theorem init_mem (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (hy : 0 ≤ y) (hϖ₂ : 0 ≤ ϖ₂)
    (hϖ₃ : 0 ≤ ϖ₃) {ê : ℝ} (hê : 0 < ê) (hêq : ê < 1 - p₃) {Z : Finset (Fin 8 → ℝ)}
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (ν₀ νE : ℕ) (d₃ d₂ : ℕ → ℕ)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C6 : ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    {ν c₂ c₃ : ℕ} (hc : c₂ + c₃ ≤ ν)
    (hcase : c₂ + c₃ = 0 ∨ νE < ν ∨
      (2 ≤ ν ∧ ν ≤ νE ∧ ((c₂ = 0 ∧ d₃ ν ≤ 1 ∧ 1 ≤ c₃ ∧ c₃ ≤ ν - 1) ∨
        (d₃ ν ≤ 1 ∧ d₂ ν ≤ 1 ∧ 1 ≤ c₂ ∧ c₂ + c₃ ≤ ν - 1)))) :
    init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z := by
  have hq3 : 0 < 1 - p₃ := by linarith
  have hq3le : 1 - p₃ ≤ 1 := by linarith [hp.1, hp.2.1]
  have hq23 : 1 - p₃ ≤ 1 - p₂ := by linarith [hp.2.1]
  have hq2 : 0 < 1 - p₂ := by linarith
  have hê1 : ê ≤ 1 := by linarith [hp.1, hp.2.1]
  rcases hcase with h0 | hνE | ⟨h2, hνE', (⟨rfl, hd3, h1, hle⟩ | ⟨hd3, hd2, h1, hle⟩)⟩
  · obtain ⟨rfl, rfl⟩ : c₂ = 0 ∧ c₃ = 0 := by omega
    by_cases hν : ν ≤ ν₀
    · exact C2.1 ν hν
    · have hsplit : init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0
          = initInf p₂ y + ![0, 0, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0] := by
        funext i; fin_cases i <;> simp [init, initInf]
      have hK : 0 ≤ (![0, 0, 0, 0, (1/2 : ℝ) ^ ν, 0, 0, 0] : Fin 8 → ℝ) := by
        have h4 : (0 : ℝ) ≤ (1/2 : ℝ) ^ ν := pow_nonneg (by norm_num) _
        intro i; fin_cases i <;> simpa using h4
      rw [hsplit]
      refine smul_PZ_mono hZ0 (pow_pos hê _) ?_
        (smul_PZ_add_Kpos (pow_pos hê _) C2.2 (Kpos_of_nonneg hK))
      exact pow_le_pow_of_le_one hê.le hê1 (by omega)
  · 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
    have hA : (1 - p₃) ^ ν ≤ (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ := by
      calc (1 - p₃) ^ ν ≤ (1 - p₃) ^ (c₂ + c₃) := pow_le_pow_of_le_one hq3.le hq3le hc
        _ = (1 - p₃) ^ c₂ * (1 - p₃) ^ c₃ := pow_add _ _ _
        _ ≤ (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ :=
          mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hq3.le hq23 c₂) (pow_nonneg hq3.le _)
    have hscale2 : ê ^ (1 + ν) ≤ (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * ê ^ (ν₀ + 2) :=
      hscale.trans (mul_le_mul_of_nonneg_right hA (pow_nonneg hê.le _))
    have hpos : 0 < (1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ := mul_pos (pow_pos hq2 _) (pow_pos hq3 _)
    have hInf : ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃) • initInf p₂ y
        ∈ ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * ê ^ (ν₀ + 2)) • PZ Z := by
      obtain ⟨w, hw, hw'⟩ := C2.2
      refine ⟨w, hw, ?_⟩
      show ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * ê ^ (ν₀ + 2)) • w
        = ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃) • initInf p₂ y
      rw [← hw']
      show ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃ * ê ^ (ν₀ + 2)) • w
        = ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃) • (ê ^ (ν₀ + 2) • w)
      rw [smul_smul]
    have h4 : (0 : ℝ) ≤ (1/2 : ℝ) ^ ν * ϖ₂ ^ c₂ * ϖ₃ ^ c₃ :=
      mul_nonneg (mul_nonneg (pow_nonneg (by norm_num) _) (pow_nonneg hϖ₂ _)) (pow_nonneg hϖ₃ _)
    have hK : 0 ≤ (![0, 0, 0, 0, (1/2 : ℝ) ^ ν * ϖ₂ ^ c₂ * ϖ₃ ^ c₃, 0, 0, 0] : Fin 8 → ℝ) := by
      intro i; fin_cases i <;> simpa using h4
    have hsplit : init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃
        = ((1 - p₂) ^ c₂ * (1 - p₃) ^ c₃) • initInf p₂ y
          + ![0, 0, 0, 0, (1/2 : ℝ) ^ ν * ϖ₂ ^ c₂ * ϖ₃ ^ c₃, 0, 0, 0] := by
      funext i; fin_cases i <;> simp [init, initInf] <;> ring
    rw [hsplit]
    exact smul_PZ_mono hZ0 (pow_pos hê _) hscale2
      (smul_PZ_add_Kpos (mul_pos hpos (pow_pos hê _)) hInf (Kpos_of_nonneg hK))
  · exact (C4 ν h2 hνE' hd3).1 c₃ h1 hle
  · exact (C4 ν h2 hνE' hd3).2 hd2 c₂ c₃ h1 hle

/-- Steps 1–4 of `lem:rsc-cert`, for arbitrary lightness predicates `L₂`, `L₃`: every
message of an admissible tree lies in `ê ^ (size + Σ ν) • 𝒫_Z`. -/
theorem message_mem (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (hy : 0 ≤ y) (hϖ₂ : 0 ≤ ϖ₂)
    (hϖ₃ : 0 ≤ ϖ₃) {ê : ℝ} (hê : 0 < ê) (hêq : ê < 1 - p₃) {Z : Finset (Fin 8 → ℝ)}
    (hZ0 : ∀ z ∈ Z, 0 ≤ z) (ν₀ νE : ℕ) (d₃ d₂ : ℕ → ℕ)
    (hd : ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν)
    (L₂ L₃ : ℕ → ℕ → Prop)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE →
          (∀ d, 1 ≤ d → d < d₃ ν → L₃ ν d) ∧ (∀ d, 1 ≤ d → d < d₂ ν → L₂ ν d))
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (C6 : ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1)) :
    ∀ t (b : Bool), AdmAt L₂ L₃ b t →
      message p₂ p₃ y ϖ₂ ϖ₃ t ∈ ê ^ (size t + nuSum t) • PZ Z := by
  refine MaxLeafFormal.Antinorm8.RTree.ind _ ?_
  rintro ⟨ν, c₂, c₃⟩ cs ih b hadm
  rw [AdmAt] at hadm
  obtain ⟨⟨hc, hL2, hL3, h1⟩, hcs⟩ := hadm
  rw [AdmAll_iff] at hcs
  have hch : ∀ c ∈ cs, message p₂ p₃ y ϖ₂ ϖ₃ c ∈ ê ^ (size c + nuSum c) • PZ Z ∧
      0 ≤ message p₂ p₃ y ϖ₂ ϖ₃ c :=
    fun c hc' => ⟨ih c hc' true (hcs c hc'), message_nonneg hp hy hϖ₂ hϖ₃ c⟩
  rw [message_node, size_node, nuSum_node]
  set d := deg b cs with hd_def
  by_cases hcase : c₂ + c₃ = 0 ∨ νE < ν ∨
      (2 ≤ ν ∧ ν ≤ νE ∧ ((c₂ = 0 ∧ d₃ ν ≤ 1 ∧ 1 ≤ c₃ ∧ c₃ ≤ ν - 1) ∨
        (d₃ ν ≤ 1 ∧ d₂ ν ≤ 1 ∧ 1 ≤ c₂ ∧ c₂ + c₃ ≤ ν - 1)))
  · have hi := init_mem hp hy hϖ₂ hϖ₃ hê hêq hZ0 ν₀ νE d₃ d₂ C2 C4 C6 hc hcase
    have := mergeAll_mem hp hZ0 C1 hê cs _ _ (pow_pos hê _) hi hch
    convert this using 2
    rw [← pow_add]; congr 1; ring
  · have hννE : ν ≤ νE := by
      by_contra h; exact hcase (Or.inr (Or.inl (by omega)))
    have hν1 : 1 ≤ ν := by omega
    have hcpos : 1 ≤ c₂ + c₃ := by omega
    have hnot : ¬ (2 ≤ ν ∧ ν ≤ νE ∧ ((c₂ = 0 ∧ d₃ ν ≤ 1 ∧ 1 ≤ c₃ ∧ c₃ ≤ ν - 1) ∨
        (d₃ ν ≤ 1 ∧ d₂ ν ≤ 1 ∧ 1 ≤ c₂ ∧ c₂ + c₃ ≤ ν - 1))) :=
      fun h => hcase (Or.inr (Or.inr h))
    have hdlen : d ≤ cs.length + 1 := by
      rw [hd_def]; unfold deg; split <;> omega
    obtain ⟨hd3lo, hd32⟩ := hd ν hν1 hννE
    have hJ : (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) ≤ cs.length := by
      split_ifs with hc2
      · have hc3 : 1 ≤ c₃ := by omega
        have hnL3 : ¬ L₃ ν d := fun h => by
          have := hL3 (Or.inl h); omega
        have hd0 : d ≠ 0 := fun h => by
          have := hL3 (Or.inr h); omega
        have hd3 : d₃ ν ≤ d := by
          by_contra hlt
          exact hnL3 ((C3 ν hν1 hννE).1 d (by omega) (by omega))
        have hd2 : 2 ≤ d := by
          by_contra h2
          have hd1 : d = 1 := by omega
          have := h1 ⟨hd1, by omega⟩
          exact hnot ⟨by omega, hννE, Or.inl ⟨hc2, by omega, hc3, by omega⟩⟩
        unfold jOf; omega
      · have hnL2 : ¬ L₂ ν d := fun h => by
          have := hL2 (Or.inl h); omega
        have hd0 : d ≠ 0 := fun h => by
          have := hL2 (Or.inr h); omega
        have hd2' : d₂ ν ≤ d := by
          by_contra hlt
          exact hnL2 ((C3 ν hν1 hννE).2 d (by omega) (by omega))
        have hd2 : 2 ≤ d := by
          by_contra h2
          have hd1 : d = 1 := by omega
          have := h1 ⟨hd1, by omega⟩
          exact hnot ⟨by omega, hννE, Or.inr ⟨by omega, by omega, by omega, by omega⟩⟩
        unfold jOf; omega
    set J := (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) with hJdef
    have hsub : ∀ c ∈ cs.take J, c ∈ cs := fun c hc' => List.mem_of_mem_take hc'
    have hlen : (List.map (fun c => (ê ^ (size c + nuSum c))⁻¹ •
        message p₂ p₃ y ϖ₂ ϖ₃ c) (cs.take J)).length = J := by
      rw [List.length_map, List.length_take]; omega
    have hQ : ∀ Q ∈ List.map (fun c => (ê ^ (size c + nuSum c))⁻¹ •
        message p₂ p₃ y ϖ₂ ϖ₃ c) (cs.take J), Q ∈ PZ Z ∧ 0 ≤ Q := by
      intro Q hQ'
      obtain ⟨c, hc', rfl⟩ := List.mem_map.1 hQ'
      obtain ⟨h1', h2'⟩ := hch c (hsub c hc')
      exact ⟨(mem_smul_PZ_iff (pow_pos hê _)).1 h1',
        smul_nonneg (inv_nonneg.2 (pow_nonneg hê.le _)) h2'⟩
    have hfold := C5 ν hν1 hννE c₂ c₃ hcpos hc
      (List.map (fun c => (ê ^ (size c + nuSum c))⁻¹ • message p₂ p₃ y ϖ₂ ϖ₃ c) (cs.take J))
      hlen hQ
    have hmerge := mergeAll_eq_smul_foldl (p₂ := p₂) (p₃ := p₃) (y := y) (ϖ₂ := ϖ₂)
      (ϖ₃ := ϖ₃) hê.ne' (cs.take J)
      (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) (ê ^ (1 + ν)) (pow_ne_zero _ hê.ne')
    have htake : mergeAll p₂ p₃ y ϖ₂ ϖ₃ (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) (cs.take J)
        ∈ ((ê ^ (1 + ν)) * ê ^ (sizeAll (cs.take J) + nuSumAll (cs.take J))) • PZ Z := by
      rw [hmerge]
      exact Set.smul_mem_smul_set hfold
    have hη : 0 < (ê ^ (1 + ν)) * ê ^ (sizeAll (cs.take J) + nuSumAll (cs.take J)) := by
      positivity
    have hdrop := mergeAll_mem hp hZ0 C1 hê (cs.drop J) _ _ hη htake
      (fun c hc' => hch c (List.mem_of_mem_drop hc'))
    have e1 : mergeAll p₂ p₃ y ϖ₂ ϖ₃ (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) cs
        = mergeAll p₂ p₃ y ϖ₂ ϖ₃ (mergeAll p₂ p₃ y ϖ₂ ϖ₃ (init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃)
            (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, ← pow_add, ← pow_add]
    congr 1
    ring

/-- lem:rsc-cert, for arbitrary lightness predicates L₂, L₃ in (C3) and in admissibility. -/
theorem certificate_conditions_of (p₂ p₃ y ϖ₂ ϖ₃ ê : ℝ)
    (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1/2) (hy : 0 < y)
    (hϖ : 1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃))
    (hê : 0 < ê ∧ ê < 1 - p₃)
    (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (ν₀ νE : ℕ) (hνE : 1 ≤ νE) (d₃ d₂ : ℕ → ℕ)
    (hd : ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν)
    (L₂ L₃ : ℕ → ℕ → Prop)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE →
          (∀ d, 1 ≤ d → d < d₃ ν → L₃ ν d) ∧ (∀ d, 1 ≤ d → d < d₂ ν → L₂ ν d))
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (C6 : ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    (t : RTree Label) (ht : AdmAt L₂ L₃ false t) :
    cZ p₂ Z hZ * ê ^ (size t + nuSum t) ≤ fin p₂ (message p₂ p₃ y ϖ₂ ϖ₃ t) := by
  have hp' : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 := ⟨hp.1, hp.2.1, by linarith [hp.2.2]⟩
  have hm := message_mem hp' hy.le (by linarith [hϖ.1]) (by linarith [hϖ.2.2.1]) hê.1 hê.2 hZ0
    ν₀ νE d₃ d₂ hd L₂ L₃ C1 C2 C3 C4 C5 C6 t false ht
  obtain ⟨w, ⟨a, ha, k, hk, rfl⟩, hw⟩ := hm
  have hw' : message p₂ 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 hp.1.le (by linarith [hp.2.1, hp.2.2]) hk
  nlinarith

/-- lem:rsc-cert (the paper's lightness). -/
theorem certificate_conditions (p₂ p₃ y ϖ₂ ϖ₃ ê : ℝ)
    (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1/2) (hy : 0 < y)
    (hϖ : 1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃))
    (hê : 0 < ê ∧ ê < 1 - p₃)
    (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (ν₀ νE : ℕ) (hνE : 1 ≤ νE) (d₃ d₂ : ℕ → ℕ)
    (hd : ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν)
    (C1 : ∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z)
    (C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
          initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z)
    (C3 : ∀ ν, 1 ≤ ν → ν ≤ νE →
          (∀ d, 1 ≤ d → d < d₃ ν → Light₃ p₂ p₃ y ν d) ∧
          (∀ d, 1 ≤ d → d < d₂ ν → Light₂ p₂ p₃ y ν d))
    (C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
          (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
          (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
             init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z))
    (C5 : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
          ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
          (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
          Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z)
    (C6 : ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1))
    (t : RTree Label) (ht : Admissible p₂ p₃ y t) :
    cZ p₂ Z hZ * ê ^ (size t + nuSum t) ≤ fin p₂ (message p₂ p₃ y ϖ₂ ϖ₃ t) :=
  certificate_conditions_of p₂ p₃ y ϖ₂ ϖ₃ ê hp hy hϖ hê Z hZ hZ0 ν₀ νE hνE d₃ d₂ hd
    (Light₂ p₂ p₃ y) (Light₃ p₂ p₃ y) C1 C2 C3 C4 C5 C6 t ht

/-- Staged chains suffice for (C5). -/
theorem C5_of_stages {p₂ p₃ : ℝ} (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1)
    {Z : Finset (Fin 8 → ℝ)} (hZ0 : ∀ z ∈ Z, 0 ≤ z) (P : Fin 8 → ℝ) (hP : 0 ≤ P) (j : ℕ)
    (Ys : ℕ → Finset (Fin 8 → ℝ)) (hY0 : Ys 0 = {P}) (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₂ p₃ x z ∈ convexHull ℝ (Ys i : Set (Fin 8 → ℝ)) + Kpos) :
    ∀ Qs : List (Fin 8 → ℝ), Qs.length = j → (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
      Qs.foldl (merge p₂ p₃) P ∈ PZ Z := by
  have hp' : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 := ⟨hp.1, hp.2.1, hp.2.2.le⟩
  have gen : ∀ (Qs : List (Fin 8 → ℝ)) (i : ℕ) (x : Fin 8 → ℝ), i + Qs.length = j →
      x ∈ convexHull ℝ (Ys i : Set (Fin 8 → ℝ)) + Kpos →
      (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) → Qs.foldl (merge p₂ p₃) x ∈ PZ Z := by
    intro Qs
    induction Qs with
    | nil =>
      intro i x h hx _
      have hi : i = j := by simpa using h
      rw [List.foldl_nil]
      rw [hi, hYj] at hx
      exact hx
    | cons Q Qs ih =>
      intro i x h hx hQs
      rw [List.length_cons] at h
      have hi : i < j := by omega
      have hY' := hY (i + 1) (by omega) (by omega)
      rw [Nat.add_sub_cancel] at hY'
      have hQ := hQs Q (List.mem_cons_self ..)
      have hnew := merge_hull hp' (fun y hy => hYnn i hi y hy) hZ0 hY' hx hQ.1 hQ.2
      rw [List.foldl_cons]
      exact ih (i + 1) (merge p₂ p₃ x Q) (by omega) hnew
        (fun Q' hQ' => hQs Q' (List.mem_cons_of_mem _ hQ'))
  intro Qs hlen hQs
  have h1 : P ∈ convexHull ℝ ((Ys 0 : Finset (Fin 8 → ℝ)) : Set (Fin 8 → ℝ)) := by
    rw [hY0]
    exact subset_convexHull ℝ _ (by simp)
  have hPmem : P ∈ convexHull ℝ (Ys 0 : Set (Fin 8 → ℝ)) + Kpos :=
    Set.mem_add.2 ⟨P, h1, 0, Kpos_of_nonneg le_rfl, add_zero P⟩
  exact gen Qs 0 P (by omega) hPmem hQs

end Certificate

end

end MaxLeafFormal.RSCCert