MaxLeafFormal.RSCRec

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

Statements of the paper formalised here: Lemma D.5.9.

import MaxLeafFormal.RSCCert

/-!
# The ten-state recursion as algebra

Transcribes the merge, `fin`, `Init` and the forced initial messages of `sec:rsc-rec`
(the paper), the messages of `def:rsc-messages` on ordered rooted labelled trees, and
proves `eq:rsc-credit-small`, nonnegativity, the product formulas at an unforced node and
`lem:rsc-messages` (a)–(d).
-/

namespace MaxLeafFormal.RSCRec
open Finset
open MaxLeafFormal.Antinorm8 (RTree)
open MaxLeafFormal.RSCCert (Label bconst)

noncomputable section

/-- The parameters (p₂, p₃, y, ϖ₂, ϖ₃). -/
structure Par where
  p₂ : ℝ
  p₃ : ℝ
  y : ℝ
  ϖ₂ : ℝ
  ϖ₃ : ℝ

/-- Standing assumptions of `sec:rsc-light` on the parameters. -/
def Par.Standing (P : Par) : Prop :=
  0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2 ∧ 0 < P.y ∧
    1 ≤ P.ϖ₂ ∧ P.ϖ₂ ≤ 2 * (1 - P.p₂) ∧ 1 ≤ P.ϖ₃ ∧ P.ϖ₃ ≤ 2 * (1 - P.p₃)

/-- Forcing values; `in` is a Lean keyword, hence `inn`. -/
inductive Force | inn | out | excl
  deriving DecidableEq

def lam (P : Par) : ℝ := P.p₃ / P.p₂

-- indices 0..9 = A, C₀, C₁, C₂, C₃, O₀₀, O₀₁, O₁, O₂, O₃

def chiS10 (P : Par) (Q : Fin 10 → ℝ) : ℝ :=
  2 * Q 0 + 2 * Q 2 + 2 * lam P * (Q 3 + Q 4) + Q 5 + Q 6 + (1 - P.p₂) * Q 7
    + (1 - P.p₃) * (Q 8 + Q 9)

def chiCs10 (Q : Fin 10 → ℝ) : ℝ := 2 * Q 0

def chiCu10 (P : Par) (Q : Fin 10 → ℝ) : ℝ :=
  2 * Q 3 + 2 * lam P * Q 4 + Q 5 + Q 6 + Q 7 + (1 - P.p₂) * Q 8 + (1 - P.p₃) * Q 9

def chiOs10 (Q : Fin 10 → ℝ) : ℝ := Q 0

def chiOx10 (P : Par) (Q : Fin 10 → ℝ) : ℝ := Q 3 + lam P * Q 4

def chiOu10 (P : Par) (Q : Fin 10 → ℝ) : ℝ :=
  Q 5 / 2 + Q 6 + Q 7 + (1 - P.p₂) * Q 8 + (1 - P.p₃) * Q 9

def chiO10 (P : Par) (Q : Fin 10 → ℝ) : ℝ := chiOs10 Q + chiOx10 P Q + chiOu10 P Q

/-- `P ∘ Q`. -/
def merge10 (P : Par) (M Q : Fin 10 → ℝ) : Fin 10 → ℝ :=
  ![M 0 * chiS10 P Q,
    M 1 * chiCu10 P Q,
    M 2 * chiCu10 P Q + M 1 * chiCs10 Q,
    M 3 * chiCu10 P Q + M 2 * chiCs10 Q,
    M 4 * (chiCu10 P Q + chiCs10 Q) + M 3 * chiCs10 Q,
    M 5 * chiOu10 P Q,
    M 6 * (chiOu10 P Q + chiOx10 P Q) + M 5 * chiOx10 P Q,
    M 7 * (chiOu10 P Q + chiOx10 P Q) + (M 5 + M 6) * chiOs10 Q,
    M 8 * (chiOu10 P Q + chiOx10 P Q) + M 7 * chiOs10 Q,
    M 9 * (chiOu10 P Q + chiOx10 P Q + chiOs10 Q) + M 8 * chiOs10 Q]

/-- `fin`. -/
def fin10 (P : Par) (M : Fin 10 → ℝ) : ℝ :=
  M 0 + M 3 + lam P * M 4 + M 5 / 2 + M 6 + M 7 + (1 - P.p₂) * M 8 + (1 - P.p₃) * M 9

/-- `Init(ν; c₂, c₃)`. -/
def init10 (P : Par) (ν c₂ c₃ : ℕ) : Fin 10 → ℝ :=
  ![(1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.y / 2), (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.p₂ / 2),
    0, 0, 0, (1/2 : ℝ) ^ ν * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃, 0, 0, 0, 0]

/-- `Init_f`. -/
def initF (P : Par) (ν c₂ c₃ : ℕ) : Option Force → Fin 10 → ℝ
  | none => init10 P ν c₂ c₃
  | some .inn => fun i => if i = 0 then init10 P ν c₂ c₃ i else 0
  | some .out => fun i => if i = 0 then 0 else init10 P ν c₂ c₃ i
  | some .excl => fun i => if i.val < 2 then 0 else init10 P ν c₂ c₃ i

/-- A node carries `((ν_v, c_{v,2}, c_{v,3}), f(v))`. -/
abbrev FLabel := Label × Option Force

mutual

/-- `M_v` of `def:rsc-messages`: children merged left to right. -/
def message10 (P : Par) : RTree FLabel → Fin 10 → ℝ
  | .node ((ν, c₂, c₃), f) cs => mergeAll10 P (initF P ν c₂ c₃ f) cs

def mergeAll10 (P : Par) : (Fin 10 → ℝ) → List (RTree FLabel) → Fin 10 → ℝ
  | M, [] => M
  | M, c :: cs => mergeAll10 P (merge10 P M (message10 P c)) cs
end

def forcing : RTree FLabel → Option Force
  | .node (_, f) _ => f

def kids {α : Type} : RTree α → List (RTree α)
  | .node _ cs => cs

mutual

def AllLabels {α : Type} (R : α → Prop) : RTree α → Prop
  | .node a cs => R a ∧ AllLabelsList R cs

def AllLabelsList {α : Type} (R : α → Prop) : List (RTree α) → Prop
  | [] => True
  | c :: cs => AllLabels R c ∧ AllLabelsList R cs
end

