MaxLeafFormal.RSCGraph

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

Statements of the paper formalised here: Lemma D.5.1, Lemma D.5.2, Lemma D.5.4, Lemma D.5.14, Corollary D.5.17, Lemma D.5.13, Lemma D.5.11, Lemma D.5.6, Proposition 8.6.

import MaxLeafFormal.RSCTreeModel
import MaxLeafFormal.RSCGraphDefs
import MaxLeafFormal.RSCParams
import MaxLeafFormal.RSC.Mono
import MaxLeafFormal.RSC.Pointwise
import MaxLeafFormal.RSC.Leaf
import MaxLeafFormal.RSC.Model
import MaxLeafFormal.RSC.Measure
import MaxLeafFormal.RSC.Jensen
import MaxLeafFormal.RSC.Expect

/-!
# Graph-level facts and the assembly

`lem:rsc-mono`, `lem:rsc-pointwise`, `lem:rsc-model`, `lem:rsc-leaf`, the owner facts,
`lem:rsc-jensen` with `eq:rsc-EQ3`, `eq:rsc-EQ2`, `eq:rsc-EQex`, `lem:rsc-jlemma`,
`lem:rsc-credit`, `cor:rsc-reduction`, and `prop:rsc-bound` conditional on the data conditions.
-/

namespace MaxLeafFormal.RSCGraph
open Finset
open MaxLeafFormal.CDS (IsCDS γc termCount)
open MaxLeafFormal.Antinorm8 (RTree size fin cZ PZ initInf)
open MaxLeafFormal.RSCCert (Label nuSum Admissible Light₂ Light₃ eps delta₂ delta₃ rho₁ Credits)
open MaxLeafFormal.RSCRec (Par)
open MaxLeafFormal.RSCTree

noncomputable section
open Classical

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

section Graph
variable (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V)

/-- `lem:rsc-mono`. -/
theorem rsc_mono {X Y : Finset V} (hXY : X ⊆ Y) : termCount G Y ≤ termCount G X :=
  mono_core G hXY

