MaxLeafFormal.RSCTreeGen

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

import MaxLeafFormal.RSCTreeDefs

/-!
# A generic ten-state recursion (proof machinery for the tree model)

The closure probability of a candidate `v` is `g b j`, where `b` says that `v` is not the root and
its parent is sampled, and `j` is the number of sampled children of `v`. With
`g b j = p_{j + [b]}` this is the tree model of `def:rsc-tm` (`gPk`); with `g true j = p₃` for
`j ≥ 2` and `p₂` otherwise it is the relaxed model `p̃` of `sec:rsc-cert` (`gRel`). The recursion
`recursionG` is the proof of `lem:rsc-recursion`, written once for both.
-/

namespace MaxLeafFormal.RSCTree
open Finset
open MaxLeafFormal.Antinorm8 (RTree)
open MaxLeafFormal.RSCCert (Label)
open MaxLeafFormal.RSCRec
open MaxLeafFormal.Antinorm3 (children D)
open MaxLeafFormal.CDS (par comp)

noncomputable section
open Classical

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

/-- The two closure-probability functions. -/
def gPk (P : Par) (b : Bool) (j : ℕ) : ℝ := pk P.p₂ P.p₃ (j + if b then 1 else 0)

def gRel (P : Par) (b : Bool) (j : ℕ) : ℝ := if b = true ∧ 2 ≤ j then P.p₃ else P.p₂