/-- `eq:rsc-credit-small`. -/
theorem credit_small (P : Par) (hP : P.Standing) (ν c₂ c₃ : ℕ) (hc : c₂ + c₃ ≤ ν) :
    (1/2 : ℝ) ^ ν * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃ ≤ (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ := by
  obtain ⟨hp2, hp23, hp3, _, hw2, hw2', hw3, hw3'⟩ := hP
  obtain ⟨m, rfl⟩ : ∃ m, ν = c₂ + c₃ + m := ⟨ν - (c₂ + c₃), by omega⟩
  have h2' : (0 : ℝ) ≤ 1 - P.p₂ := by linarith
  have h3' : (0 : ℝ) ≤ 1 - P.p₃ := by linarith
  have hA : P.ϖ₂ / 2 ≤ 1 - P.p₂ := by linarith
  have hB : P.ϖ₃ / 2 ≤ 1 - P.p₃ := by linarith
  have hA0 : 0 ≤ P.ϖ₂ / 2 := by linarith
  have hB0 : 0 ≤ P.ϖ₃ / 2 := by linarith
  have hC1 : (1/2 : ℝ) ^ m ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
  have hA' : (P.ϖ₂ / 2) ^ c₂ ≤ (1 - P.p₂) ^ c₂ := pow_le_pow_left₀ hA0 hA c₂
  have hB' : (P.ϖ₃ / 2) ^ c₃ ≤ (1 - P.p₃) ^ c₃ := pow_le_pow_left₀ hB0 hB c₃
  have e : (1/2 : ℝ) ^ (c₂ + c₃ + m) * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃
      = (P.ϖ₂ / 2) ^ c₂ * (P.ϖ₃ / 2) ^ c₃ * (1/2 : ℝ) ^ m := by
    ring
  rw [e]
  have h1 : (P.ϖ₂ / 2) ^ c₂ * (P.ϖ₃ / 2) ^ c₃ * (1/2 : ℝ) ^ m
      ≤ (P.ϖ₂ / 2) ^ c₂ * (P.ϖ₃ / 2) ^ c₃ :=
    mul_le_of_le_one_right (mul_nonneg (pow_nonneg hA0 _) (pow_nonneg hB0 _)) hC1
  have h2 : (P.ϖ₂ / 2) ^ c₂ * (P.ϖ₃ / 2) ^ c₃ ≤ (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ :=
    mul_le_mul hA' hB' (pow_nonneg hB0 _) (pow_nonneg h2' _)
  linarith

/-- Nonnegativity helpers for `message10_nonneg`. -/
theorem lam_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) : 0 ≤ lam P := by
  unfold lam
  apply div_nonneg <;> linarith [hp.1, hp.2.1]

theorem merge10_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1)
    {M Q : Fin 10 → ℝ} (hM : 0 ≤ M) (hQ : 0 ≤ Q) : 0 ≤ merge10 P M Q := by
  have hl := lam_nonneg P hp
  have h2 : 0 ≤ 1 - P.p₂ := by linarith [hp.2.1, hp.2.2]
  have h3 : 0 ≤ 1 - P.p₃ := by linarith [hp.2.2]
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  have m : ∀ i, 0 ≤ M i := fun i => hM i
  have hS : 0 ≤ chiS10 P Q := by
    have a1 : 0 ≤ 2 * lam P * (Q 3 + Q 4) :=
      mul_nonneg (mul_nonneg (by norm_num) hl) (add_nonneg (g 3) (g 4))
    have a2 : 0 ≤ (1 - P.p₂) * Q 7 := mul_nonneg h2 (g 7)
    have a3 : 0 ≤ (1 - P.p₃) * (Q 8 + Q 9) := mul_nonneg h3 (add_nonneg (g 8) (g 9))
    unfold chiS10
    linarith [g 0, g 2, g 5, g 6]
  have hCu : 0 ≤ chiCu10 P Q := by
    have a1 : 0 ≤ 2 * lam P * Q 4 := mul_nonneg (mul_nonneg (by norm_num) hl) (g 4)
    have a2 : 0 ≤ (1 - P.p₂) * Q 8 := mul_nonneg h2 (g 8)
    have a3 : 0 ≤ (1 - P.p₃) * Q 9 := mul_nonneg h3 (g 9)
    unfold chiCu10
    linarith [g 3, g 5, g 6, g 7]
  have hCs : 0 ≤ chiCs10 Q := by
    unfold chiCs10
    linarith [g 0]
  have hOs : 0 ≤ chiOs10 Q := g 0
  have hOx : 0 ≤ chiOx10 P Q := by
    have a1 : 0 ≤ lam P * Q 4 := mul_nonneg hl (g 4)
    unfold chiOx10
    linarith [g 3]
  have hOu : 0 ≤ chiOu10 P Q := by
    have a2 : 0 ≤ (1 - P.p₂) * Q 8 := mul_nonneg h2 (g 8)
    have a3 : 0 ≤ (1 - P.p₃) * Q 9 := mul_nonneg h3 (g 9)
    unfold chiOu10
    linarith [g 5, g 6, g 7]
  intro i
  fin_cases i
  · exact mul_nonneg (m 0) hS
  · exact mul_nonneg (m 1) hCu
  · exact add_nonneg (mul_nonneg (m 2) hCu) (mul_nonneg (m 1) hCs)
  · exact add_nonneg (mul_nonneg (m 3) hCu) (mul_nonneg (m 2) hCs)
  · exact add_nonneg (mul_nonneg (m 4) (add_nonneg hCu hCs)) (mul_nonneg (m 3) hCs)
  · exact mul_nonneg (m 5) hOu
  · exact add_nonneg (mul_nonneg (m 6) (add_nonneg hOu hOx)) (mul_nonneg (m 5) hOx)
  · exact add_nonneg (mul_nonneg (m 7) (add_nonneg hOu hOx)) (mul_nonneg (add_nonneg (m 5) (m 6)) hOs)
  · exact add_nonneg (mul_nonneg (m 8) (add_nonneg hOu hOx)) (mul_nonneg (m 7) hOs)
  · exact add_nonneg (mul_nonneg (m 9) (add_nonneg (add_nonneg hOu hOx) hOs)) (mul_nonneg (m 8) hOs)

theorem init10_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (ν c₂ c₃ : ℕ) : 0 ≤ init10 P ν c₂ c₃ := by
  have h2 : (0 : ℝ) ≤ 1 - P.p₂ := by linarith [hp.2.1, hp.2.2]
  have h3 : (0 : ℝ) ≤ 1 - P.p₃ := by linarith [hp.2.2]
  have hϖ2 : (0 : ℝ) ≤ P.ϖ₂ := by linarith [hϖ.1]
  have hϖ3 : (0 : ℝ) ≤ P.ϖ₃ := by linarith [hϖ.2]
  have e0 : 0 ≤ (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.y / 2) :=
    mul_nonneg (mul_nonneg (pow_nonneg h2 _) (pow_nonneg h3 _)) (div_nonneg hy (by norm_num))
  have e1 : 0 ≤ (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.p₂ / 2) :=
    mul_nonneg (mul_nonneg (pow_nonneg h2 _) (pow_nonneg h3 _)) (div_nonneg hp.1.le (by norm_num))
  have e5 : 0 ≤ (1/2 : ℝ) ^ ν * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃ :=
    mul_nonneg (mul_nonneg (pow_nonneg (by norm_num) _) (pow_nonneg hϖ2 _)) (pow_nonneg hϖ3 _)
  intro i
  fin_cases i <;> first | exact e0 | exact e1 | exact e5 | simp [init10]

theorem initF_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (ν c₂ c₃ : ℕ) (f : Option Force) :
    0 ≤ initF P ν c₂ c₃ f := by
  have h0 := init10_nonneg P hp hy hϖ ν c₂ c₃
  cases f with
  | none => exact h0
  | some g =>
    cases g <;> intro i <;> simp only [initF, Pi.zero_apply] <;> split_ifs <;>
      first | exact h0 i | exact le_refl _

/-- Nonnegativity of messages (`lem:rsc-recursion`, first assertion). -/
theorem message10_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (t : RTree FLabel) : 0 ≤ message10 P t := by
  revert t
  refine MaxLeafFormal.Antinorm8.RTree.ind _ ?_
  rintro ⟨⟨ν, c₂, c₃⟩, f⟩ cs ih
  rw [message10]
  have key : ∀ (l : List (RTree FLabel)), (∀ c ∈ l, 0 ≤ message10 P c) →
      ∀ M : Fin 10 → ℝ, 0 ≤ M → 0 ≤ mergeAll10 P M l := by
    intro l
    induction l with
    | nil => intro _ M hM; rwa [mergeAll10]
    | cons c l ihl =>
      intro hl M hM
      rw [mergeAll10]
      exact ihl (fun c' hc' => hl c' (List.mem_cons_of_mem _ hc')) _
        (merge10_nonneg P hp hM (hl c (List.mem_cons_self ..)))
  exact key cs ih _ (initF_nonneg P hp hy hϖ ν c₂ c₃ f)