/-- `lem:rsc-pointwise`: the first assertion and (i)–(v). -/
theorem rsc_pointwise (p₂ p₃ : ℝ) (hp : 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1/2)
    (o : Out S → S) (ho : ∀ u, G.Adj u.1 (o u).1) (u : Out S) {X' X : Finset S} (hX : X' ⊆ X) :
    (o u ∉ X → hbar o u X ≤ hfac p₂ p₃ G S u X' X) ∧
    (Private G S u → hbar o u X ≤ hfac p₂ p₃ G S u X' X) ∧
    (Shared G S u →
      hbar o u X * qT p₂ p₃ (typ G S u) ^ (if o u ∈ X then 1 else 0) ≤ hfac p₂ p₃ G S u X' X) ∧
    (Shared G S u → o u ∉ X → (Nprime G S o u ∩ X).Nonempty →
      Real.exp (deltaT p₃ (typ G S u)) * hbar o u X ≤ hfac p₂ p₃ G S u X' X) ∧
    (Shared G S u → typ G S u = 3 →
      ind (Nprime G S o u ∩ X').Nonempty * (delta₃ p₃ * ind (o u ∉ X) - eps p₃ * ind (o u ∈ X))
        ≤ Real.log (hfac p₂ p₃ G S u X' X / hbar o u X)) ∧
    (Shared G S u → typ G S u = 2 →
      ind (Nprime G S o u ∩ X').Nonempty * (delta₂ * ind (o u ∉ X) - eps p₂ * ind (o u ∈ X'))
        ≤ Real.log (hfac p₂ p₃ G S u X' X / hbar o u X)) :=
  pointwise_core G S p₂ p₃ hp o ho u hX

/-- `lem:rsc-leaf`. -/
theorem rsc_leaf (hS : IsCDS G S) (hmin : S.card = γc G) (h2 : 2 ≤ S.card)
    (F : SimpleGraph S) (hFG : F ≤ G.induce (S : Set V)) (hF : F.IsTree)
    (v : S) (hv : F.degree v = 1) :
    ∃ u : Out S, NS G S u = {v} :=
  leaf_core G S hS hmin h2 F hFG hF v hv

end Graph

/-- A vertex of a connected graph has a neighbour when there is another vertex. -/
theorem deg_pos_of_conn {α : Type*} [Fintype α] (F : SimpleGraph α) (hF : F.Connected)
    (v w : α) (hvw : v ≠ w) : 0 < F.degree v := by
  obtain ⟨p⟩ := hF.preconnected v w
  cases p with
  | nil => exact absurd rfl hvw
  | cons h _ => exact (SimpleGraph.degree_pos_iff_exists_adj F v).2 ⟨_, h⟩

omit [Fintype V] in

/-- A shared outside vertex sees two distinct inside vertices, so every inside vertex has
positive degree in a connected `F` on `S`. -/
theorem deg_pos_of_shared (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V)
    (F : SimpleGraph S) (hF : F.Connected) (u : Out S) (hu : Shared G S u) (v : S) :
    0 < F.degree v := by
  have h1 : 1 < (NS G S u).card := by unfold Shared at hu; omega
  obtain ⟨a, -, b, -, hab⟩ := Finset.one_lt_card.1 h1
  by_cases hav : a = v
  · exact deg_pos_of_conn F hF v b (fun h => hab (hav.trans h))
  · exact deg_pos_of_conn F hF v a (fun h => hav h.symm)

omit [Fintype V] [DecidableEq V] in

/-- A vertex of a span is in it: the trivial path. -/
theorem mem_span_self {S : Finset V} (F : SimpleGraph S) (N : Finset S) {x : S} (hx : x ∈ N) :
    x ∈ span F N := by
  refine Finset.mem_filter.2 ⟨Finset.mem_univ _, x, hx, x, hx, SimpleGraph.Walk.nil,
    SimpleGraph.Walk.IsPath.nil, ?_⟩
  simp

/-- In a tree, a neighbour `x` of `a` that is no farther from the root `b` than `a` is the parent
of `a` towards `b`. -/
theorem ownerPar_of_max {α : Type*} [Fintype α] [DecidableEq α] {F : SimpleGraph α}
    (hF : F.IsTree) (a b x : α) (hadj : F.Adj a x) (hmax : F.dist x b ≤ F.dist a b) :
    F.dist b x + 1 = F.dist b a := by
  rcases hF.dist_eq_dist_add_one_of_adj b hadj with h1 | h1
  · omega
  · have e1 : F.dist x b = F.dist b x := SimpleGraph.dist_comm
    have e2 : F.dist a b = F.dist b a := SimpleGraph.dist_comm
    omega

/-- In a tree, along a path that starts at `v` and avoids the parent `w` of `v` towards `b`,
the distance from `b` increases by one at each step. -/
theorem dist_up_of_path {α : Type*} [Fintype α] [DecidableEq α] {F : SimpleGraph α}
    (hF : F.IsTree) (b : α) : ∀ {v e : α} (p : F.Walk v e) (w : α), p.IsPath → F.Adj w v →
      F.dist b w + 1 = F.dist b v → w ∉ p.support → F.dist b e = F.dist b v + p.length := by
  intro v e p
  induction p with
  | nil => intro w _ _ _ _; simp
  | @cons v v' e h p ih =>
    intro w hp hwv hd hw
    rw [SimpleGraph.Walk.cons_isPath_iff] at hp
    have hv'w : v' ≠ w := by
      intro h'
      apply hw
      subst h'
      simp
    have hd' : F.dist b v' = F.dist b v + 1 := by
      rcases hF.dist_eq_dist_add_one_of_adj b h with h1 | h1
      · exact absurd (MaxLeafFormal.CDS.parent_unique hF b h hwv.symm h1.symm hd) hv'w
      · exact h1
    have := ih v hp.1 h hd'.symm hp.2
    simp only [SimpleGraph.Walk.length_cons]
    omega

/-- In a tree, let every vertex of `N` be at distance at most `dist a b` from `b`.
A neighbour `x` of `a` lying on a path between two vertices of `N` is the parent of `a` towards
`b`. -/
theorem span_adj_par {α : Type*} [Fintype α] [DecidableEq α] {F : SimpleGraph α}
    (hF : F.IsTree) (N : Finset α) (a b x : α)
    (hmax : ∀ y ∈ N, F.dist y b ≤ F.dist a b) (hadj : F.Adj a x)
    (hx : ∃ c ∈ N, ∃ d ∈ N, ∃ p : F.Walk c d, p.IsPath ∧ x ∈ p.support) :
    F.dist b x + 1 = F.dist b a := by
  rcases hF.dist_eq_dist_add_one_of_adj b hadj with h1 | h1
  · exact h1.symm
  exfalso
  obtain ⟨c, hc, d, hd, p, hp, hxp⟩ := hx
  have key : ∀ {e : α} (q : F.Walk x e), q.IsPath → a ∉ q.support → e ∈ N → False := by
    intro e q hq ha he
    have h2 := dist_up_of_path hF b q a hq hadj h1.symm ha
    have h3 := hmax e he
    have e1 : F.dist e b = F.dist b e := SimpleGraph.dist_comm
    have e2 : F.dist a b = F.dist b a := SimpleGraph.dist_comm
    omega
  by_cases ha : a ∈ (p.dropUntil x hxp).support
  · refine key (p.takeUntil x hxp).reverse
      ((SimpleGraph.Walk.isPath_reverse_iff _).2 (hp.takeUntil hxp)) ?_ hc
    rw [SimpleGraph.Walk.support_reverse, List.mem_reverse]
    intro ha'
    have hnd : ((p.takeUntil x hxp).append (p.dropUntil x hxp)).support.Nodup := by
      rw [SimpleGraph.Walk.take_spec]
      exact hp.support_nodup
    rw [SimpleGraph.Walk.support_append] at hnd
    have hax : a ≠ x := hadj.ne
    have ha2 : a ∈ (p.dropUntil x hxp).support.tail := by
      rw [← SimpleGraph.Walk.cons_tail_support, List.mem_cons] at ha
      exact ha.resolve_left hax
    exact (List.nodup_append.1 hnd).2.2 a ha' a ha2 rfl
  · exact key _ (hp.dropUntil hxp) ha hd

/-- `c_v ≤ ν_v` for the labels of any set of exposed vertices. -/
theorem labOf_c_le (G : SimpleGraph V) (S : Finset V) (o : Out S → S) (Oex : Finset (Out S))
    (v : S) : (labOf G S o Oex v).2.1 + (labOf G S o Oex v).2.2 ≤ (labOf G S o Oex v).1 := by
  show cOf G S o Oex 2 v + cOf G S o Oex 3 v ≤ nuOf o v
  unfold cOf nuOf
  rw [← Finset.card_union_of_disjoint]
  · apply Finset.card_le_card
    intro u hu
    simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and] at hu ⊢
    rcases hu with h | h <;> exact h.1
  · refine Finset.disjoint_filter.2 (fun u _ h2 h3 => ?_)
    have := h2.2.2.symm.trans h3.2.2
    omega

omit [Fintype V] [DecidableEq V] in

theorem typ_eq_three (G : SimpleGraph V) (S : Finset V) (u : Out S) (h : typ G S u ≠ 2) :
    typ G S u = 3 := by
  unfold typ at h ⊢; split_ifs at h ⊢ <;> simp_all

theorem standing_parts {P : Par} (hP : P.Standing) :
    (0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) ∧ 0 ≤ P.y ∧ (1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) :=
  ⟨⟨hP.1, hP.2.1, hP.2.2.1⟩, hP.2.2.2.1.le, ⟨hP.2.2.2.2.1, hP.2.2.2.2.2.2.1⟩⟩

section TMSetting
variable (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V)
  (hS : IsCDS G S) (F : SimpleGraph S) (hFG : F ≤ G.induce (S : Set V)) (hF : F.IsTree)
  (o : Out S → S) (ho : ∀ u, G.Adj u.1 (o u).1)
  (Oex : Finset (Out S)) (hOex : ∀ u ∈ Oex, Shared G S u)
include hG hS hFG hF ho hOex

/-- `lem:rsc-jensen`. -/
theorem rsc_jensen (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) :
    Wtm P F (labOf G S o Oex) * Real.exp
        (∑ u ∈ Oco G S Oex,
            Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ)))
          + ∑ u ∈ Oex,
            Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htilEx P G S o u X' (X' ∪ Υ))))
      ≤ Wcl G S P.p₂ P.p₃ P.y :=
  jensen_core G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ

/-- "In particular" of `lem:rsc-jensen`. -/
theorem rsc_jensen_nonneg (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃)
    (hco : ∀ u ∈ Oco G S Oex,
      0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))))
    (hex : ∀ u ∈ Oex,
      0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htilEx P G S o u X' (X' ∪ Υ)))) :
    Wtm P F (labOf G S o Oex) ≤ Wcl G S P.p₂ P.p₃ P.y :=
  jensen_nonneg_core G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ hco hex