/-- `[v ≠ r ∧ par v ∈ X']` and `|X' ∩ children v|`. -/
def bpar {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (X' : Finset Vt) (v : Vt) : Bool :=
  decide (v ≠ r ∧ par hF r v ∈ X')

def jch {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (X' : Finset Vt) (v : Vt) : ℕ :=
  (X' ∩ children hF r v).card

/-- The weight of `(X', Υ)` with closure probabilities `g`. -/
def wtG (P : Par) (g : Bool → ℕ → ℝ) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (lab : Vt → Label) (X' Υ : Finset Vt) : ℝ :=
  P.y ^ X'.card * prodMeas (fun v => g (bpar hF r X' v) (jch hF r X' v)) (candF F X') Υ
    * (1/2 : ℝ) ^ psiF F (X' ∪ Υ) * ∏ v, hhat P lab v (X' ∪ Υ)

def wsumG (P : Par) (g : Bool → ℕ → ℝ) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
    (lab : Vt → Label) (E : Finset Vt → Finset Vt → Prop) : ℝ :=
  ∑ X' : Finset Vt, ∑ Υ ∈ (candF F X').powerset, if E X' Υ then wtG P g hF r lab X' Υ else 0

/-- The functionals and the merge with closure probabilities `g` (`q = 1 - g`). -/
def chiSG (P : Par) (g : Bool → ℕ → ℝ) (Q : Fin 10 → ℝ) : ℝ :=
  2 * Q 0 + 2 * (g true 1 / P.p₂) * Q 2 + 2 * (g true 2 / P.p₂) * Q 3
    + 2 * (g true 3 / P.p₂) * Q 4 + Q 5 + Q 6 + (1 - g true 1) * Q 7 + (1 - g true 2) * Q 8
    + (1 - g true 3) * Q 9

def chiCuG (P : Par) (g : Bool → ℕ → ℝ) (Q : Fin 10 → ℝ) : ℝ :=
  2 * (g false 2 / P.p₂) * Q 3 + 2 * (g false 3 / P.p₂) * Q 4 + Q 5 + Q 6 + Q 7
    + (1 - g false 2) * Q 8 + (1 - g false 3) * Q 9

def chiOxG (P : Par) (g : Bool → ℕ → ℝ) (Q : Fin 10 → ℝ) : ℝ :=
  (g false 2 / P.p₂) * Q 3 + (g false 3 / P.p₂) * Q 4

def chiOuG (g : Bool → ℕ → ℝ) (Q : Fin 10 → ℝ) : ℝ :=
  Q 5 / 2 + Q 6 + Q 7 + (1 - g false 2) * Q 8 + (1 - g false 3) * Q 9

def mergeG (P : Par) (g : Bool → ℕ → ℝ) (M Q : Fin 10 → ℝ) : Fin 10 → ℝ :=
  ![M 0 * chiSG P g Q,
    M 1 * chiCuG P g Q,
    M 2 * chiCuG P g Q + M 1 * chiCs10 Q,
    M 3 * chiCuG P g Q + M 2 * chiCs10 Q,
    M 4 * (chiCuG P g Q + chiCs10 Q) + M 3 * chiCs10 Q,
    M 5 * chiOuG g Q,
    M 6 * (chiOuG g Q + chiOxG P g Q) + M 5 * chiOxG P g Q,
    M 7 * (chiOuG g Q + chiOxG P g Q) + (M 5 + M 6) * chiOs10 Q,
    M 8 * (chiOuG g Q + chiOxG P g Q) + M 7 * chiOs10 Q,
    M 9 * (chiOuG g Q + chiOxG P g Q + chiOs10 Q) + M 8 * chiOs10 Q]

mutual

def messageG (P : Par) (g : Bool → ℕ → ℝ) : RTree FLabel → Fin 10 → ℝ
  | .node ((ν, c₂, c₃), f) cs => mergeAllG P g (initF P ν c₂ c₃ f) cs

def mergeAllG (P : Par) (g : Bool → ℕ → ℝ) : (Fin 10 → ℝ) → List (RTree FLabel) → Fin 10 → ℝ
  | M, [] => M
  | M, c :: cs => mergeAllG P g (mergeG P g M (messageG P g c)) cs
end

/-! ### Proof machinery: the merge on basis vectors -/

/-- The basis vector of a state. -/
def eB (i : Fin 10) : Fin 10 → ℝ := Pi.single i 1

/-- The coefficient of `e_i ∘ e_j`: the completing factor of a child in state `j` (with the edge
factor) when its parent is in state `i`; it depends on `i` only through the status of the
parent (sampled, in `Υ`, out). -/
def cfG (P : Par) (g : Bool → ℕ → ℝ) (i j : Fin 10) : ℝ :=
  if i = 0 then
    (![2, 0, 2 * (g true 1 / P.p₂), 2 * (g true 2 / P.p₂), 2 * (g true 3 / P.p₂), 1, 1,
      1 - g true 1, 1 - g true 2, 1 - g true 3] : Fin 10 → ℝ) j
  else if i.val < 5 then
    (![2, 0, 0, 2 * (g false 2 / P.p₂), 2 * (g false 3 / P.p₂), 1, 1, 1, 1 - g false 2,
      1 - g false 3] : Fin 10 → ℝ) j
  else
    (![1, 0, 0, g false 2 / P.p₂, g false 3 / P.p₂, 1/2, 1, 1, 1 - g false 2,
      1 - g false 3] : Fin 10 → ℝ) j

/-- The new state of the parent. -/
def trG (i j : Fin 10) : Fin 10 :=
  if i = 0 then 0
  else if i.val < 5 then
    (if j = 0 then (if i = 1 then 2 else if i = 2 then 3 else 4) else i)
  else if j = 0 then (if i = 7 then 8 else if 8 ≤ i.val then 9 else 7)
  else if j.val < 5 then (if i = 5 then 6 else i)
  else i

theorem mergeG_eB_0 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 0) (eB j) = cfG P g 0 j • eB (trG 0 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_1 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 1) (eB j) = cfG P g 1 j • eB (trG 1 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_2 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 2) (eB j) = cfG P g 2 j • eB (trG 2 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_3 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 3) (eB j) = cfG P g 3 j • eB (trG 3 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_4 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 4) (eB j) = cfG P g 4 j • eB (trG 4 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_5 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 5) (eB j) = cfG P g 5 j • eB (trG 5 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_6 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 6) (eB j) = cfG P g 6 j • eB (trG 6 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_7 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 7) (eB j) = cfG P g 7 j • eB (trG 7 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_8 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 8) (eB j) = cfG P g 8 j • eB (trG 8 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB_9 (P : Par) (g : Bool → ℕ → ℝ) (j : Fin 10) :
    mergeG P g (eB 9) (eB j) = cfG P g 9 j • eB (trG 9 j) := by
  funext k
  fin_cases j <;> fin_cases k <;>
    simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10, eB, cfG, trG]

theorem mergeG_eB (P : Par) (g : Bool → ℕ → ℝ) (i j : Fin 10) :
    mergeG P g (eB i) (eB j) = cfG P g i j • eB (trG i j) := by
  fin_cases i
  · exact mergeG_eB_0 P g j
  · exact mergeG_eB_1 P g j
  · exact mergeG_eB_2 P g j
  · exact mergeG_eB_3 P g j
  · exact mergeG_eB_4 P g j
  · exact mergeG_eB_5 P g j
  · exact mergeG_eB_6 P g j
  · exact mergeG_eB_7 P g j
  · exact mergeG_eB_8 P g j
  · exact mergeG_eB_9 P g j

theorem mergeG_add_left (P : Par) (g : Bool → ℕ → ℝ) (M M' Q : Fin 10 → ℝ) :
    mergeG P g (M + M') Q = mergeG P g M Q + mergeG P g M' Q := by
  funext k
  fin_cases k <;> simp [mergeG] <;> ring

theorem mergeG_add_right (P : Par) (g : Bool → ℕ → ℝ) (M Q Q' : Fin 10 → ℝ) :
    mergeG P g M (Q + Q') = mergeG P g M Q + mergeG P g M Q' := by
  funext k
  fin_cases k <;> simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10] <;> ring

theorem mergeG_smul_left (P : Par) (g : Bool → ℕ → ℝ) (a : ℝ) (M Q : Fin 10 → ℝ) :
    mergeG P g (a • M) Q = a • mergeG P g M Q := by
  funext k
  fin_cases k <;> simp [mergeG] <;> ring

theorem mergeG_smul_right (P : Par) (g : Bool → ℕ → ℝ) (a : ℝ) (M Q : Fin 10 → ℝ) :
    mergeG P g M (a • Q) = a • mergeG P g M Q := by
  funext k
  fin_cases k <;> simp [mergeG, chiSG, chiCuG, chiOxG, chiOuG, chiCs10, chiOs10] <;> ring

theorem mergeG_zero_left (P : Par) (g : Bool → ℕ → ℝ) (Q : Fin 10 → ℝ) :
    mergeG P g 0 Q = 0 := by
  simpa using mergeG_smul_left P g 0 0 Q

theorem mergeG_zero_right (P : Par) (g : Bool → ℕ → ℝ) (M : Fin 10 → ℝ) :
    mergeG P g M 0 = 0 := by
  simpa using mergeG_smul_right P g 0 M 0

theorem mergeG_sum_left (P : Par) (g : Bool → ℕ → ℝ) {ι : Type*} (s : Finset ι)
    (f : ι → Fin 10 → ℝ) (Q : Fin 10 → ℝ) :
    mergeG P g (∑ i ∈ s, f i) Q = ∑ i ∈ s, mergeG P g (f i) Q := by
  induction s using Finset.induction_on with
  | empty => simp [mergeG_zero_left]
  | insert a s ha ih => rw [sum_insert ha, sum_insert ha, mergeG_add_left, ih]

theorem mergeG_sum_right (P : Par) (g : Bool → ℕ → ℝ) {ι : Type*} (s : Finset ι)
    (M : Fin 10 → ℝ) (f : ι → Fin 10 → ℝ) :
    mergeG P g M (∑ i ∈ s, f i) = ∑ i ∈ s, mergeG P g M (f i) := by
  induction s using Finset.induction_on with
  | empty => simp [mergeG_zero_right]
  | insert a s ha ih => rw [sum_insert ha, sum_insert ha, mergeG_add_right, ih]

theorem mergeG_smul_eB (P : Par) (g : Bool → ℕ → ℝ) (a b : ℝ) (i j : Fin 10) :
    mergeG P g (a • eB i) (b • eB j) = (a * b * cfG P g i j) • eB (trG i j) := by
  rw [mergeG_smul_left, mergeG_smul_right, mergeG_eB, smul_smul, smul_smul, mul_assoc]

/-! ### Local factors -/

section Local

variable (P : Par) (g : Bool → ℕ → ℝ) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
  (lab : Vt → Label)

/-- The complete local factor of `x` in the configuration `(X', U)`. -/
def phiG (x : Vt) (X' U : Finset Vt) : ℝ :=
  (if x ∈ X' then P.y else 1)
  * (if x ∈ U then (if 2 ≤ kF F X' x then g (bpar hF r X' x) (jch hF r X' x) else 0)
      else if x ∉ X' ∧ 2 ≤ kF F X' x then 1 - g (bpar hF r X' x) (jch hF r X' x) else 1)
  * (if x ∈ X' ∪ U ∧ ¬ (x ≠ r ∧ par hF r x ∈ X' ∪ U) then (1/2 : ℝ) else 1)
  * (if x ∉ X' ∪ U ∧ ∀ u, F.Adj x u → u ∉ X' ∪ U then (1/2 : ℝ) else 1)
  * hhat P lab x (X' ∪ U)

/-- The partial local factor of the top vertex `x` of a partial subtree. -/
def psiG (x : Vt) (X' U : Finset Vt) : ℝ :=
  if x ∈ X' then (1 - P.p₂) ^ (lab x).2.1 * (1 - P.p₃) ^ (lab x).2.2 * (P.y / 2)
  else if x ∈ U then (1 - P.p₂) ^ (lab x).2.1 * (1 - P.p₃) ^ (lab x).2.2 * (P.p₂ / 2)
  else (1/2 : ℝ) ^ (lab x).1 * P.ϖ₂ ^ (lab x).2.1 * P.ϖ₃ ^ (lab x).2.2

/-- The state of `x` in the configuration `(X', U)`. -/
def sttG (x : Vt) (X' U : Finset Vt) : Fin 10 :=
  if x ∈ X' then 0
  else if x ∈ U then
    (if jch hF r X' x = 0 then 1 else if jch hF r X' x = 1 then 2
      else if jch hF r X' x = 2 then 3 else 4)
  else if jch hF r X' x = 0 then (if (U ∩ children hF r x).Nonempty then 6 else 5)
  else if jch hF r X' x = 1 then 7 else if jch hF r X' x = 2 then 8 else 9

theorem adj_of_mem_children {x c : Vt} (h : c ∈ children hF r x) : F.Adj x c := by
  obtain ⟨hcr, hp⟩ := (Antinorm3.mem_children hF r).1 h
  have := (CDS.par_spec hF r hcr).1
  rw [hp] at this
  exact this.symm

theorem par_not_mem_children {x : Vt} (h : x ≠ r) : par hF r x ∉ children hF r x := by
  intro hc
  have h1 := Antinorm3.dist_child hF r hc
  have h2 := (CDS.par_spec hF r h).2
  omega

theorem kF_eq_jchG (X : Finset Vt) (x : Vt) :
    kF F X x = jch hF r X x + (if x ≠ r ∧ par hF r x ∈ X then 1 else 0) := by
  unfold kF jch
  have e : X.filter (F.Adj x)
      = (X ∩ children hF r x) ∪ X.filter (fun u => x ≠ r ∧ par hF r x = u) := by
    ext u
    simp only [mem_filter, mem_union, mem_inter, Antinorm3.mem_children]
    rw [CDS.adj_iff_par hF r]
    tauto
  rw [e, card_union_of_disjoint]
  · congr 1
    split_ifs with h
    · rw [card_eq_one]
      refine ⟨par hF r x, ?_⟩
      ext u
      simp only [mem_filter, mem_singleton]
      constructor
      · rintro ⟨_, _, rfl⟩; rfl
      · rintro rfl; exact ⟨h.2, h.1, rfl⟩
    · rw [card_eq_zero, filter_eq_empty_iff]
      rintro u hu ⟨hx, rfl⟩
      exact h ⟨hx, hu⟩
  · rw [disjoint_left]
    rintro u hu hu'
    obtain ⟨hx, rfl⟩ := (mem_filter.1 hu').2
    exact par_not_mem_children hF r hx (mem_inter.1 hu).2

theorem phiG_congr {x : Vt} {X₁ U₁ X₂ U₂ : Finset Vt}
    (h : ∀ u, (u = x ∨ F.Adj x u) → ((u ∈ X₁ ↔ u ∈ X₂) ∧ (u ∈ U₁ ↔ u ∈ U₂))) :
    phiG P g hF r lab x X₁ U₁ = phiG P g hF r lab x X₂ U₂ := by
  have hx := h x (Or.inl rfl)
  have hk : kF F X₁ x = kF F X₂ x := by
    unfold kF; congr 1; ext u; simp only [mem_filter]
    constructor
    · rintro ⟨hu, ha⟩; exact ⟨(h u (Or.inr ha)).1.1 hu, ha⟩
    · rintro ⟨hu, ha⟩; exact ⟨(h u (Or.inr ha)).1.2 hu, ha⟩
  have hj : jch hF r X₁ x = jch hF r X₂ x := by
    unfold jch; congr 1; ext u; simp only [mem_inter]
    constructor
    · rintro ⟨hu, hc⟩; exact ⟨(h u (Or.inr (adj_of_mem_children hF r hc))).1.1 hu, hc⟩
    · rintro ⟨hu, hc⟩; exact ⟨(h u (Or.inr (adj_of_mem_children hF r hc))).1.2 hu, hc⟩
  have hp : (x ≠ r ∧ par hF r x ∈ X₁) ↔ (x ≠ r ∧ par hF r x ∈ X₂) := by
    constructor
    · rintro ⟨hr, hm⟩; exact ⟨hr, (h _ (Or.inr (CDS.par_spec hF r hr).1)).1.1 hm⟩
    · rintro ⟨hr, hm⟩; exact ⟨hr, (h _ (Or.inr (CDS.par_spec hF r hr).1)).1.2 hm⟩
  have hb : bpar hF r X₁ x = bpar hF r X₂ x := by
    unfold bpar; exact decide_eq_decide.2 hp
  have hpU : (x ≠ r ∧ par hF r x ∈ X₁ ∪ U₁) ↔ (x ≠ r ∧ par hF r x ∈ X₂ ∪ U₂) := by
    simp only [mem_union]
    constructor
    · rintro ⟨hr, hm⟩
      obtain ⟨h1, h2⟩ := h _ (Or.inr (CDS.par_spec hF r hr).1)
      exact ⟨hr, hm.imp h1.1 h2.1⟩
    · rintro ⟨hr, hm⟩
      obtain ⟨h1, h2⟩ := h _ (Or.inr (CDS.par_spec hF r hr).1)
      exact ⟨hr, hm.imp h1.2 h2.2⟩
  have hd : (∀ u, F.Adj x u → u ∉ X₁ ∪ U₁) ↔ (∀ u, F.Adj x u → u ∉ X₂ ∪ U₂) := by
    simp only [mem_union, not_or]
    constructor
    · intro H u hu
      obtain ⟨h1, h2⟩ := h u (Or.inr hu)
      obtain ⟨a, b⟩ := H u hu
      exact ⟨fun h' => a (h1.2 h'), fun h' => b (h2.2 h')⟩
    · intro H u hu
      obtain ⟨h1, h2⟩ := h u (Or.inr hu)
      obtain ⟨a, b⟩ := H u hu
      exact ⟨fun h' => a (h1.1 h'), fun h' => b (h2.1 h')⟩
  have hxX : x ∈ X₁ ∪ U₁ ↔ x ∈ X₂ ∪ U₂ := by rw [mem_union, mem_union, hx.1, hx.2]
  unfold phiG hhat
  rw [hk, hj, hb]
  simp only [hx.1, hx.2, hxX, hpU, hd]

theorem sttG_zero_iff (x : Vt) (X U : Finset Vt) : sttG hF r x X U = 0 ↔ x ∈ X := by
  unfold sttG; split_ifs <;> simp_all

theorem sttG_lt5_iff (x : Vt) (X U : Finset Vt) :
    (sttG hF r x X U).val < 5 ↔ (x ∈ X ∨ x ∈ U) := by
  unfold sttG; split_ifs <;> simp_all

theorem prod_phiG {X' U : Finset Vt} (hd : Disjoint X' U) :
    ∏ x, phiG P g hF r lab x X' U = if U ⊆ candF F X' then wtG P g hF r lab X' U else 0 := by
  split_ifs with hU
  · unfold phiG wtG prodMeas psiF
    simp only [prod_mul_distrib]
    rw [Antinorm3.comp_eq_tops hF r]
    have e1 : ∏ x, (if x ∈ X' then P.y else 1) = P.y ^ X'.card := by
      rw [prod_ite_mem univ X' (fun _ => P.y)]; simp
    have e2 : ∏ x, (if x ∈ U then (if 2 ≤ kF F X' x then g (bpar hF r X' x) (jch hF r X' x)
          else 0) else if x ∉ X' ∧ 2 ≤ kF F X' x then 1 - g (bpar hF r X' x) (jch hF r X' x)
          else 1)
        = (∏ x ∈ U, g (bpar hF r X' x) (jch hF r X' x))
          * ∏ x ∈ candF F X' \ U, (1 - g (bpar hF r X' x) (jch hF r X' x)) := by
      have hx : ∀ x, (if x ∈ U then (if 2 ≤ kF F X' x then g (bpar hF r X' x) (jch hF r X' x)
          else 0) else if x ∉ X' ∧ 2 ≤ kF F X' x then 1 - g (bpar hF r X' x) (jch hF r X' x)
          else 1)
          = (if x ∈ U then g (bpar hF r X' x) (jch hF r X' x) else 1)
            * (if x ∈ candF F X' \ U then 1 - g (bpar hF r X' x) (jch hF r X' x) else 1) := by
        intro x
        by_cases hxU : x ∈ U
        · have := hU hxU
          simp only [candF, mem_filter, mem_univ, true_and] at this
          simp [hxU, this.2]
        · simp [hxU, candF, mem_sdiff]
      rw [prod_congr rfl (fun x _ => hx x), prod_mul_distrib, prod_ite_mem, prod_ite_mem,
        univ_inter, univ_inter]
    have e3 : ∏ x, (if x ∈ X' ∪ U ∧ ¬ (x ≠ r ∧ par hF r x ∈ X' ∪ U) then (1/2 : ℝ) else 1)
        = (1/2 : ℝ) ^ (Antinorm3.tops hF r (X' ∪ U)).card := by
      rw [← prod_filter, prod_const]
      congr 2
      ext x
      simp [Antinorm3.tops]
    have e4 : ∏ x, (if x ∉ X' ∪ U ∧ ∀ u, F.Adj x u → u ∉ X' ∪ U then (1/2 : ℝ) else 1)
        = (1/2 : ℝ) ^ (univ.filter (fun v => v ∉ X' ∪ U ∧ ∀ u, F.Adj v u → u ∉ X' ∪ U)).card := by
      rw [← prod_filter, prod_const]
    rw [e1, e2, e3, e4, pow_add]
    ring
  · obtain ⟨x, hxU, hxc⟩ := not_subset.1 hU
    apply prod_eq_zero (mem_univ x)
    have hxX : x ∉ X' := fun h => disjoint_left.1 hd h hxU
    have : ¬ 2 ≤ kF F X' x := fun h => hxc (by simp [candF, hxX, h])
    simp [phiG, hxU, this]

set_option maxHeartbeats 400000 in

theorem phiG_child (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    {A B : Finset Vt} {v w : Vt} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
    (hwr : w ≠ r) (hpw : par hF r w = v) (hwA : ∀ u ∈ A, F.Adj w u → u = v)
    {Y₁ U₁ Y₂ U₂ : Finset Vt} (hY₁ : Y₁ ⊆ A) (hU₁ : U₁ ⊆ A) (hY₂ : Y₂ ⊆ B) (hU₂ : U₂ ⊆ B)
    (hd₁ : Disjoint Y₁ U₁) (hd₂ : Disjoint Y₂ U₂) :
    phiG P g hF r lab w (Y₁ ∪ Y₂) (U₁ ∪ U₂)
      = psiG P lab w Y₂ U₂ * cfG P g (sttG hF r v Y₁ U₁) (sttG hF r w Y₂ U₂) := by
  have hwA' : w ∉ A := fun h => disjoint_left.1 hAB h hw
  have hvB : v ∉ B := fun h => disjoint_left.1 hAB hv h
  have hcA : ∀ c ∈ children hF r w, c ∉ A := by
    intro c hc hcA
    have := hwA c hcA (adj_of_mem_children hF r hc)
    rw [this, ← hpw] at hc
    exact par_not_mem_children hF r hwr hc
  have hwY : w ∈ Y₁ ∪ Y₂ ↔ w ∈ Y₂ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_left (fun h' => hwA' (hY₁ h')), Or.inr⟩
  have hwU : w ∈ U₁ ∪ U₂ ↔ w ∈ U₂ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_left (fun h' => hwA' (hU₁ h')), Or.inr⟩
  have hvY : v ∈ Y₁ ∪ Y₂ ↔ v ∈ Y₁ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_right (fun h' => hvB (hY₂ h')), Or.inl⟩
  have hvU : v ∈ U₁ ∪ U₂ ↔ v ∈ U₁ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_right (fun h' => hvB (hU₂ h')), Or.inl⟩
  have hj : jch hF r (Y₁ ∪ Y₂) w = jch hF r Y₂ w := by
    unfold jch; congr 1; ext c; simp only [mem_inter, mem_union]
    constructor
    · rintro ⟨h | h, hc⟩
      · exact absurd (hY₁ h) (hcA c hc)
      · exact ⟨h, hc⟩
    · rintro ⟨h, hc⟩; exact ⟨Or.inr h, hc⟩
  have hk : kF F (Y₁ ∪ Y₂) w = jch hF r Y₂ w + (if v ∈ Y₁ then 1 else 0) := by
    rw [kF_eq_jchG hF r, hj, hpw]
    simp only [hvY, ne_eq, hwr, not_false_eq_true, true_and]
  have hb : bpar hF r (Y₁ ∪ Y₂) w = decide (v ∈ Y₁) := by
    unfold bpar; rw [hpw]; simp only [hvY, ne_eq, hwr, not_false_eq_true, true_and]
  have htop : (w ≠ r ∧ par hF r w ∈ Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂)) ↔ (v ∈ Y₁ ∨ v ∈ U₁) := by
    rw [hpw, mem_union, hvY, hvU]; simp [hwr]
  have hwX : w ∈ Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂) ↔ (w ∈ Y₂ ∨ w ∈ U₂) := by rw [mem_union, hwY, hwU]
  have hdom : (∀ u, F.Adj w u → u ∉ Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂)) ↔
      ((v ∉ Y₁ ∧ v ∉ U₁) ∧ jch hF r Y₂ w = 0 ∧ ¬ (U₂ ∩ children hF r w).Nonempty) := by
    constructor
    · intro H
      have hv' := H v (hpw ▸ (CDS.par_spec hF r hwr).1)
      rw [mem_union, hvY, hvU, not_or] at hv'
      refine ⟨hv', ?_, ?_⟩
      · unfold jch; rw [card_eq_zero, eq_empty_iff_forall_notMem]
        intro c hc; rw [mem_inter] at hc
        exact H c (adj_of_mem_children hF r hc.2) (by simp [hc.1])
      · rintro ⟨c, hc⟩; rw [mem_inter] at hc
        exact H c (adj_of_mem_children hF r hc.2) (by simp [hc.1])
    · rintro ⟨hv', hj0, hn⟩ u hu
      rcases (CDS.adj_iff_par hF r).1 hu with ⟨-, hpu⟩ | ⟨hur, hpu⟩
      · rw [← hpu, hpw, mem_union, hvY, hvU]; exact fun h => h.elim hv'.1 hv'.2
      · have hc : u ∈ children hF r w := (Antinorm3.mem_children hF r).2 ⟨hur, hpu⟩
        have huA : u ∉ A := hcA u hc
        unfold jch at hj0; rw [card_eq_zero] at hj0
        simp only [mem_union, not_or]
        refine ⟨⟨fun h => huA (hY₁ h), fun h => ?_⟩, fun h => huA (hU₁ h),
          fun h => hn ⟨u, mem_inter.2 ⟨h, hc⟩⟩⟩
        have : u ∈ Y₂ ∩ children hF r w := mem_inter.2 ⟨h, hc⟩
        rw [hj0] at this; simp at this
  have hh : hhat P lab w (Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂)) = hhat P lab w (Y₂ ∪ U₂) := by
    simp only [hhat, hwX, mem_union]
  have hs0 := sttG_zero_iff hF r v Y₁ U₁
  have hs5 := sttG_lt5_iff hF r v Y₁ U₁
  have hdw : ¬ (w ∈ Y₂ ∧ w ∈ U₂) := fun h => disjoint_left.1 hd₂ h.1 h.2
  have hdv : ¬ (v ∈ Y₁ ∧ v ∈ U₁) := fun h => disjoint_left.1 hd₁ h.1 h.2
  unfold phiG
  rw [hk, hj, hb, hh]
  simp only [hwY, hwU, hwX, htop, hdom]
  unfold cfG
  simp only [hs0, hs5]
  unfold psiG sttG hhat
  generalize jch hF r Y₂ w = j
  by_cases a1 : v ∈ Y₁ <;> by_cases a2 : v ∈ U₁ <;> by_cases b1 : w ∈ Y₂ <;>
    by_cases b2 : w ∈ U₂ <;>
    simp only [a1, a2, b1, b2, and_self, not_true_eq_false] at hdv hdw
  all_goals
    rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ 3 ≤ j by omega) with rfl | rfl | rfl | hj
    · by_cases hn : (U₂ ∩ children hF r w).Nonempty <;> simp [hn, a1, a2, b1, b2] <;>
        (try field_simp) <;> (try ring)
    · simp [a1, a2, b1, b2] <;> (try field_simp) <;> (try ring)
    · simp [a1, a2, b1, b2] <;> (try field_simp) <;> (try ring)
    · have h0 : j ≠ 0 := by omega
      have h1 : j ≠ 1 := by omega
      have h2 : j ≠ 2 := by omega
      have h3 : 2 ≤ j := by omega
      have h4 : 2 ≤ j + 1 := by omega
      have hg3 : ∀ b, g b j = g b 3 := fun b => hg b j hj
      simp [a1, a2, b1, b2, h0, h1, h2, h3, h4, hg3] <;> (try field_simp) <;> (try ring)

theorem sttG_parent {A B : Finset Vt} {v w : Vt} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
    (hvB : ∀ u ∈ B, F.Adj v u → u = w) (hwr : w ≠ r) (hpw : par hF r w = v)
    {Y₁ U₁ Y₂ U₂ : Finset Vt} (hY₁ : Y₁ ⊆ A) (hU₁ : U₁ ⊆ A) (hY₂ : Y₂ ⊆ B) (hU₂ : U₂ ⊆ B)
    (hd₁ : Disjoint Y₁ U₁) (hd₂ : Disjoint Y₂ U₂) :
    sttG hF r v (Y₁ ∪ Y₂) (U₁ ∪ U₂) = trG (sttG hF r v Y₁ U₁) (sttG hF r w Y₂ U₂) := by
  have hvB' : v ∉ B := fun h => disjoint_left.1 hAB hv h
  have hwc : w ∈ children hF r v := (Antinorm3.mem_children hF r).2 ⟨hwr, hpw⟩
  have hcB : ∀ c ∈ children hF r v, c ∈ B → c = w :=
    fun c hc hcB => hvB c hcB (adj_of_mem_children hF r hc)
  have hvY : v ∈ Y₁ ∪ Y₂ ↔ v ∈ Y₁ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_right (fun h' => hvB' (hY₂ h')), Or.inl⟩
  have hvU : v ∈ U₁ ∪ U₂ ↔ v ∈ U₁ := by
    simp only [mem_union]; exact ⟨fun h => h.resolve_right (fun h' => hvB' (hU₂ h')), Or.inl⟩
  have hj : jch hF r (Y₁ ∪ Y₂) v = jch hF r Y₁ v + (if w ∈ Y₂ then 1 else 0) := by
    unfold jch
    rw [union_inter_distrib_right, card_union_of_disjoint (disjoint_of_subset_left
      inter_subset_left (disjoint_of_subset_right inter_subset_left
        (disjoint_of_subset_left hY₁ (disjoint_of_subset_right hY₂ hAB))))]
    congr 1
    split_ifs with h
    · rw [card_eq_one]
      refine ⟨w, ?_⟩
      ext c
      simp only [mem_inter, mem_singleton]
      constructor
      · rintro ⟨h1, h2⟩; exact hcB c h2 (hY₂ h1)
      · rintro rfl; exact ⟨h, hwc⟩
    · rw [card_eq_zero, eq_empty_iff_forall_notMem]
      intro c hc
      rw [mem_inter] at hc
      exact h (hcB c hc.2 (hY₂ hc.1) ▸ hc.1)
  have hn : ((U₁ ∪ U₂) ∩ children hF r v).Nonempty
      ↔ ((U₁ ∩ children hF r v).Nonempty ∨ w ∈ U₂) := by
    constructor
    · rintro ⟨c, hc⟩
      rw [mem_inter, mem_union] at hc
      rcases hc with ⟨h | h, hc⟩
      · exact Or.inl ⟨c, mem_inter.2 ⟨h, hc⟩⟩
      · right; rw [← hcB c hc (hU₂ h)]; exact h
    · rintro (⟨c, hc⟩ | h)
      · rw [mem_inter] at hc; exact ⟨c, mem_inter.2 ⟨mem_union_left _ hc.1, hc.2⟩⟩
      · exact ⟨w, mem_inter.2 ⟨mem_union_right _ h, hwc⟩⟩
  have hs0 := sttG_zero_iff hF r w Y₂ U₂
  have hs5 := sttG_lt5_iff hF r w Y₂ U₂
  have hdw : ¬ (w ∈ Y₂ ∧ w ∈ U₂) := fun h => disjoint_left.1 hd₂ h.1 h.2
  have hdv : ¬ (v ∈ Y₁ ∧ v ∈ U₁) := fun h => disjoint_left.1 hd₁ h.1 h.2
  unfold trG
  simp only [hs0, hs5]
  unfold sttG
  rw [hj]
  simp only [hvY, hvU, hn]
  generalize jch hF r Y₁ v = j
  by_cases hn : (U₁ ∩ children hF r v).Nonempty <;> by_cases a1 : v ∈ Y₁ <;>
    by_cases a2 : v ∈ U₁ <;> by_cases b1 : w ∈ Y₂ <;> by_cases b2 : w ∈ U₂ <;>
    simp only [a1, a2, b1, b2, and_self, not_true_eq_false] at hdv hdw
  all_goals
    rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ 3 ≤ j by omega) with rfl | rfl | rfl | hj
    · simp [hn, a1, a2, b1, b2]
    · simp [a1, a2, b1, b2]
    · simp [a1, a2, b1, b2]
    · have h0 : j ≠ 0 := by omega
      have h1 : j ≠ 1 := by omega
      have h2 : j ≠ 2 := by omega
      simp [a1, a2, b1, b2, h0, h1, h2]

theorem phiG_root (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    {Y U : Finset Vt} (hd : Disjoint Y U) :
    phiG P g hF r lab r Y U = psiG P lab r Y U * cfG P g 5 (sttG hF r r Y U) := by
  have hk : kF F Y r = jch hF r Y r := by rw [kF_eq_jchG hF r]; simp
  have hb : bpar hF r Y r = false := by simp [bpar]
  have hdom : (∀ u, F.Adj r u → u ∉ Y ∪ U) ↔
      (jch hF r Y r = 0 ∧ ¬ (U ∩ children hF r r).Nonempty) := by
    constructor
    · intro H
      refine ⟨?_, ?_⟩
      · unfold jch; rw [card_eq_zero, eq_empty_iff_forall_notMem]
        intro c hc; rw [mem_inter] at hc
        exact H c (adj_of_mem_children hF r hc.2) (mem_union_left _ hc.1)
      · rintro ⟨c, hc⟩; rw [mem_inter] at hc
        exact H c (adj_of_mem_children hF r hc.2) (mem_union_right _ hc.1)
    · rintro ⟨hj0, hn⟩ u hu
      rcases (CDS.adj_iff_par hF r).1 hu with ⟨h, -⟩ | ⟨hur, hpu⟩
      · exact absurd rfl h
      · have hc : u ∈ children hF r r := (Antinorm3.mem_children hF r).2 ⟨hur, hpu⟩
        unfold jch at hj0; rw [card_eq_zero] at hj0
        rw [mem_union, not_or]
        refine ⟨fun h => ?_, fun h => hn ⟨u, mem_inter.2 ⟨h, hc⟩⟩⟩
        have : u ∈ Y ∩ children hF r r := mem_inter.2 ⟨h, hc⟩
        rw [hj0] at this; simp at this
  have hdw : ¬ (r ∈ Y ∧ r ∈ U) := fun h => disjoint_left.1 hd h.1 h.2
  unfold phiG
  rw [hk, hb]
  simp only [hdom, ne_eq, not_true_eq_false, false_and, not_false_eq_true, and_true]
  unfold cfG psiG sttG hhat
  generalize jch hF r Y r = j
  by_cases b1 : r ∈ Y <;> by_cases b2 : r ∈ U <;>
    simp only [b1, b2, and_self, not_true_eq_false] at hdw
  all_goals
    rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ 3 ≤ j by omega) with rfl | rfl | rfl | hj
    · by_cases hn : (U ∩ children hF r r).Nonempty <;> simp [hn, b1, b2] <;>
        (try field_simp) <;> (try ring)
    · simp [b1, b2] <;> (try field_simp) <;> (try ring)
    · simp [b1, b2] <;> (try field_simp) <;> (try ring)
    · have h0 : j ≠ 0 := by omega
      have h1 : j ≠ 1 := by omega
      have h2 : j ≠ 2 := by omega
      have h3 : 2 ≤ j := by omega
      have hg3 : ∀ b, g b j = g b 3 := fun b => hg b j hj
      simp [b1, b2, h0, h1, h2, h3, hg3] <;> (try field_simp) <;> (try ring)

end Local

/-! ### Partial messages -/

section Msg

variable (P : Par) (g : Bool → ℕ → ℝ) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
  (lab : Vt → Label) (f : Vt → Option Force)

/-- `(X', U)` respects the forcing on `A`. -/
def RespOn (A X' U : Finset Vt) : Prop :=
  ∀ x ∈ A, (f x = some .inn → x ∈ X') ∧ (f x = some .out → x ∉ X') ∧
    (f x = some .excl → x ∉ X' ∪ U)

/-- The term of a partial configuration `(Y, U)` on `A` with top `v`. -/
def termP (A : Finset Vt) (v : Vt) (Y U : Finset Vt) : Fin 10 → ℝ :=
  if Disjoint Y U ∧ RespOn f A Y U then
    ((∏ x ∈ A.erase v, phiG P g hF r lab x Y U) * psiG P lab v Y U) • eB (sttG hF r v Y U)
  else 0

/-- The partial message of `A` with top `v`. -/
def msgP (A : Finset Vt) (v : Vt) : Fin 10 → ℝ :=
  ∑ Y ∈ A.powerset, ∑ U ∈ A.powerset, termP P g hF r lab f A v Y U

theorem msgP_single (v : Vt) :
    msgP P g hF r lab f {v} v = initF P (lab v).1 (lab v).2.1 (lab v).2.2 (f v) := by
  have hP : ({v} : Finset Vt).powerset = {∅, {v}} := by
    ext X; simp [subset_singleton_iff]
  have hj : jch hF r ∅ v = 0 := by simp [jch]
  unfold msgP
  rw [hP, sum_pair (by simp), sum_pair (by simp), sum_pair (by simp)]
  unfold termP
  simp only [erase_singleton, prod_empty, one_mul]
  funext i
  rcases hf : f v with _ | ⟨_ | _ | _⟩ <;>
    fin_cases i <;> simp [initF, init10, eB, RespOn, psiG, sttG, hj, hf]

theorem termP_split (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    {A B : Finset Vt} {v w : Vt} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
    (hwr : w ≠ r) (hpw : par hF r w = v)
    (hAc : ∀ x ∈ A, x ≠ v → ∀ u, F.Adj x u → u ∈ A)
    (hBc : ∀ x ∈ B, x ≠ w → ∀ u, F.Adj x u → u ∈ B)
    (hvB : ∀ u ∈ B, F.Adj v u → u = w) (hwA : ∀ u ∈ A, F.Adj w u → u = v)
    {Y₁ U₁ Y₂ U₂ : Finset Vt} (hY₁ : Y₁ ⊆ A) (hU₁ : U₁ ⊆ A) (hY₂ : Y₂ ⊆ B) (hU₂ : U₂ ⊆ B) :
    termP P g hF r lab f (A ∪ B) v (Y₁ ∪ Y₂) (U₁ ∪ U₂)
      = mergeG P g (termP P g hF r lab f A v Y₁ U₁) (termP P g hF r lab f B w Y₂ U₂) := by
  have mA : ∀ u ∈ A, (u ∈ Y₁ ∪ Y₂ ↔ u ∈ Y₁) ∧ (u ∈ U₁ ∪ U₂ ↔ u ∈ U₁) := by
    intro u hu
    have h1 : u ∉ Y₂ := fun h => disjoint_left.1 hAB hu (hY₂ h)
    have h2 : u ∉ U₂ := fun h => disjoint_left.1 hAB hu (hU₂ h)
    simp [mem_union, h1, h2]
  have mB : ∀ u ∈ B, (u ∈ Y₁ ∪ Y₂ ↔ u ∈ Y₂) ∧ (u ∈ U₁ ∪ U₂ ↔ u ∈ U₂) := by
    intro u hu
    have h1 : u ∉ Y₁ := fun h => disjoint_left.1 hAB (hY₁ h) hu
    have h2 : u ∉ U₁ := fun h => disjoint_left.1 hAB (hU₁ h) hu
    simp [mem_union, h1, h2]
  have hdisj : Disjoint (Y₁ ∪ Y₂) (U₁ ∪ U₂) ↔ Disjoint Y₁ U₁ ∧ Disjoint Y₂ U₂ := by
    rw [disjoint_union_left, disjoint_union_right, disjoint_union_right]
    have c1 : Disjoint Y₁ U₂ := disjoint_of_subset_left hY₁ (disjoint_of_subset_right hU₂ hAB)
    have c2 : Disjoint Y₂ U₁ :=
      disjoint_of_subset_left hY₂ (disjoint_of_subset_right hU₁ hAB.symm)
    constructor
    · rintro ⟨⟨a, _⟩, ⟨_, b⟩⟩; exact ⟨a, b⟩
    · rintro ⟨a, b⟩; exact ⟨⟨a, c1⟩, ⟨c2, b⟩⟩
  have eA : ∀ x ∈ A, ((f x = some .inn → x ∈ Y₁ ∪ Y₂) ∧ (f x = some .out → x ∉ Y₁ ∪ Y₂) ∧
      (f x = some .excl → x ∉ Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂))) ↔ ((f x = some .inn → x ∈ Y₁) ∧
      (f x = some .out → x ∉ Y₁) ∧ (f x = some .excl → x ∉ Y₁ ∪ U₁)) := by
    intro x hx
    have h1 : x ∉ Y₂ := fun h => disjoint_left.1 hAB hx (hY₂ h)
    have h2 : x ∉ U₂ := fun h => disjoint_left.1 hAB hx (hU₂ h)
    simp only [mem_union, h1, h2, or_false]
  have eB' : ∀ x ∈ B, ((f x = some .inn → x ∈ Y₁ ∪ Y₂) ∧ (f x = some .out → x ∉ Y₁ ∪ Y₂) ∧
      (f x = some .excl → x ∉ Y₁ ∪ Y₂ ∪ (U₁ ∪ U₂))) ↔ ((f x = some .inn → x ∈ Y₂) ∧
      (f x = some .out → x ∉ Y₂) ∧ (f x = some .excl → x ∉ Y₂ ∪ U₂)) := by
    intro x hx
    have h1 : x ∉ Y₁ := fun h => disjoint_left.1 hAB (hY₁ h) hx
    have h2 : x ∉ U₁ := fun h => disjoint_left.1 hAB (hU₁ h) hx
    simp only [mem_union, h1, h2, false_or]
  have hresp : RespOn f (A ∪ B) (Y₁ ∪ Y₂) (U₁ ∪ U₂) ↔ RespOn f A Y₁ U₁ ∧ RespOn f B Y₂ U₂ := by
    unfold RespOn
    constructor
    · intro H
      exact ⟨fun x hx => (eA x hx).1 (H x (mem_union_left _ hx)),
        fun x hx => (eB' x hx).1 (H x (mem_union_right _ hx))⟩
    · rintro ⟨H1, H2⟩ x hx
      rcases mem_union.1 hx with hx | hx
      · exact (eA x hx).2 (H1 x hx)
      · exact (eB' x hx).2 (H2 x hx)
  unfold termP
  by_cases h1 : Disjoint Y₁ U₁ ∧ RespOn f A Y₁ U₁
  · by_cases h2 : Disjoint Y₂ U₂ ∧ RespOn f B Y₂ U₂
    · rw [ite_eq_left ⟨hdisj.2 ⟨h1.1, h2.1⟩, hresp.2 ⟨h1.2, h2.2⟩⟩, ite_eq_left h1, ite_eq_left h2,
        mergeG_smul_eB, sttG_parent hF r hAB hv hw hvB hwr hpw hY₁ hU₁ hY₂ hU₂ h1.1 h2.1]
      congr 1
      have hvB' : v ∉ B := fun h => disjoint_left.1 hAB hv h
      rw [erase_union_distrib, erase_eq_of_notMem hvB',
        prod_union (disjoint_of_subset_left (erase_subset _ _) hAB), ← mul_prod_erase B _ hw]
      have pA : ∏ x ∈ A.erase v, phiG P g hF r lab x (Y₁ ∪ Y₂) (U₁ ∪ U₂)
          = ∏ x ∈ A.erase v, phiG P g hF r lab x Y₁ U₁ := by
        apply prod_congr rfl
        intro x hx
        apply phiG_congr
        intro u hu
        have huA : u ∈ A := by
          rcases hu with rfl | hu
          · exact mem_of_mem_erase hx
          · exact hAc x (mem_of_mem_erase hx) (ne_of_mem_erase hx) u hu
        exact mA u huA
      have pB : ∏ x ∈ B.erase w, phiG P g hF r lab x (Y₁ ∪ Y₂) (U₁ ∪ U₂)
          = ∏ x ∈ B.erase w, phiG P g hF r lab x Y₂ U₂ := by
        apply prod_congr rfl
        intro x hx
        apply phiG_congr
        intro u hu
        have huB : u ∈ B := by
          rcases hu with rfl | hu
          · exact mem_of_mem_erase hx
          · exact hBc x (mem_of_mem_erase hx) (ne_of_mem_erase hx) u hu
        exact mB u huB
      have pv : psiG P lab v (Y₁ ∪ Y₂) (U₁ ∪ U₂) = psiG P lab v Y₁ U₁ := by
        simp only [psiG, (mA v hv).1, (mA v hv).2]
      rw [pA, pB, pv,
        phiG_child P g hF r lab hp₂ hg hAB hv hw hwr hpw hwA hY₁ hU₁ hY₂ hU₂ h1.1 h2.1]
      ring
    · rw [ite_eq_right (fun h => h2 ⟨(hdisj.1 h.1).2, (hresp.1 h.2).2⟩), ite_eq_right h2, mergeG_zero_right]
  · rw [ite_eq_right (fun h => h1 ⟨(hdisj.1 h.1).1, (hresp.1 h.2).1⟩), ite_eq_right h1, mergeG_zero_left]

theorem msgP_split (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    {A B : Finset Vt} {v w : Vt} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
    (hwr : w ≠ r) (hpw : par hF r w = v)
    (hAc : ∀ x ∈ A, x ≠ v → ∀ u, F.Adj x u → u ∈ A)
    (hBc : ∀ x ∈ B, x ≠ w → ∀ u, F.Adj x u → u ∈ B)
    (hvB : ∀ u ∈ B, F.Adj v u → u = w) (hwA : ∀ u ∈ A, F.Adj w u → u = v) :
    msgP P g hF r lab f (A ∪ B) v
      = mergeG P g (msgP P g hF r lab f A v) (msgP P g hF r lab f B w) := by
  unfold msgP
  rw [Antinorm3.sum_powerset_union hAB, mergeG_sum_left]
  apply sum_congr rfl
  intro Y₁ hY₁
  simp_rw [Antinorm3.sum_powerset_union hAB]
  conv_lhs => rw [sum_comm]
  rw [mergeG_sum_left]
  apply sum_congr rfl
  intro U₁ hU₁
  rw [mergeG_sum_right]
  apply sum_congr rfl
  intro Y₂ hY₂
  rw [mergeG_sum_right]
  apply sum_congr rfl
  intro U₂ hU₂
  exact termP_split P g hF r lab f hp₂ hg hAB hv hw hwr hpw hAc hBc hvB hwA
    (mem_powerset.1 hY₁) (mem_powerset.1 hU₁) (mem_powerset.1 hY₂) (mem_powerset.1 hU₂)

end Msg

/-! ### Messages of subtrees and the root -/

section Tree

variable (P : Par) (g : Bool → ℕ → ℝ) {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt)
  (lab : Vt → Label) (f : Vt → Option Force)

theorem mergeAll_msgP (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3) (v : Vt)
    (T : Vt → RTree FLabel) :
    ∀ (l : List Vt) (S : Finset Vt), S ⊆ children hF r v → l.Nodup →
      (∀ w ∈ l, w ∈ children hF r v ∧ w ∉ S) →
      (∀ w ∈ l, messageG P g (T w) = msgP P g hF r lab f (D hF r w) w) →
      mergeAllG P g (msgP P g hF r lab f (insert v (S.biUnion (D hF r))) v) (l.map T)
        = msgP P g hF r lab f (insert v ((S ∪ l.toFinset).biUnion (D hF r))) v := by
  intro l
  induction l with
  | nil => intro S _ _ _ _; simp [mergeAllG]
  | cons w l ih =>
    intro S hS hl hlc hT
    have hwc := (hlc w (List.mem_cons_self ..)).1
    have hwS := (hlc w (List.mem_cons_self ..)).2
    obtain ⟨hwr, hpw⟩ := (Antinorm3.mem_children hF r).1 hwc
    have hwv : w ≠ v := by
      intro h
      have := (CDS.par_spec hF r hwr).1
      rw [hpw, h] at this
      exact F.loopless.irrefl _ this
    have hvD : v ∉ D hF r w := Antinorm3.not_mem_D_child hF r hwc
    have hsr : ∀ s ∈ S, s ≠ r ∧ par hF r s = v := fun s hs =>
      (Antinorm3.mem_children hF r).1 (hS hs)
    have hsw : ∀ s ∈ S, Disjoint (D hF r s) (D hF r w) := fun s hs =>
      Antinorm3.D_disjoint hF r (hS hs) hwc (fun h => hwS (h ▸ hs))
    rw [List.map_cons, mergeAllG, hT w (List.mem_cons_self ..)]
    rw [← msgP_split P g hF r lab f hp₂ hg (A := insert v (S.biUnion (D hF r)))
      (B := D hF r w) (v := v) (w := w)]
    · have e : insert v (S.biUnion (D hF r)) ∪ D hF r w
          = insert v ((insert w S).biUnion (D hF r)) := by
        rw [biUnion_insert]; ext u; simp only [mem_union, mem_insert]; tauto
      rw [e, ih (insert w S) (insert_subset hwc hS) (List.nodup_cons.1 hl).2
        (fun u hu => ⟨(hlc u (List.mem_cons_of_mem _ hu)).1, by
          rw [mem_insert, not_or]
          exact ⟨fun h => (List.nodup_cons.1 hl).1 (h ▸ hu), (hlc u (List.mem_cons_of_mem _ hu)).2⟩⟩)
        (fun u hu => hT u (List.mem_cons_of_mem _ hu))]
      congr 3
      ext u; simp only [mem_union, mem_insert, List.mem_toFinset, List.mem_cons]; tauto
    · rw [disjoint_insert_left, disjoint_biUnion_left]
      exact ⟨hvD, hsw⟩
    · exact mem_insert_self _ _
    · exact Antinorm3.self_mem_D hF r w
    · exact hwr
    · exact hpw
    · intro x hx hxv u hu
      rcases mem_insert.1 hx with rfl | hx
      · exact absurd rfl hxv
      obtain ⟨s, hs, hxs⟩ := mem_biUnion.1 hx
      by_cases hus : u ∈ D hF r s
      · exact mem_insert_of_mem (mem_biUnion.2 ⟨s, hs, hus⟩)
      · obtain ⟨-, hu'⟩ := Antinorm3.D_edge hF r (hsr s hs).1 hxs hus hu.symm
        rw [hu', (hsr s hs).2]
        exact mem_insert_self _ _
    · intro x hx hxw u hu
      by_contra hu'
      exact hxw (Antinorm3.D_edge hF r hwr hx hu' hu.symm).1
    · intro u hu hvu
      exact (Antinorm3.D_edge hF r hwr hu hvD hvu).1
    · intro u hu hwu
      rcases mem_insert.1 hu with rfl | hu
      · rfl
      obtain ⟨s, hs, hus⟩ := mem_biUnion.1 hu
      have hwDs : w ∉ D hF r s := fun h =>
        disjoint_left.1 (hsw s hs) h (Antinorm3.self_mem_D hF r w)
      obtain ⟨-, h⟩ := Antinorm3.D_edge hF r (hsr s hs).1 hus hwDs hwu
      exact absurd (h.trans (hsr s hs).2) hwv

theorem messageG_eq_msgP (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    (ord : Vt → List Vt) (hord : IsChildOrder hF r ord) (v : Vt) :
    messageG P g (toRTree hF r ord (fun v => (lab v, f v)) v)
      = msgP P g hF r lab f (D hF r v) v := by
  induction h : (D hF r v).card using Nat.strong_induction_on generalizing v with
  | _ n ih =>
  rw [toRTree]
  set l := (ord v).filter (· ∈ children hF r v) with hl
  rw [List.attach_map_val]
  have hmsg : messageG P g (RTree.node (lab v, f v)
      (l.map (fun w => toRTree hF r ord (fun v => (lab v, f v)) w)))
      = mergeAllG P g (initF P (lab v).1 (lab v).2.1 (lab v).2.2 (f v))
          (l.map (fun w => toRTree hF r ord (fun v => (lab v, f v)) w)) := by
    rw [messageG]
  rw [hmsg, ← msgP_single P g hF r lab f v,
    show ({v} : Finset Vt) = insert v ((∅ : Finset Vt).biUnion (D hF r)) by simp]
  have hlm : ∀ w, w ∈ l ↔ w ∈ children hF r v := by
    intro w
    rw [hl, List.mem_filter, (hord v).2 w]
    simp
  rw [mergeAll_msgP P g hF r lab f hp₂ hg v _ l ∅ (empty_subset _)
    ((hord v).1.filter _) (fun w hw => ⟨(hlm w).1 hw, notMem_empty w⟩)
    (fun w hw => ih _ (h ▸ Antinorm3.card_D_child_lt hF r ((hlm w).1 hw)) w rfl)]
  congr 1
  rw [Antinorm3.D_eq hF r v]
  congr 2
  ext w
  rw [empty_union, List.mem_toFinset, hlm]

theorem root_sum (ℓ : Fin 10 → ℝ) (Q : Finset Vt → Finset Vt → Prop)
    (hQ : ∀ Y U, Disjoint Y U → ℓ (sttG hF r r Y U) * psiG P lab r Y U
      = phiG P g hF r lab r Y U * (if Q Y U then 1 else 0)) :
    ∑ i, ℓ i * msgP P g hF r lab f univ r i
      = wsumG P g hF r lab (fun X' Υ => Respects f X' Υ ∧ Q X' Υ) := by
  unfold msgP wsumG
  rw [powerset_univ]
  have hswap : ∑ i, ℓ i * (∑ Y : Finset Vt, ∑ U : Finset Vt, termP P g hF r lab f univ r Y U) i
      = ∑ Y : Finset Vt, ∑ U : Finset Vt, ∑ i, ℓ i * termP P g hF r lab f univ r Y U i := by
    simp only [Finset.sum_apply, Finset.mul_sum]
    rw [Finset.sum_comm]
    apply sum_congr rfl
    intro Y _
    rw [Finset.sum_comm]
  rw [hswap]
  apply sum_congr rfl
  intro Y _
  have hterm : ∀ U, ∑ i, ℓ i * termP P g hF r lab f univ r Y U i
      = if Disjoint Y U ∧ RespOn f univ Y U then
          (if U ⊆ candF F Y then wtG P g hF r lab Y U else 0) * (if Q Y U then 1 else 0)
        else 0 := by
    intro U
    unfold termP
    by_cases hc : Disjoint Y U ∧ RespOn f univ Y U
    · rw [ite_eq_left hc, ite_eq_left hc]
      have hs : ∑ i, ℓ i * (((∏ x ∈ univ.erase r, phiG P g hF r lab x Y U)
          * psiG P lab r Y U) • eB (sttG hF r r Y U)) i
          = ((∏ x ∈ univ.erase r, phiG P g hF r lab x Y U) * psiG P lab r Y U)
            * ℓ (sttG hF r r Y U) := by
        rw [Finset.sum_eq_single (sttG hF r r Y U)]
        · simp [eB]; ring
        · intro b _ hb; simp [eB, hb]
        · intro h; exact absurd (mem_univ _) h
      rw [hs, ← prod_phiG P g hF r lab hc.1, ← mul_prod_erase univ _ (mem_univ r), mul_assoc,
        mul_comm (psiG P lab r Y U), hQ Y U hc.1]
      ring
    · rw [ite_eq_right hc, ite_eq_right hc]; simp
  rw [sum_congr rfl (fun U _ => hterm U)]
  symm
  rw [← sum_subset (subset_univ ((candF F Y).powerset))]
  · apply sum_congr rfl
    intro U hU
    rw [mem_powerset] at hU
    have hd : Disjoint Y U := by
      rw [disjoint_right]
      intro x hx
      have := hU hx
      simp only [candF, mem_filter] at this
      exact this.2.1
    have hr : RespOn f univ Y U ↔ Respects f Y U := by
      simp [RespOn, Respects]
    by_cases h1 : Respects f Y U <;> by_cases h2 : Q Y U <;> simp [h1, h2, hd, hr, hU]
  · intro U _ hU
    rw [mem_powerset] at hU
    simp [hU]

theorem root_pi (hp₂ : P.p₂ ≠ 0) (hg : ∀ b j, 3 ≤ j → g b j = g b 3) (π : Fin 10 → Prop) :
    ∑ i, (if π i then cfG P g 5 i else 0) * msgP P g hF r lab f univ r i
      = wsumG P g hF r lab (fun X' Υ => Respects f X' Υ ∧ π (sttG hF r r X' Υ)) :=
  root_sum P g hF r lab f _ (fun Y U => π (sttG hF r r Y U)) (fun Y U hd => by
    rw [phiG_root P g hF r lab hp₂ hg hd]; split_ifs <;> ring)

theorem wsumG_congr {E₁ E₂ : Finset Vt → Finset Vt → Prop}
    (h : ∀ X' Υ, Υ ⊆ candF F X' → (E₁ X' Υ ↔ E₂ X' Υ)) :
    wsumG P g hF r lab E₁ = wsumG P g hF r lab E₂ := by
  unfold wsumG
  apply sum_congr rfl
  intro X' _
  apply sum_congr rfl
  intro Υ hΥ
  have := h X' Υ (mem_powerset.1 hΥ)
  by_cases h1 : E₁ X' Υ
  · rw [ite_eq_left h1, ite_eq_left (this.1 h1)]
  · rw [ite_eq_right h1, ite_eq_right (fun h2 => h1 (this.2 h2))]

end Tree

/-- The generic `lem:rsc-recursion`: the three root identities. -/
theorem recursionG (P : Par) (hp₂ : P.p₂ ≠ 0) (g : Bool → ℕ → ℝ)
    (hg : ∀ b j, 3 ≤ j → g b j = g b 3)
    {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt)
    (hord : IsChildOrder hF r ord) (lab : Vt → Label) (f : Vt → Option Force) :
    let M := messageG P g (toRTree hF r ord (fun v => (lab v, f v)) r)
    M 0 = wsumG P g hF r lab (fun X' Υ => Respects f X' Υ ∧ r ∈ X') ∧
    (g false 2 / P.p₂) * M 3 + (g false 3 / P.p₂) * M 4
      = wsumG P g hF r lab (fun X' Υ => Respects f X' Υ ∧ r ∈ Υ) ∧
    M 5 / 2 + M 6 + M 7 + (1 - g false 2) * M 8 + (1 - g false 3) * M 9
      = wsumG P g hF r lab (fun X' Υ => Respects f X' Υ ∧ r ∉ X' ∪ Υ) := by
  have hM := messageG_eq_msgP P g hF r lab f hp₂ hg ord hord r
  rw [Antinorm3.D_root] at hM
  dsimp only
  rw [hM]
  have cat0 : ∀ Y U, sttG hF r r Y U = 0 ↔ r ∈ Y := fun Y U => sttG_zero_iff hF r r Y U
  have cat5 : ∀ Y U, (sttG hF r r Y U).val < 5 ↔ (r ∈ Y ∨ r ∈ U) :=
    fun Y U => sttG_lt5_iff hF r r Y U
  refine ⟨?_, ?_, ?_⟩
  · rw [wsumG_congr P g hF r lab
      (E₂ := fun X' Υ => Respects f X' Υ ∧ sttG hF r r X' Υ = 0)
      (fun X' Υ _ => and_congr_right (fun _ => (cat0 X' Υ).symm)),
      ← root_pi P g hF r lab f hp₂ hg (fun i => i = 0)]
    simp [cfG]
  · rw [wsumG_congr P g hF r lab
      (E₂ := fun X' Υ => Respects f X' Υ ∧ (sttG hF r r X' Υ ≠ 0 ∧ (sttG hF r r X' Υ).val < 5))
      (fun X' Υ hΥ => and_congr_right (fun _ => by
        have hrX : r ∈ Υ → r ∉ X' := fun h => (mem_filter.1 (hΥ h)).2.1
        rw [Ne, cat0, cat5]
        constructor
        · intro h; exact ⟨hrX h, Or.inr h⟩
        · rintro ⟨h1, h2⟩; exact h2.resolve_left h1)),
      ← root_pi P g hF r lab f hp₂ hg (fun i => i ≠ 0 ∧ i.val < 5)]
    simp [Fin.sum_univ_succ, cfG]
  · rw [wsumG_congr P g hF r lab
      (E₂ := fun X' Υ => Respects f X' Υ ∧ 5 ≤ (sttG hF r r X' Υ).val)
      (fun X' Υ _ => and_congr_right (fun _ => by rw [mem_union, ← cat5, not_lt])),
      ← root_pi P g hF r lab f hp₂ hg (fun i => 5 ≤ i.val)]
    simp [Fin.sum_univ_succ, cfG]
    ring

end
end MaxLeafFormal.RSCTree