/-- Zeroth coordinate of a merge chain. -/
theorem merge10_zero (P : Par) (M Q : Fin 10 → ℝ) : merge10 P M Q 0 = M 0 * chiS10 P Q := by
  rfl

theorem mergeAll10_zero (P : Par) (cs : List (RTree FLabel)) : ∀ M : Fin 10 → ℝ,
    mergeAll10 P M cs 0 = M 0 * (cs.map (fun c => chiS10 P (message10 P c))).prod := by
  induction cs with
  | nil => intro M; rw [mergeAll10]; simp
  | cons c cs ih =>
    intro M
    rw [mergeAll10, ih, merge10_zero]
    simp only [List.map_cons, List.prod_cons]
    ring

/-- Sum of coordinates 5..9 of a merge. -/
theorem merge10_osum (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 5 + merge10 P M Q 6 + merge10 P M Q 7 + merge10 P M Q 8 + merge10 P M Q 9
      = (M 5 + M 6 + M 7 + M 8 + M 9) * chiO10 P Q := by
  show (M 5 * chiOu10 P Q) + (M 6 * (chiOu10 P Q + chiOx10 P Q) + M 5 * chiOx10 P Q)
      + (M 7 * (chiOu10 P Q + chiOx10 P Q) + (M 5 + M 6) * chiOs10 Q)
      + (M 8 * (chiOu10 P Q + chiOx10 P Q) + M 7 * chiOs10 Q)
      + (M 9 * (chiOu10 P Q + chiOx10 P Q + chiOs10 Q) + M 8 * chiOs10 Q)
      = (M 5 + M 6 + M 7 + M 8 + M 9) * chiO10 P Q
  rw [chiO10]
  ring

theorem mergeAll10_osum (P : Par) (cs : List (RTree FLabel)) : ∀ M : Fin 10 → ℝ,
    mergeAll10 P M cs 5 + mergeAll10 P M cs 6 + mergeAll10 P M cs 7 + mergeAll10 P M cs 8
      + mergeAll10 P M cs 9
      = (M 5 + M 6 + M 7 + M 8 + M 9) * (cs.map (fun c => chiO10 P (message10 P c))).prod := by
  induction cs with
  | nil => intro M; rw [mergeAll10]; simp
  | cons c cs ih =>
    intro M
    rw [mergeAll10, ih, merge10_osum]
    simp only [List.map_cons, List.prod_cons]
    ring

/-- At an unforced node: `A = q^c·(y/2)·∏ χ_S` and `O₀₀+…+O₃ = 2^{-ν}ϖ^c·∏ χ_O`
(the identities used in `lem:rsc-jlemma` and `lem:rsc-odds`). -/
theorem message10_root (P : Par) (ℓ : Label) (cs : List (RTree FLabel)) :
    message10 P (.node (ℓ, none) cs) 0
        = (1 - P.p₂) ^ ℓ.2.1 * (1 - P.p₃) ^ ℓ.2.2 * (P.y / 2)
            * (cs.map (fun c => chiS10 P (message10 P c))).prod ∧
    (message10 P (.node (ℓ, none) cs) 5 + message10 P (.node (ℓ, none) cs) 6
        + message10 P (.node (ℓ, none) cs) 7 + message10 P (.node (ℓ, none) cs) 8
        + message10 P (.node (ℓ, none) cs) 9)
        = (1/2 : ℝ) ^ ℓ.1 * P.ϖ₂ ^ ℓ.2.1 * P.ϖ₃ ^ ℓ.2.2
            * (cs.map (fun c => chiO10 P (message10 P c))).prod := by
  obtain ⟨ν, c₂, c₃⟩ := ℓ
  dsimp only
  have hinit : initF P ν c₂ c₃ none = init10 P ν c₂ c₃ := rfl
  rw [message10, hinit]
  have h0 : init10 P ν c₂ c₃ 0 = (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.y / 2) := rfl
  have h5 : init10 P ν c₂ c₃ 5 + init10 P ν c₂ c₃ 6 + init10 P ν c₂ c₃ 7
      + init10 P ν c₂ c₃ 8 + init10 P ν c₂ c₃ 9 = (1/2 : ℝ) ^ ν * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃ := by
    simp [init10]
  refine ⟨?_, ?_⟩
  · rw [mergeAll10_zero, h0]
  · rw [mergeAll10_osum, h5]

/-! ### Helpers for `lem:rsc-messages` -/

theorem standing_hp (P : Par) (hP : P.Standing) : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 := by
  obtain ⟨h1, h2, h3, -, -, -, -, -⟩ := hP
  exact ⟨h1, h2, by linarith⟩

theorem standing_y (P : Par) (hP : P.Standing) : 0 < P.y := by
  obtain ⟨-, -, -, h, -, -, -, -⟩ := hP
  exact h

theorem standing_ϖ (P : Par) (hP : P.Standing) : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ := by
  obtain ⟨-, -, -, -, h1, -, h2, -⟩ := hP
  exact ⟨h1, h2⟩

theorem msg_nonneg (P : Par) (hP : P.Standing) (t : RTree FLabel) : 0 ≤ message10 P t :=
  message10_nonneg P (standing_hp P hP) (standing_y P hP).le (standing_ϖ P hP) t

theorem lam_one (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) : 1 ≤ lam P := by
  unfold lam
  rw [le_div_iff₀ hp.1]
  linarith [hp.2.1]

theorem lam_mul (P : Par) (hp2 : 0 < P.p₂) : lam P * P.p₂ = P.p₃ := by
  unfold lam
  have : P.p₂ ≠ 0 := ne_of_gt hp2
  field_simp

theorem merge10_e1 (P : Par) (M Q : Fin 10 → ℝ) : merge10 P M Q 1 = M 1 * chiCu10 P Q := by
  first | rfl | simp [merge10]

theorem merge10_e2 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 2 = M 2 * chiCu10 P Q + M 1 * chiCs10 Q := by
  first | rfl | simp [merge10]

theorem merge10_e3 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 3 = M 3 * chiCu10 P Q + M 2 * chiCs10 Q := by
  first | rfl | simp [merge10]

theorem merge10_e4 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 4 = M 4 * (chiCu10 P Q + chiCs10 Q) + M 3 * chiCs10 Q := by
  first | rfl | simp [merge10]

theorem merge10_e5 (P : Par) (M Q : Fin 10 → ℝ) : merge10 P M Q 5 = M 5 * chiOu10 P Q := by
  first | rfl | simp [merge10]

theorem merge10_e6 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 6 = M 6 * (chiOu10 P Q + chiOx10 P Q) + M 5 * chiOx10 P Q := by
  first | rfl | simp [merge10]

theorem merge10_e7 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 7 = M 7 * (chiOu10 P Q + chiOx10 P Q) + (M 5 + M 6) * chiOs10 Q := by
  first | rfl | simp [merge10]

theorem merge10_e8 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 8 = M 8 * (chiOu10 P Q + chiOx10 P Q) + M 7 * chiOs10 Q := by
  first | rfl | simp [merge10]

theorem merge10_e9 (P : Par) (M Q : Fin 10 → ℝ) :
    merge10 P M Q 9 = M 9 * (chiOu10 P Q + chiOx10 P Q + chiOs10 Q) + M 8 * chiOs10 Q := by
  first | rfl | simp [merge10]

theorem init10_0 (P : Par) (ν c₂ c₃ : ℕ) :
    init10 P ν c₂ c₃ 0 = (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.y / 2) := by
  first | rfl | simp [init10]

theorem init10_1 (P : Par) (ν c₂ c₃ : ℕ) :
    init10 P ν c₂ c₃ 1 = (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.p₂ / 2) := by
  first | rfl | simp [init10]

theorem init10_5 (P : Par) (ν c₂ c₃ : ℕ) :
    init10 P ν c₂ c₃ 5 = (1/2 : ℝ) ^ ν * P.ϖ₂ ^ c₂ * P.ϖ₃ ^ c₃ := by
  first | rfl | simp [init10]

theorem init10_2 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 2 = 0 := by
  first | rfl | simp [init10]

theorem init10_3 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 3 = 0 := by
  first | rfl | simp [init10]

theorem init10_4 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 4 = 0 := by
  first | rfl | simp [init10]

theorem init10_6 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 6 = 0 := by
  first | rfl | simp [init10]

theorem init10_7 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 7 = 0 := by
  first | rfl | simp [init10]

theorem init10_8 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 8 = 0 := by
  first | rfl | simp [init10]

theorem init10_9 (P : Par) (ν c₂ c₃ : ℕ) : init10 P ν c₂ c₃ 9 = 0 := by
  first | rfl | simp [init10]

theorem merge10_low (P : Par) {M : Fin 10 → ℝ} (Q : Fin 10 → ℝ)
    (h : M 0 = 0 ∧ M 1 = 0 ∧ M 2 = 0 ∧ M 3 = 0 ∧ M 4 = 0) :
    merge10 P M Q 0 = 0 ∧ merge10 P M Q 1 = 0 ∧ merge10 P M Q 2 = 0 ∧
      merge10 P M Q 3 = 0 ∧ merge10 P M Q 4 = 0 := by
  obtain ⟨h0, h1, h2, h3, h4⟩ := h
  rw [merge10_zero, merge10_e1, merge10_e2, merge10_e3, merge10_e4, h0, h1, h2, h3, h4]
  simp

theorem mergeAll10_low (P : Par) (cs : List (RTree FLabel)) : ∀ M : Fin 10 → ℝ,
    (M 0 = 0 ∧ M 1 = 0 ∧ M 2 = 0 ∧ M 3 = 0 ∧ M 4 = 0) →
      (mergeAll10 P M cs 0 = 0 ∧ mergeAll10 P M cs 1 = 0 ∧ mergeAll10 P M cs 2 = 0 ∧
        mergeAll10 P M cs 3 = 0 ∧ mergeAll10 P M cs 4 = 0) := by
  induction cs with
  | nil => intro M h; rw [mergeAll10]; exact h
  | cons c cs ih => intro M h; rw [mergeAll10]; exact ih _ (merge10_low P _ h)

theorem chi_facts (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) {Q : Fin 10 → ℝ}
    (hQ : 0 ≤ Q) :
    0 ≤ chiOu10 P Q ∧ 0 ≤ chiOx10 P Q ∧ 0 ≤ chiOs10 Q ∧ 0 ≤ chiCu10 P Q ∧ 0 ≤ chiCs10 Q ∧
      0 ≤ chiS10 P Q ∧ chiOu10 P Q + chiOx10 P Q ≤ chiCu10 P Q ∧ chiOs10 Q ≤ chiCs10 Q := by
  have hl := lam_nonneg P hp
  have h2 : 0 ≤ 1 - P.p₂ := by linarith [hp.2.1, hp.2.2]
  have h3 : 0 ≤ 1 - P.p₃ := by linarith [hp.2.2]
  have g : ∀ i, 0 ≤ Q i := fun i => hQ i
  have hS : 0 ≤ chiS10 P Q := by
    have a1 : 0 ≤ 2 * lam P * (Q 3 + Q 4) :=
      mul_nonneg (mul_nonneg (by norm_num) hl) (add_nonneg (g 3) (g 4))
    have a2 : 0 ≤ (1 - P.p₂) * Q 7 := mul_nonneg h2 (g 7)
    have a3 : 0 ≤ (1 - P.p₃) * (Q 8 + Q 9) := mul_nonneg h3 (add_nonneg (g 8) (g 9))
    unfold chiS10
    linarith [g 0, g 2, g 5, g 6]
  have hCu : 0 ≤ chiCu10 P Q := by
    have a1 : 0 ≤ 2 * lam P * Q 4 := mul_nonneg (mul_nonneg (by norm_num) hl) (g 4)
    have a2 : 0 ≤ (1 - P.p₂) * Q 8 := mul_nonneg h2 (g 8)
    have a3 : 0 ≤ (1 - P.p₃) * Q 9 := mul_nonneg h3 (g 9)
    unfold chiCu10
    linarith [g 3, g 5, g 6, g 7]
  have hCs : 0 ≤ chiCs10 Q := by
    unfold chiCs10
    linarith [g 0]
  have hOs : 0 ≤ chiOs10 Q := g 0
  have hOx : 0 ≤ chiOx10 P Q := by
    have a1 : 0 ≤ lam P * Q 4 := mul_nonneg hl (g 4)
    unfold chiOx10
    linarith [g 3]
  have hOu : 0 ≤ chiOu10 P Q := by
    have a2 : 0 ≤ (1 - P.p₂) * Q 8 := mul_nonneg h2 (g 8)
    have a3 : 0 ≤ (1 - P.p₃) * Q 9 := mul_nonneg h3 (g 9)
    unfold chiOu10
    linarith [g 5, g 6, g 7]
  have hw : chiOu10 P Q + chiOx10 P Q ≤ chiCu10 P Q := by
    have a1 : 0 ≤ lam P * Q 4 := mul_nonneg hl (g 4)
    unfold chiOu10 chiOx10 chiCu10
    linarith [g 3, g 5]
  have hsO : chiOs10 Q ≤ chiCs10 Q := by
    unfold chiCs10 chiOs10
    linarith [g 0]
  exact ⟨hOu, hOx, hOs, hCu, hCs, hS, hw, hsO⟩

/-- The (a)-inequalities of `lem:rsc-messages`. -/
def AInd (P : Par) (M : Fin 10 → ℝ) : Prop :=
  P.p₂ / 2 * (M 5 + M 6) ≤ M 1 ∧ P.p₂ / 2 * M 7 ≤ M 2 ∧
    P.p₂ / 2 * M 8 ≤ M 3 ∧ P.p₂ / 2 * M 9 ≤ M 4

/-- The (b)-inequality of `lem:rsc-messages`. -/
def BInd (P : Par) (M : Fin 10 → ℝ) : Prop :=
  M 1 + M 2 + M 3 + M 4 ≤ P.p₂ / P.y * M 0

theorem AInd_merge (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1)
    {M Q : Fin 10 → ℝ} (hM : 0 ≤ M) (hQ : 0 ≤ Q) (ha : AInd P M) : AInd P (merge10 P M Q) := by
  obtain ⟨hou, hox, hos, -, -, -, hw, hsO⟩ := chi_facts P hp hQ
  unfold AInd at ha ⊢
  obtain ⟨a1, a2, a3, a4⟩ := ha
  have n : ∀ i, (0 : ℝ) ≤ M i := fun i => hM i
  have hwo : 0 ≤ chiOu10 P Q + chiOx10 P Q := add_nonneg hou hox
  rw [merge10_e1, merge10_e2, merge10_e3, merge10_e4, merge10_e5, merge10_e6, merge10_e7,
    merge10_e8, merge10_e9]
  refine ⟨?_, ?_, ?_, ?_⟩
  · have k1 := mul_le_mul_of_nonneg_right a1 hwo
    have k2 := mul_le_mul_of_nonneg_left hw (n 1)
    linarith
  · have k1 := mul_le_mul_of_nonneg_right a2 hwo
    have k2 := mul_le_mul_of_nonneg_left hw (n 2)
    have k3 := mul_le_mul_of_nonneg_right a1 hos
    have k4 := mul_le_mul_of_nonneg_left hsO (n 1)
    linarith
  · have k1 := mul_le_mul_of_nonneg_right a3 hwo
    have k2 := mul_le_mul_of_nonneg_left hw (n 3)
    have k3 := mul_le_mul_of_nonneg_right a2 hos
    have k4 := mul_le_mul_of_nonneg_left hsO (n 2)
    linarith
  · have k1 := mul_le_mul_of_nonneg_right a4 (add_nonneg hwo hos)
    have k2 := mul_le_mul_of_nonneg_left (add_le_add hw hsO) (n 4)
    have k3 := mul_le_mul_of_nonneg_right a3 hos
    have k4 := mul_le_mul_of_nonneg_left hsO (n 3)
    linarith

theorem AInd_mergeAll (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1)
    (cs : List (RTree FLabel)) :
    (∀ c ∈ cs, 0 ≤ message10 P c) → ∀ M : Fin 10 → ℝ, 0 ≤ M → AInd P M →
      AInd P (mergeAll10 P M cs) := by
  induction cs with
  | nil => intro _ M _ ha; rw [mergeAll10]; exact ha
  | cons c cs ih =>
    intro hn M hM ha
    rw [mergeAll10]
    exact ih (fun c' hc' => hn c' (List.mem_cons_of_mem _ hc')) _
      (merge10_nonneg P hp hM (hn c (List.mem_cons_self ..)))
      (AInd_merge P hp hM (hn c (List.mem_cons_self ..)) ha)