/-- `eq:rsc-EQ3` and `eq:rsc-EQ2`, for every shared `u`. -/
theorem EQ3 (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (u : Out S) (hu : Shared G S u) (h3 : typ G S u = 3) :
    delta₃ P.p₃ * Ptm P F (labOf G S o Oex)
          (fun X' Υ => (Nprime G S o u ∩ X').Nonempty ∧ o u ∉ X' ∪ Υ)
        - eps P.p₃ * Ptm P F (labOf G S o Oex)
          (fun X' Υ => (Nprime G S o u ∩ X').Nonempty ∧ o u ∈ X' ∪ Υ)
      ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))) :=
  EQ3_core G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu h3

theorem EQ2 (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (u : Out S) (hu : Shared G S u) (h2 : typ G S u = 2) :
    delta₂ * Ptm P F (labOf G S o Oex)
          (fun X' Υ => (Nprime G S o u ∩ X').Nonempty ∧ o u ∉ X' ∪ Υ)
        - eps P.p₂ * Ptm P F (labOf G S o Oex)
          (fun X' _Υ => (Nprime G S o u ∩ X').Nonempty ∧ o u ∈ X')
      ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))) :=
  EQ2_core G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu h2

/-- `eq:rsc-EQex` and the remark after it. -/
theorem EQex (P : Par) (hp : 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1/2) (hy : 0 ≤ P.y)
    (hϖ : 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃) (u : Out S) (hu : u ∈ Oex) :
    (0 < Ptm P F (labOf G S o Oex) (fun X' Υ => o u ∉ X' ∪ Υ) →
      Ptm P F (labOf G S o Oex) (fun X' Υ => o u ∉ X' ∪ Υ)
          * (deltaT P.p₃ (typ G S u)
              * Pcond P F (labOf G S o Oex) (fun X' Υ => (Nprime G S o u ∩ (X' ∪ Υ)).Nonempty)
                  (fun X' Υ => o u ∉ X' ∪ Υ)
            - Real.log (ϖT P (typ G S u)))
        ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htilEx P G S o u X' (X' ∪ Υ)))) ∧
    (Ptm P F (labOf G S o Oex) (fun X' Υ => o u ∉ X' ∪ Υ) = 0 →
      0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htilEx P G S o u X' (X' ∪ Υ)))) :=
  EQex_core G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu

/-- `lem:rsc-jlemma`, for an owner with at most one `F`-neighbour in `N'_u`. -/
theorem rsc_jlemma_of (P : Par) (hP : P.Standing) (u : Out S) (hu : Shared G S u)
    (hlight : LightT P (typ G S u) (nuOf o (o u)) (F.degree (o u)))
    (hok : ((Nprime G S o u).filter (F.Adj (o u))).card ≤ 1) :
    0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))) := by
  obtain ⟨hp, hy, hϖ⟩ := standing_parts hP
  have hc := labOf_c_le G S o Oex
  have ho' : o u ∉ Nprime G S o u := Finset.notMem_erase _ _
  have jt := jlemma_tree P hP hF (labOf G S o Oex) hc (o u) (Nprime G S o u) ho' hok
  by_cases h2 : typ G S u = 2
  · have hl : Light₂ P.p₂ P.p₃ P.y (nuOf o (o u)) (F.degree (o u)) := by
      simpa [LightT, h2] using hlight
    have := jt.2 hl
    have hE := EQ2 G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu h2
    linarith
  · have h3 := typ_eq_three G S u h2
    have hl : Light₃ P.p₂ P.p₃ P.y (nuOf o (o u)) (F.degree (o u)) := by
      simpa [LightT, h3] using hlight
    have := jt.1 hl
    have hE := EQ3 G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu h3
    linarith

