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