theorem AInd_of_zero (P : Par) (M : Fin 10 → ℝ) (h1 : M 1 = 0) (h2 : M 2 = 0) (h3 : M 3 = 0)
    (h4 : M 4 = 0) (h5 : M 5 = 0) (h6 : M 6 = 0) (h7 : M 7 = 0) (h8 : M 8 = 0)
    (h9 : M 9 = 0) : AInd P M := by
  unfold AInd
  rw [h1, h2, h3, h4, h5, h6, h7, h8, h9]
  norm_num

theorem AInd_init10 (P : Par) (hP : P.Standing) (ν c₂ c₃ : ℕ) (hc : c₂ + c₃ ≤ ν) :
    AInd P (init10 P ν c₂ c₃) := by
  have hC := credit_small P hP ν c₂ c₃ hc
  have hq : 0 ≤ P.p₂ / 2 := by linarith [(standing_hp P hP).1]
  have hA1 := mul_le_mul_of_nonneg_left hC hq
  unfold AInd
  rw [init10_1, init10_5, init10_2, init10_3, init10_4, init10_6, init10_7, init10_8,
    init10_9]
  refine ⟨by linarith, by norm_num, by norm_num, by norm_num⟩

theorem AInd_initF (P : Par) (hP : P.Standing) (ν c₂ c₃ : ℕ) (hc : c₂ + c₃ ≤ ν)
    (f : Option Force) (hf : f ≠ some .excl) : AInd P (initF P ν c₂ c₃ f) := by
  cases f with
  | none => exact AInd_init10 P hP ν c₂ c₃ hc
  | some g =>
    cases g with
    | inn =>
      apply AInd_of_zero P <;> simp [initF]
    | out =>
      have hI := AInd_init10 P hP ν c₂ c₃ hc
      have ho : ∀ i : Fin 10, i ≠ 0 → initF P ν c₂ c₃ (some .out) i = init10 P ν c₂ c₃ i :=
        fun i hi => by simp [initF, hi]
      unfold AInd at hI ⊢
      rw [ho 5 (by decide), ho 6 (by decide), ho 1 (by decide), ho 7 (by decide),
        ho 2 (by decide), ho 8 (by decide), ho 3 (by decide), ho 9 (by decide),
        ho 4 (by decide)]
      exact hI
    | excl => exact absurd rfl hf