/-- `lem:rsc-jlemma` as stated. -/
theorem rsc_jlemma (P : Par) (hP : P.Standing) (u : Out S) (hu : Shared G S u)
    (hlight : LightT P (typ G S u) (nuOf o (o u)) (F.degree (o u)))
    (hleaf : IsLeafIn F (span F (NS G S u)) (o u)) :
    0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))) := by
  refine rsc_jlemma_of G hG S hS F hFG hF o ho Oex hOex P hP u hu hlight ?_
  refine le_trans (Finset.card_le_card ?_) hleaf.2.le
  intro x hx
  simp only [Finset.mem_filter] at hx ⊢
  exact ⟨mem_span_self F _ (Finset.mem_of_mem_erase hx.1), hx.2⟩

set_option linter.unusedSectionVars false in

/-- `lem:rsc-credit`, first assertion. -/
theorem rsc_credit (P : Par) (hP : P.Standing) (u : Out S) (hu : u ∈ Oex) :
    (if typ G S u = 2 then 1 - rho₁ P.p₃ P.y else 1 - rho₁ P.p₃ P.y ^ 2)
      ≤ Pcond P F (labOf G S o Oex) (fun X' Υ => (Nprime G S o u ∩ (X' ∪ Υ)).Nonempty)
          (fun X' Υ => o u ∉ X' ∪ Υ) := by
  have hc := labOf_c_le G S o Oex
  have ho' : o u ∉ Nprime G S o u := Finset.notMem_erase _ _
  have hct := credit_tree P hP hF (labOf G S o Oex) hc (o u) (Nprime G S o u) ho'
  have hou : o u ∈ NS G S u := by simp [NS, ho u]
  have hcard : (Nprime G S o u).card = (NS G S u).card - 1 := Finset.card_erase_of_mem hou
  have hsh : 2 ≤ (NS G S u).card := hOex u hu
  split_ifs with h2
  · apply hct.1
    rw [← Finset.card_pos]; omega
  · apply hct.2
    have : (NS G S u).card ≠ 2 := by intro h; apply h2; simp [typ, h]
    omega

/-- `lem:rsc-credit`, "consequently". -/
theorem rsc_credit_ex (P : Par) (hP : P.Standing) (hcr : Credits P.p₃ P.y P.ϖ₂ P.ϖ₃) :
    ∀ u ∈ Oex,
      0 ≤ Etm P F (labOf G S o Oex) (fun X' Υ => Real.log (htilEx P G S o u X' (X' ∪ Υ))) := by
  intro u hu
  obtain ⟨hp, hy, hϖ⟩ := standing_parts hP
  have hp' : 0 ≤ P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ ≤ 1 := ⟨hp.1.le, hp.2.1, by linarith [hp.2.2]⟩
  have hpos : 0 < Ptm P F (labOf G S o Oex) (fun X' Υ => o u ∉ X' ∪ Υ) :=
    div_pos (wsum_pos_of_empty P hp' hy hϖ F _ _ (by simp)) (Wtm_pos P hp' hy hϖ F _)
  have hEQ := EQex G hG S hS F hFG hF o ho Oex hOex P hp hy hϖ u hu
  refine le_trans ?_ (hEQ.1 hpos)
  apply mul_nonneg hpos.le
  have hcr' := rsc_credit G hG S hS F hFG hF o ho Oex hOex P hP u hu
  have hδ₂ : 0 < delta₂ := Real.log_pos (by norm_num)
  have hδ₃ : 0 < delta₃ P.p₃ := Real.log_pos (by linarith [hp.2.2])
  by_cases h2 : typ G S u = 2
  · simp only [h2, ite_true, deltaT, ϖT] at hcr' ⊢
    nlinarith [hcr.1]
  · have h3 := typ_eq_three G S u h2
    simp only [h3, ite_false, deltaT, ϖT, show (3 : ℕ) ≠ 2 by decide] at hcr' ⊢
    nlinarith [hcr.2]

end TMSetting

section TreeSetting
variable (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V)
  (hS : IsCDS G S) (F : SimpleGraph S) (hFG : F ≤ G.induce (S : Set V)) (hF : F.IsTree)
include hG hS hFG hF

/-- `lem:rsc-model`. -/
theorem rsc_model (p₂ p₃ y : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (hy : 0 ≤ y) :
    ∑ X' : Finset S, ∑ Υ ∈ (candF F X').powerset,
        y ^ X'.card * piF p₂ p₃ F X' Υ * (1/2 : ℝ) ^ psiF F (X' ∪ Υ)
          * ∏ u : Out S, hfac p₂ p₃ G S u X' (X' ∪ Υ)
      ≤ Wcl G S p₂ p₃ y :=
  model_core.{_, 0, 0} G hG S hS F hFG hF (fun _ _ h => mono_core G h)
    monotone_coupling prodMeas_sum_one p₂ p₃ y hp hy

set_option linter.unusedSectionVars false in

/-- An owner that is a leaf of `T_u` has at most one `F`-neighbour in `N'_u`. -/
theorem ownerOK_of_rule (o : Out S → S) (_ho : ∀ u, G.Adj u.1 (o u).1)
    (hrule : OwnerRule G S F o) : OwnerOK G S F o := by
  intro u hu
  obtain ⟨-, hcard⟩ := hrule u hu
  refine le_trans (Finset.card_le_card ?_) hcard.le
  intro x hx
  rw [Finset.mem_filter] at hx ⊢
  have hx1 : x ∈ (NS G S u).erase (o u) := hx.1
  exact ⟨mem_span_self F _ (Finset.mem_of_mem_erase hx1), hx.2⟩

set_option linter.unusedSectionVars false in

/-- Owner maps with `OwnerOK` exist (farthest pair in `N_S(u)`). -/
theorem exists_ownerOK : ∃ o : Out S → S, (∀ u, G.Adj u.1 (o u).1) ∧ OwnerOK G S F o := by
  have hch : ∀ u : Out S, ∃ a : S, a ∈ NS G S u ∧ ∃ b : S, b ∈ NS G S u ∧
      ∀ x ∈ NS G S u, ∀ y ∈ NS G S u, F.dist x y ≤ F.dist a b := by
    intro u
    have hne : (NS G S u ×ˢ NS G S u).Nonempty := by
      rcases hS.2 u.1 with h | ⟨w, hw, hadj⟩
      · exact absurd h u.2
      · exact ⟨(⟨w, hw⟩, ⟨w, hw⟩), Finset.mem_product.2
          ⟨by simp [NS, hadj], by simp [NS, hadj]⟩⟩
    obtain ⟨⟨a, b⟩, hab, hmax⟩ :=
      Finset.exists_max_image _ (fun p : S × S => F.dist p.1 p.2) hne
    rw [Finset.mem_product] at hab
    exact ⟨a, hab.1, b, hab.2, fun x hx y hy => hmax (x, y) (Finset.mem_product.2 ⟨hx, hy⟩)⟩
  choose o hoNS b hbNS hmaxo using hch
  refine ⟨o, fun u => ?_, ?_⟩
  · have h := hoNS u
    simp only [NS, Finset.mem_filter, Finset.mem_univ, true_and] at h
    exact h
  intro u _
  apply Finset.card_le_one.2
  intro x hx y hy
  rw [Finset.mem_filter] at hx hy
  have hx' := hx
  have hy' := hy
  have hxN : x ∈ NS G S u := Finset.mem_of_mem_erase hx'.1
  have hyN : y ∈ NS G S u := Finset.mem_of_mem_erase hy'.1
  have h1 := ownerPar_of_max hF (o u) (b u) x hx'.2 (hmaxo u x hxN (b u) (hbNS u))
  have h2 := ownerPar_of_max hF (o u) (b u) y hy'.2 (hmaxo u y hyN (b u) (hbNS u))
  exact MaxLeafFormal.CDS.parent_unique hF (b u) hx'.2 hy'.2 h1 h2

set_option linter.unusedSectionVars false in

/-- The owner rule is well defined. For a farthest pair `a, b` in
`N_S(u)`, the vertex `a` is a leaf of `T_u`: its only `F`-neighbour in `T_u` is its parent
towards `b`. -/
theorem exists_ownerRule : ∃ o : Out S → S, (∀ u, G.Adj u.1 (o u).1) ∧ OwnerRule G S F o := by
  have hch : ∀ u : Out S, ∃ a : S, a ∈ NS G S u ∧ ∃ b : S, b ∈ NS G S u ∧
      ∀ x ∈ NS G S u, ∀ y ∈ NS G S u, F.dist x y ≤ F.dist a b := by
    intro u
    have hne : (NS G S u ×ˢ NS G S u).Nonempty := by
      rcases hS.2 u.1 with h | ⟨w, hw, hadj⟩
      · exact absurd h u.2
      · exact ⟨(⟨w, hw⟩, ⟨w, hw⟩), Finset.mem_product.2
          ⟨by simp [NS, hadj], by simp [NS, hadj]⟩⟩
    obtain ⟨⟨a, b⟩, hab, hmax⟩ :=
      Finset.exists_max_image _ (fun p : S × S => F.dist p.1 p.2) hne
    rw [Finset.mem_product] at hab
    exact ⟨a, hab.1, b, hab.2, fun x hx y hy => hmax (x, y) (Finset.mem_product.2 ⟨hx, hy⟩)⟩
  choose o hoNS b hbNS hmaxo using hch
  refine ⟨o, fun u => ?_, ?_⟩
  · have h := hoNS u
    simp only [NS, Finset.mem_filter, Finset.mem_univ, true_and] at h
    exact h
  intro u hu
  have haN := hoNS u
  have hbN := hbNS u
  have hmax' : ∀ y ∈ NS G S u, F.dist y (b u) ≤ F.dist (o u) (b u) :=
    fun y hy => hmaxo u y hy (b u) hbN
  have hne : o u ≠ b u := by
    have h1 : 1 < (NS G S u).card := by unfold Shared at hu; omega
    obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.1 h1
    have hpos := hF.connected.pos_dist_of_ne hxy
    have := hmaxo u x hx y hy
    intro h
    rw [h, SimpleGraph.dist_self] at this
    omega
  obtain ⟨w, hw, hdw⟩ := MaxLeafFormal.CDS.exists_parent hF (b u) hne
  have hwspan : w ∈ span F (NS G S u) := by
    obtain ⟨q, hq⟩ := hF.connected.exists_walk_length_eq_dist w (b u)
    refine Finset.mem_filter.2 ⟨Finset.mem_univ _, o u, haN, b u, hbN,
      SimpleGraph.Walk.cons hw q, ?_, by simp⟩
    apply SimpleGraph.Walk.isPath_of_length_eq_dist
    have e1 : F.dist w (b u) = F.dist (b u) w := SimpleGraph.dist_comm
    have e2 : F.dist (o u) (b u) = F.dist (b u) (o u) := SimpleGraph.dist_comm
    simp only [SimpleGraph.Walk.length_cons]
    omega
  refine ⟨mem_span_self F _ haN, Finset.card_eq_one.2 ⟨w, ?_⟩⟩
  ext y
  simp only [Finset.mem_filter, Finset.mem_singleton]
  constructor
  · rintro ⟨hy, hya⟩
    have hyx : ∃ c ∈ NS G S u, ∃ d ∈ NS G S u, ∃ p : F.Walk c d, p.IsPath ∧ y ∈ p.support := by
      unfold span at hy
      exact (Finset.mem_filter.1 hy).2
    have hpy := span_adj_par hF (NS G S u) (o u) (b u) y hmax' hya hyx
    exact MaxLeafFormal.CDS.parent_unique hF (b u) hya hw hpy hdw
  · rintro rfl
    exact ⟨hwspan, hw⟩

/-- `cor:rsc-reduction` for owner maps with `OwnerOK`. -/
theorem rsc_reduction_of (P : Par) (hP : P.Standing) (hcr : Credits P.p₃ P.y P.ϖ₂ P.ϖ₃)
    (hmin : S.card = γc G) (o : Out S → S) (ho : ∀ u, G.Adj u.1 (o u).1)
    (hok : OwnerOK G S F o) :
    AdmissibleG P F (labOf G S o (OexRule P G S F o)) ∧
      S.card + ∑ v, nuOf o v = Fintype.card V ∧
      Wtm P F (labOf G S o (OexRule P G S F o)) ≤ Wcl G S P.p₂ P.p₃ P.y := by
  have hPs := hP
  unfold Par.Standing at hPs
  obtain ⟨hp₂, hp₂₃, hp₃, hy, hϖ₂, -, hϖ₃, -⟩ := hPs
  obtain ⟨Oex, hOexdef⟩ : ∃ X : Finset (Out S), X = OexRule P G S F o := ⟨_, rfl⟩
  rw [← hOexdef]
  have hmemOex : ∀ u, u ∈ Oex ↔ Shared G S u ∧
      ¬ LightT P (typ G S u) (nuOf o (o u)) (F.degree (o u)) := by
    intro u
    rw [hOexdef]
    simp [OexRule]
  have hOexS : ∀ u ∈ Oex, Shared G S u := fun u hu => ((hmemOex u).1 hu).1
  -- counting
  have hcount : S.card + ∑ v, nuOf o v = Fintype.card V := by
    have h1 : ∑ v : S, nuOf o v = Fintype.card (Out S) := by
      have h := Finset.card_eq_sum_card_fiberwise (s := (univ : Finset (Out S)))
        (t := (univ : Finset S)) (f := o) (fun x _ => mem_univ _)
      rw [Finset.card_univ] at h
      exact h.symm
    have h3 : Fintype.card (Out S) = Sᶜ.card := by
      rw [Fintype.card_subtype]
      congr 1
      ext x
      simp
    have h6 := Finset.card_compl_add_card S
    rw [h1, h3]
    omega
  -- disjointness of the two exposed filters over a fibre
  have hdisj : ∀ v : S, Disjoint
      (univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 2))
      (univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 3)) := by
    intro v
    refine Finset.disjoint_filter.2 (fun u _ h2 h3 => ?_)
    have := h2.2.2.symm.trans h3.2.2
    omega
  have hcardU : ∀ v : S, cOf G S o Oex 2 v + cOf G S o Oex 3 v =
      (univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 2) ∪
        univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 3)).card := by
    intro v
    rw [Finset.card_union_of_disjoint (hdisj v)]
    rfl
  have keyab : ∀ v : S, cOf G S o Oex 2 v + cOf G S o Oex 3 v ≤ nuOf o v := by
    intro v
    rw [hcardU v]
    apply Finset.card_le_card
    intro u hu
    simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and] at hu ⊢
    rcases hu with h | h <;> exact h.1
  have key2 : ∀ v : S, (Light₂ P.p₂ P.p₃ P.y (nuOf o v) (F.degree v) ∨ F.degree v = 0) →
      cOf G S o Oex 2 v = 0 := by
    intro v hL
    unfold cOf
    rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
    rintro u - ⟨huv, huOex, hty⟩
    subst huv
    have hnl := ((hmemOex u).1 huOex).2
    have hnl' : ¬ Light₂ P.p₂ P.p₃ P.y (nuOf o (o u)) (F.degree (o u)) := by
      simpa [LightT, hty] using hnl
    rcases hL with hL | hL
    · exact hnl' hL
    · have := deg_pos_of_shared G S F hF.connected u ((hmemOex u).1 huOex).1 (o u)
      omega
  have key3 : ∀ v : S, (Light₃ P.p₂ P.p₃ P.y (nuOf o v) (F.degree v) ∨ F.degree v = 0) →
      cOf G S o Oex 3 v = 0 := by
    intro v hL
    unfold cOf
    rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
    rintro u - ⟨huv, huOex, hty⟩
    subst huv
    have hnl := ((hmemOex u).1 huOex).2
    have hnl' : ¬ Light₃ P.p₂ P.p₃ P.y (nuOf o (o u)) (F.degree (o u)) := by
      simpa [LightT, hty] using hnl
    rcases hL with hL | hL
    · exact hnl' hL
    · have := deg_pos_of_shared G S F hF.connected u ((hmemOex u).1 huOex).1 (o u)
      omega
  have keyd : ∀ v : S, F.degree v = 1 → 1 ≤ cOf G S o Oex 2 v + cOf G S o Oex 3 v →
      cOf G S o Oex 2 v + cOf G S o Oex 3 v ≤ nuOf o v - 1 := by
    intro v hdv hpos
    rw [hcardU v] at hpos ⊢
    have hU : 0 < (univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 2) ∪
        univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 3)).card := by
      omega
    obtain ⟨u0, hu0⟩ := Finset.card_pos.1 hU
    have hu0ex : u0 ∈ Oex ∧ o u0 = v := by
      rcases Finset.mem_union.1 hu0 with h | h
      · exact ⟨(Finset.mem_filter.1 h).2.2.1, (Finset.mem_filter.1 h).2.1⟩
      · exact ⟨(Finset.mem_filter.1 h).2.2.1, (Finset.mem_filter.1 h).2.1⟩
    have hsh0 := hOexS u0 hu0ex.1
    have hS2 : 2 ≤ S.card := by
      have h := Finset.card_le_univ (NS G S u0)
      rw [Fintype.card_coe] at h
      unfold Shared at hsh0
      omega
    obtain ⟨u', hu'⟩ := rsc_leaf G S hS hmin hS2 F hFG hF v hdv
    have hnsh' : ¬ Shared G S u' := by
      unfold Shared
      rw [hu']
      simp
    have hnOex' : u' ∉ Oex := fun h => hnsh' (hOexS u' h)
    have hou' : o u' = v := by
      have hm : o u' ∈ NS G S u' := by
        unfold NS
        simp only [Finset.mem_filter, Finset.mem_univ, true_and]
        exact ho u'
      rw [hu'] at hm
      exact Finset.mem_singleton.1 hm
    have hu'fib : u' ∈ univ.filter (fun u : Out S => o u = v) :=
      Finset.mem_filter.2 ⟨mem_univ _, hou'⟩
    have hsub : (univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 2) ∪
        univ.filter (fun u : Out S => o u = v ∧ u ∈ Oex ∧ typ G S u = 3)) ⊆
        (univ.filter (fun u : Out S => o u = v)).erase u' := by
      intro u hu
      have hcond : o u = v ∧ u ∈ Oex := by
        rcases Finset.mem_union.1 hu with h | h
        · exact ⟨(Finset.mem_filter.1 h).2.1, (Finset.mem_filter.1 h).2.2.1⟩
        · exact ⟨(Finset.mem_filter.1 h).2.1, (Finset.mem_filter.1 h).2.2.1⟩
      refine Finset.mem_erase.2 ⟨fun heq => hnOex' (by rw [← heq]; exact hcond.2),
        Finset.mem_filter.2 ⟨mem_univ _, hcond.1⟩⟩
    have hle := Finset.card_le_card hsub
    rw [Finset.card_erase_of_mem hu'fib] at hle
    unfold nuOf
    omega
  have hadm : AdmissibleG P F (labOf G S o Oex) := by
    intro v
    exact ⟨keyab v, fun h => key2 v h, fun h => key3 v h, fun h => keyd v h.1 h.2⟩
  have hco : ∀ u ∈ Oco G S Oex, 0 ≤ Etm P F (labOf G S o Oex)
      (fun X' Υ => Real.log (htil P G S o u X' (X' ∪ Υ))) := by
    intro u hu
    simp only [Oco, Finset.mem_filter, Finset.mem_univ, true_and] at hu
    have hlight : LightT P (typ G S u) (nuOf o (o u)) (F.degree (o u)) := by
      by_contra hl
      exact hu.2 ((hmemOex u).2 ⟨hu.1, hl⟩)
    exact rsc_jlemma_of G hG S hS F hFG hF o ho Oex hOexS P hP u hu.1 hlight (hok u hu.1)
  have hex := rsc_credit_ex G hG S hS F hFG hF o ho Oex hOexS P hP hcr
  have hW := rsc_jensen_nonneg G hG S hS F hFG hF o ho Oex hOexS P ⟨hp₂, hp₂₃, hp₃⟩ hy.le
    ⟨hϖ₂, hϖ₃⟩ hco hex
  exact ⟨hadm, hcount, hW⟩

/-- `cor:rsc-reduction` as stated, for the owner rule. -/
theorem rsc_reduction (P : Par) (hP : P.Standing) (hcr : Credits P.p₃ P.y P.ϖ₂ P.ϖ₃)
    (hmin : S.card = γc G) (o : Out S → S) (ho : ∀ u, G.Adj u.1 (o u).1)
    (hrule : OwnerRule G S F o) :
    AdmissibleG P F (labOf G S o (OexRule P G S F o)) ∧
      S.card + ∑ v, nuOf o v = Fintype.card V ∧
      Wtm P F (labOf G S o (OexRule P G S F o)) ≤ Wcl G S P.p₂ P.p₃ P.y :=
  rsc_reduction_of G hG S hS F hFG hF P hP hcr hmin o ho
    (ownerOK_of_rule G hG S hS F hFG hF o ho hrule)

end TreeSetting

/-- The composition: a bound for all admissible ordered labelled trees gives the same bound for
`W^cl_S(y)` of every minimum connected dominating set. -/
theorem bound_of_tree_bound (P : Par) (hP : P.Standing) (hcr : Credits P.p₃ P.y P.ϖ₂ P.ϖ₃)
    (K e : ℝ)
    (htree : ∀ t : RTree Label, Admissible P.p₂ P.p₃ P.y t →
      K * e ^ (size t + nuSum t) ≤ fin P.p₂ (RSCCert.message P.p₂ P.p₃ P.y P.ϖ₂ P.ϖ₃ t))
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V)
    (hS : IsCDS G S) (hmin : S.card = γc G) :
    K * e ^ Fintype.card V ≤ Wcl G S P.p₂ P.p₃ P.y := by
  obtain ⟨F, hFG, hF⟩ := hS.1.exists_isTree_le
  obtain ⟨o, ho, hok⟩ := exists_ownerOK G hG S hS F hFG hF
  obtain ⟨hadm, hcount, hW⟩ := rsc_reduction_of G hG S hS F hFG hF P hP hcr hmin o ho hok
  -- a root `r ∈ S`
  have hV : Nonempty V := hG.nonempty
  obtain ⟨v⟩ := hV
  have hSne : S.Nonempty := by
    rcases hS.2 v with hv | ⟨u, hu, -⟩
    · exact ⟨v, hv⟩
    · exact ⟨u, hu⟩
  obtain ⟨r0, hr0⟩ := hSne
  set r : S := ⟨r0, hr0⟩
  set lab := labOf G S o (OexRule P G S F o)
  set ord : S → List S := fun v => (Antinorm3.children hF r v).toList
  have hord : IsChildOrder hF r ord := isChildOrder_toList hF r
  set t := toRTree hF r ord lab r
  have ht := htree t (admissible_toRTree P hF r ord hord lab hadm)
  have hsize : size t + nuSum t = Fintype.card V := by
    rw [size_toRTree hF r ord hord lab, nuSum_toRTree hF r ord hord lab]
    have hcS : Fintype.card (S : Set V) = S.card := by simp
    rw [hcS]
    simpa [lab, labOf] using hcount
  have hc : ∀ v, (lab v).2.1 + (lab v).2.2 ≤ (lab v).1 := fun v => (hadm v).1
  obtain ⟨hrel, hrelEq⟩ := rsc_relaxed P hP hF r ord hord lab hc
  rw [← hsize]
  calc K * e ^ (size t + nuSum t)
      ≤ fin P.p₂ (RSCCert.message P.p₂ P.p₃ P.y P.ϖ₂ P.ϖ₃ t) := ht
    _ = Wrel P hF r lab := hrelEq.symm
    _ ≤ Wtm P F lab := hrel
    _ ≤ Wcl G S P.p₂ P.p₃ P.y := hW

section Data
open Pointwise
open MaxLeafFormal.RSCParams
open MaxLeafFormal.RSCCert (merge init jOf)

/-- `prop:rsc-bound` with `c_Z`, conditional on the data conditions (C1), (C2), (C4), (C5). -/
theorem rsc_bound_of_data (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (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)
    (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)
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V)
    (hS : IsCDS G S) (hmin : S.card = γc G) :
    cZ p₂ Z hZ * ê ^ Fintype.card V ≤ Wcl G S p₂ p₃ y := by
  obtain ⟨⟨hp₂, hp₂₃, hp₃⟩, hy, -, -, -⟩ := rsc_side
  obtain ⟨⟨hϖ₂, hϖ₂', hϖ₃, hϖ₃'⟩, hcr⟩ := rsc_rsccredits
  have hP : (⟨p₂, p₃, y, ϖ₂, ϖ₃⟩ : Par).Standing :=
    ⟨hp₂, hp₂₃, hp₃, hy, hϖ₂, hϖ₂', hϖ₃, hϖ₃'⟩
  exact bound_of_tree_bound (⟨p₂, p₃, y, ϖ₂, ϖ₃⟩ : Par) hP hcr (cZ p₂ Z hZ) ê
    (fun t ht => rsc_tree_bound_of_data Z hZ hZ0 C1 C2 C4 C5 t ht) G hG S hS hmin

/-- `prop:rsc-bound` as stated, given also `c_Z > 0.6060`. -/
theorem rsc_bound_of_data' (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty) (hZ0 : ∀ z ∈ Z, 0 ≤ z)
    (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)
    (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)
    (hc : (6060/10000 : ℝ) < cZ p₂ Z hZ)
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V)
    (hS : IsCDS G S) (hmin : S.card = γc G) :
    (6060/10000 : ℝ) * ê ^ Fintype.card V ≤ Wcl G S p₂ p₃ y := by
  obtain ⟨-, -, ⟨hê, -⟩, -, -⟩ := rsc_side
  calc (6060/10000 : ℝ) * ê ^ Fintype.card V ≤ cZ p₂ Z hZ * ê ^ Fintype.card V :=
        mul_le_mul_of_nonneg_right hc.le (pow_nonneg hê.le _)
    _ ≤ Wcl G S p₂ p₃ y := rsc_bound_of_data Z hZ hZ0 C1 C2 C4 C5 G hG S hS hmin

end Data
end
end MaxLeafFormal.RSCGraph