theorem BInd_of_zero (P : Par) (hp2 : 0 ≤ P.p₂) (hy : 0 < P.y) (M : Fin 10 → ℝ)
    (h1 : M 1 = 0) (h2 : M 2 = 0) (h3 : M 3 = 0) (h4 : M 4 = 0) (h0 : 0 ≤ M 0) :
    BInd P M := by
  unfold BInd
  rw [h1, h2, h3, h4]
  have := mul_nonneg (div_nonneg hp2 hy.le) h0
  linarith

theorem BInd_init10 (P : Par) (hy : 0 < P.y) (ν c₂ c₃ : ℕ) : BInd P (init10 P ν c₂ c₃) := by
  have hy0 : P.y ≠ 0 := ne_of_gt hy
  have eq : P.p₂ / P.y * ((1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.y / 2))
      = (1 - P.p₂) ^ c₂ * (1 - P.p₃) ^ c₃ * (P.p₂ / 2) := by
    field_simp <;> ring
  unfold BInd
  rw [init10_0, init10_1, init10_2, init10_3, init10_4, eq]
  linarith

theorem BInd_initF (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 < P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (ν c₂ c₃ : ℕ) (f : Option Force) (hf : f ≠ some .out) :
    BInd P (initF P ν c₂ c₃ f) := by
  cases f with
  | none => exact BInd_init10 P hy ν c₂ c₃
  | some g =>
    cases g with
    | inn =>
      have hz : ∀ i : Fin 10, i ≠ 0 → initF P ν c₂ c₃ (some .inn) i = 0 :=
        fun i hi => by simp [initF, hi]
      exact BInd_of_zero P hp.1.le hy _ (hz 1 (by decide)) (hz 2 (by decide))
        (hz 3 (by decide)) (hz 4 (by decide))
        (initF_nonneg P hp hy.le hϖ ν c₂ c₃ (some .inn) 0)
    | out => exact absurd rfl hf
    | excl =>
      have x0 : initF P ν c₂ c₃ (some .excl) 0 = 0 := by simp [initF]
      have x1 : initF P ν c₂ c₃ (some .excl) 1 = 0 := by simp [initF]
      have x2 : initF P ν c₂ c₃ (some .excl) 2 = 0 := by simp [initF, init10]
      have x3 : initF P ν c₂ c₃ (some .excl) 3 = 0 := by simp [initF, init10]
      have x4 : initF P ν c₂ c₃ (some .excl) 4 = 0 := by simp [initF, init10]
      exact BInd_of_zero P hp.1.le hy _ x1 x2 x3 x4 (le_of_eq x0.symm)

theorem BInd_merge (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 < P.y)
    {M Q : Fin 10 → ℝ} (hM : 0 ≤ M) (hQ : 0 ≤ Q) (hA : AInd P Q) (hB : BInd P M) :
    BInd P (merge10 P M Q) := by
  obtain ⟨-, -, -, hu, hs, -, -, -⟩ := chi_facts P hp hQ
  unfold AInd at hA
  obtain ⟨-, a2, a3, -⟩ := hA
  have hlam := lam_mul P hp.1
  have hl1 := lam_one P hp
  have k2 : 0 ≤ (lam P - 1) * (Q 3 - P.p₂ / 2 * Q 8) :=
    mul_nonneg (by linarith) (by linarith)
  have hlamK : lam P * P.p₂ * Q 8 = P.p₃ * Q 8 := by rw [hlam]
  have hsum : chiCu10 P Q + chiCs10 Q ≤ chiS10 P Q := by
    unfold chiS10 chiCu10 chiCs10
    linarith
  have hB' : M 1 + M 2 + M 3 + M 4 ≤ P.p₂ / P.y * M 0 := hB
  have n0 : (0 : ℝ) ≤ M 0 := hM 0
  have hq : 0 ≤ P.p₂ / P.y * M 0 := mul_nonneg (div_nonneg hp.1.le hy.le) n0
  have h1 := mul_le_mul_of_nonneg_right hB' (add_nonneg hu hs)
  have h2 := mul_le_mul_of_nonneg_left hsum hq
  unfold BInd
  rw [merge10_zero, merge10_e1, merge10_e2, merge10_e3, merge10_e4]
  linarith

theorem BInd_mergeAll (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1) (hy : 0 < P.y)
    (cs : List (RTree FLabel)) :
    (∀ c ∈ cs, 0 ≤ message10 P c) → (∀ c ∈ cs, AInd P (message10 P c)) →
      ∀ M : Fin 10 → ℝ, 0 ≤ M → BInd P M → BInd P (mergeAll10 P M cs) := by
  induction cs with
  | nil => intro _ _ M _ hB; rw [mergeAll10]; exact hB
  | cons c cs ih =>
    intro hn hA M hM hB
    rw [mergeAll10]
    exact ih (fun c' hc' => hn c' (List.mem_cons_of_mem _ hc'))
      (fun c' hc' => hA c' (List.mem_cons_of_mem _ hc')) _
      (merge10_nonneg P hp hM (hn c (List.mem_cons_self ..)))
      (BInd_merge P hp hy hM (hn c (List.mem_cons_self ..)) (hA c (List.mem_cons_self ..)) hB)

theorem allLabelsList_mem {R : FLabel → Prop} (cs : List (RTree FLabel)) :
    AllLabelsList R cs → ∀ c ∈ cs, AllLabels R c := by
  induction cs with
  | nil => intro _ c hc; simp at hc
  | cons d ds ih =>
    intro h c hc
    rw [AllLabelsList] at h
    obtain ⟨h1, h2⟩ := h
    rcases List.mem_cons.1 hc with rfl | hc'
    · exact h1
    · exact ih h2 c hc'

theorem AInd_tree (P : Par) (hP : P.Standing) (t : RTree FLabel)
    (hc : AllLabels (fun a : FLabel => a.1.2.1 + a.1.2.2 ≤ a.1.1) t)
    (hf : forcing t ≠ some .excl) : AInd P (message10 P t) := by
  cases t with
  | node a cs =>
    obtain ⟨⟨ν, c₂, c₃⟩, f⟩ := a
    rw [AllLabels] at hc
    obtain ⟨hcn, -⟩ := hc
    have hcn' : c₂ + c₃ ≤ ν := hcn
    have hf' : f ≠ some .excl := hf
    rw [message10]
    exact AInd_mergeAll P (standing_hp P hP) cs (fun c _ => msg_nonneg P hP c) _
      (initF_nonneg P (standing_hp P hP) (standing_y P hP).le (standing_ϖ P hP) ν c₂ c₃ f)
      (AInd_initF P hP ν c₂ c₃ hcn' f hf')

theorem BInd_tree (P : Par) (hP : P.Standing) (t : RTree FLabel)
    (hc : AllLabels (fun a : FLabel => a.1.2.1 + a.1.2.2 ≤ a.1.1) t)
    (hf : forcing t ≠ some .out) (hk : ∀ c ∈ kids t, forcing c ≠ some .excl) :
    BInd P (message10 P t) := by
  cases t with
  | node a cs =>
    obtain ⟨⟨ν, c₂, c₃⟩, f⟩ := a
    rw [AllLabels] at hc
    obtain ⟨-, hcs⟩ := hc
    have hf' : f ≠ some .out := hf
    rw [message10]
    exact BInd_mergeAll P (standing_hp P hP) (standing_y P hP) cs
      (fun c _ => msg_nonneg P hP c)
      (fun c hc' => AInd_tree P hP c (allLabelsList_mem cs hcs c hc') (hk c hc'))
      _
      (initF_nonneg P (standing_hp P hP) (standing_y P hP).le (standing_ϖ P hP) ν c₂ c₃ f)
      (BInd_initF P (standing_hp P hP) (standing_y P hP) (standing_ϖ P hP) ν c₂ c₃ f hf')

theorem low_tree (P : Par) (t : RTree FLabel) (hf : forcing t = some .excl) :
    message10 P t 0 = 0 ∧ message10 P t 1 = 0 ∧ message10 P t 2 = 0 ∧
      message10 P t 3 = 0 ∧ message10 P t 4 = 0 := by
  cases t with
  | node a cs =>
    obtain ⟨⟨ν, c₂, c₃⟩, f⟩ := a
    have hf' : f = some .excl := hf
    rw [message10, hf']
    have x0 : initF P ν c₂ c₃ (some .excl) 0 = 0 := by simp [initF]
    have x1 : initF P ν c₂ c₃ (some .excl) 1 = 0 := by simp [initF]
    have x2 : initF P ν c₂ c₃ (some .excl) 2 = 0 := by simp [initF, init10]
    have x3 : initF P ν c₂ c₃ (some .excl) 3 = 0 := by simp [initF, init10]
    have x4 : initF P ν c₂ c₃ (some .excl) 4 = 0 := by simp [initF, init10]
    exact mergeAll10_low P cs _ ⟨x0, x1, x2, x3, x4⟩

theorem chi_bound (P : Par) (hP : P.Standing) (M : Fin 10 → ℝ) (hM : 0 ≤ M)
    (hB : BInd P M) : chiS10 P M ≤ bconst P.p₂ P.p₃ P.y * chiO10 P M := by
  have hp := standing_hp P hP
  have hy := standing_y P hP
  obtain ⟨hp2, hp23, hp3⟩ := hp
  have n : ∀ i, (0 : ℝ) ≤ M i := fun i => hM i
  have hl : 0 ≤ lam P := lam_nonneg P ⟨hp2, hp23, hp3⟩
  have hlam := lam_mul P hp2
  have hl1 := lam_one P ⟨hp2, hp23, hp3⟩
  have h2 : 0 ≤ 1 - P.p₂ := by linarith
  have h3 : 0 ≤ 1 - P.p₃ := by linarith
  have hB' : M 1 + M 2 + M 3 + M 4 ≤ P.p₂ / P.y * M 0 := hB
  have hD : chiS10 P M - 2 * chiO10 P M ≤ 2 * M 2 + 2 * (lam P - 1) * M 3 := by
    unfold chiS10 chiO10 chiOs10 chiOx10 chiOu10
    have h7 : 0 ≤ P.p₂ * M 7 := mul_nonneg hp2.le (n 7)
    have h8 : 0 ≤ (1 - 2 * P.p₂ + P.p₃) * M 8 := mul_nonneg (by linarith) (n 8)
    have h9 : 0 ≤ (1 - P.p₃) * M 9 := mul_nonneg h3 (n 9)
    linarith [n 6, n 7]
  have hE : P.p₂ * (2 * M 2 + 2 * (lam P - 1) * M 3)
      = 2 * P.p₂ * M 2 + 2 * (P.p₃ - P.p₂) * M 3 := by
    linear_combination (2 * M 3) * hlam
  have m1 : P.p₂ ≤ max P.p₂ (P.p₃ - P.p₂) := le_max_left _ _
  have m2 : P.p₃ - P.p₂ ≤ max P.p₂ (P.p₃ - P.p₂) := le_max_right _ _
  have hF : 2 * P.p₂ * M 2 + 2 * (P.p₃ - P.p₂) * M 3
      ≤ 2 * max P.p₂ (P.p₃ - P.p₂) * (M 2 + M 3) := by
    have e1 := mul_le_mul_of_nonneg_right m1 (n 2)
    have e2 := mul_le_mul_of_nonneg_right m2 (n 3)
    linarith
  have hG : M 2 + M 3 ≤ P.p₂ / P.y * M 0 := by linarith [n 1, n 4]
  have hO0 : M 0 ≤ chiO10 P M := by
    unfold chiO10 chiOs10 chiOx10 chiOu10
    have a1 : 0 ≤ lam P * M 4 := mul_nonneg hl (n 4)
    have a2 : 0 ≤ (1 - P.p₂) * M 8 := mul_nonneg h2 (n 8)
    have a3 : 0 ≤ (1 - P.p₃) * M 9 := mul_nonneg h3 (n 9)
    linarith [n 3, n 5, n 6, n 7]
  have hm0 : 0 ≤ 2 * max P.p₂ (P.p₃ - P.p₂) := by
    have := le_max_left P.p₂ (P.p₃ - P.p₂)
    linarith
  have hq : 0 ≤ P.p₂ / P.y := div_nonneg hp2.le hy.le
  have hfin : P.p₂ * (chiS10 P M - 2 * chiO10 P M)
      ≤ P.p₂ * (2 * max P.p₂ (P.p₃ - P.p₂) / P.y * chiO10 P M) := by
    calc P.p₂ * (chiS10 P M - 2 * chiO10 P M)
        ≤ P.p₂ * (2 * M 2 + 2 * (lam P - 1) * M 3) := mul_le_mul_of_nonneg_left hD hp2.le
      _ = 2 * P.p₂ * M 2 + 2 * (P.p₃ - P.p₂) * M 3 := hE
      _ ≤ 2 * max P.p₂ (P.p₃ - P.p₂) * (M 2 + M 3) := hF
      _ ≤ 2 * max P.p₂ (P.p₃ - P.p₂) * (P.p₂ / P.y * M 0) := mul_le_mul_of_nonneg_left hG hm0
      _ ≤ 2 * max P.p₂ (P.p₃ - P.p₂) * (P.p₂ / P.y * chiO10 P M) :=
          mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left hO0 hq) hm0
      _ = P.p₂ * (2 * max P.p₂ (P.p₃ - P.p₂) / P.y * chiO10 P M) := by ring
  have hD2 := le_of_mul_le_mul_left hfin hp2
  unfold bconst
  rw [add_mul]
  linarith

theorem chi_compare (P : Par) (hP : P.Standing) (M : Fin 10 → ℝ) (hM : 0 ≤ M)
    (hA : AInd P M) : chiO10 P M ≤ chiS10 P M := by
  have hp := standing_hp P hP
  obtain ⟨hp2, hp23, hp3⟩ := hp
  have n : ∀ i, (0 : ℝ) ≤ M i := fun i => hM i
  have hl : 0 ≤ lam P := lam_nonneg P ⟨hp2, hp23, hp3⟩
  have hlam := lam_mul P hp2
  have hl1 := lam_one P ⟨hp2, hp23, hp3⟩
  unfold AInd at hA
  obtain ⟨-, a2, a3, -⟩ := hA
  have k1 := mul_le_mul_of_nonneg_left a3 (show (0 : ℝ) ≤ 2 * lam P - 1 by linarith)
  have hk : lam P * P.p₂ * M 8 = P.p₃ * M 8 := by rw [hlam]
  have hk2 := mul_nonneg hp2.le (n 8)
  have hl4 := mul_nonneg hl (n 4)
  unfold chiS10 chiO10 chiOs10 chiOx10 chiOu10
  linarith [n 0, n 5]

theorem chi_excl (P : Par) (hP : P.Standing) (M : Fin 10 → ℝ) (hM : 0 ≤ M)
    (h : M 0 = 0 ∧ M 1 = 0 ∧ M 2 = 0 ∧ M 3 = 0 ∧ M 4 = 0) :
    (1 - P.p₃) * chiO10 P M ≤ chiS10 P M := by
  obtain ⟨h0, h1, h2, h3, h4⟩ := h
  obtain ⟨hp2, hp23, hp3⟩ := standing_hp P hP
  have n : ∀ i, (0 : ℝ) ≤ M i := fun i => hM i
  unfold chiS10 chiO10 chiOs10 chiOx10 chiOu10
  rw [h0, h2, h3, h4]
  have c5 : 0 ≤ (1 - (1 - P.p₃) / 2) * M 5 := mul_nonneg (by linarith) (n 5)
  have c6 : 0 ≤ P.p₃ * M 6 := mul_nonneg (by linarith) (n 6)
  have c7 : 0 ≤ (P.p₃ - P.p₂) * M 7 := mul_nonneg (by linarith) (n 7)
  have c8 : 0 ≤ ((1 - P.p₃) * P.p₂) * M 8 :=
    mul_nonneg (mul_nonneg (by linarith) hp2.le) (n 8)
  have c9 : 0 ≤ ((1 - P.p₃) * P.p₃) * M 9 :=
    mul_nonneg (mul_nonneg (by linarith) (by linarith)) (n 9)
  linarith

/-- `lem:rsc-messages` (a)–(d), for every node of every ordered labelled tree. -/
theorem rsc_messages (P : Par) (hP : P.Standing) (t : RTree FLabel)
    (hc : AllLabels (fun a : FLabel => a.1.2.1 + a.1.2.2 ≤ a.1.1) t) :
    let M := message10 P t
    (forcing t ≠ some .excl →
      P.p₂ / 2 * (M 5 + M 6) ≤ M 1 ∧ P.p₂ / 2 * M 7 ≤ M 2 ∧
      P.p₂ / 2 * M 8 ≤ M 3 ∧ P.p₂ / 2 * M 9 ≤ M 4) ∧
    (forcing t ≠ some .out → (∀ c ∈ kids t, forcing c ≠ some .excl) →
      M 1 + M 2 + M 3 + M 4 ≤ P.p₂ / P.y * M 0) ∧
    (forcing t ≠ some .out → (∀ c ∈ kids t, forcing c ≠ some .excl) →
      chiS10 P M ≤ bconst P.p₂ P.p₃ P.y * chiO10 P M) ∧
    (forcing t ≠ some .excl → chiO10 P M ≤ chiS10 P M) ∧
    (forcing t = some .excl → (1 - P.p₃) * chiO10 P M ≤ chiS10 P M) := by
  intro M
  exact ⟨fun hf => AInd_tree P hP t hc hf,
    fun hf hk => BInd_tree P hP t hc hf hk,
    fun hf hk => chi_bound P hP (message10 P t) (msg_nonneg P hP t) (BInd_tree P hP t hc hf hk),
    fun hf => chi_compare P hP (message10 P t) (msg_nonneg P hP t) (AInd_tree P hP t hc hf),
    fun hf => chi_excl P hP (message10 P t) (msg_nonneg P hP t) (low_tree P t hf)⟩

end
end MaxLeafFormal.RSCRec