MaxLeafFormal.CDS

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

Statements of the paper formalised here: Lemma 5.1, Lemma 5.9, Lemma 5.10, Lemma 5.11, Lemma 7.3.

import Mathlib
import MaxLeafFormal.Antinorm3

/-!
# The MaxLeaf–CDS graph bridge
-/

namespace MaxLeafFormal.CDS

open Finset SimpleGraph

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

def closedNbhd (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V) : Finset V :=
  X ∪ X.biUnion (fun x => G.neighborFinset x)

def IsCDS (G : SimpleGraph V) (S : Finset V) : Prop :=
  (G.induce (S : Set V)).Connected ∧ ∀ v, v ∈ S ∨ ∃ u ∈ S, G.Adj v u

noncomputable def γc (G : SimpleGraph V) : ℕ := sInf {s | ∃ S, IsCDS G S ∧ S.card = s}

noncomputable def numLeaves (F : SimpleGraph V) : ℕ :=
  (univ.filter (fun v => Nat.card (F.neighborSet v) = 1)).card

noncomputable def termCount (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V) : ℕ :=
  Fintype.card V - (closedNbhd G X).card + comp G X

/-! ### General lemmas -/

theorem mem_closedNbhd (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V) (v : V) :
    v ∈ closedNbhd G X ↔ v ∈ X ∨ ∃ x ∈ X, G.Adj x v := by
  simp [closedNbhd, mem_neighborFinset]

theorem closedNbhd_mono {F G : SimpleGraph V} [DecidableRel F.Adj] [DecidableRel G.Adj]
    (hFG : F ≤ G) (X : Finset V) : closedNbhd F X ⊆ closedNbhd G X := by
  intro v hv
  rw [mem_closedNbhd] at hv ⊢
  rcases hv with h | ⟨x, hx, h⟩
  · exact Or.inl h
  · exact Or.inr ⟨x, hx, hFG h⟩

/-- A surjective graph homomorphism does not increase the number of components. -/
theorem card_cc_le_of_surjective {α β : Type*} [Finite α] {H : SimpleGraph α} {K : SimpleGraph β}
    (f : H →g K) (hf : Function.Surjective f) :
    Nat.card K.ConnectedComponent ≤ Nat.card H.ConnectedComponent := by
  apply Nat.card_le_card_of_surjective (ConnectedComponent.map f)
  intro c
  induction c using ConnectedComponent.ind with
  | h b =>
    obtain ⟨a, rfl⟩ := hf b
    exact ⟨H.connectedComponentMk a, rfl⟩

/-- Spanning subgraphs have at least as many induced components. -/
theorem comp_le_comp_of_le {F G : SimpleGraph V} (hFG : F ≤ G) (X : Finset V) :
    comp G X ≤ comp F X := by
  unfold comp
  exact card_cc_le_of_surjective
    ⟨id, fun h => hFG h⟩ Function.surjective_id

/-- In a connected graph, a nonempty set closed under adjacency is everything. -/
theorem eq_univ_of_closed {H : SimpleGraph V} (hH : H.Connected) (A : Set V) (a : V)
    (ha : a ∈ A) (hA : ∀ u ∈ A, ∀ w, H.Adj u w → w ∈ A) (v : V) : v ∈ A := by
  obtain ⟨p⟩ := hH a v
  induction p with
  | nil => exact ha
  | cons h _ ih => exact ih (hA _ ha _ h)

/-! ### Rooted trees: a parent function -/


/-! ### 2. `lem:cds-tree` (inequality) -/

theorem tree_inequality (F : SimpleGraph V) [DecidableRel F.Adj] (hF : F.IsTree)
    (X : Finset V) (hX : X.Nonempty) :
    1 + ∑ x ∈ X, ((F.degree x : ℤ) - 1) ≤ ((closedNbhd F X).card : ℤ) - comp F X := by
  obtain ⟨r, hr⟩ := hX
  set A := univ.filter (fun w => w ≠ r ∧ par hF r w ∈ X)
  set Ain := X.filter (fun w => w ≠ r ∧ par hF r w ∈ X)
  set T := X.filter (fun t => ¬ (t ≠ r ∧ par hF r t ∈ X))
  -- the degree sum counts the children of `X`
  have hdeg : ∑ x ∈ X, ((F.degree x : ℤ) - 1) = (A.card : ℤ) - 1 := by
    have h1 : ∑ x ∈ X, (F.degree x : ℤ)
        = ∑ x ∈ X, ((univ.filter (fun w => w ≠ r ∧ par hF r w = x)).card : ℤ)
          + ∑ x ∈ X, ((if x = r then 0 else 1 : ℕ) : ℤ) := by
      rw [← sum_add_distrib]
      exact sum_congr rfl fun x _ => by rw [degree_eq_children hF r x]; push_cast; rfl
    have h2 : (A.card : ℤ) = ∑ x ∈ X, ((univ.filter (fun w => w ≠ r ∧ par hF r w = x)).card : ℤ) := by
      rw [card_eq_sum_card_fiberwise (f := par hF r) (t := X)
        (fun w hw => (mem_filter.1 hw).2.2)]
      push_cast
      refine sum_congr rfl fun x hx => ?_
      congr 2
      ext w
      simp only [A, mem_filter, mem_univ, true_and]
      constructor
      · rintro ⟨⟨h, -⟩, h'⟩; exact ⟨h, h'⟩
      · rintro ⟨h, h'⟩; exact ⟨⟨h, h' ▸ hx⟩, h'⟩
    have h3 : ∑ x ∈ X, ((if x = r then 0 else 1 : ℕ) : ℤ) = (X.card : ℤ) - 1 := by
      rw [← sum_erase_add _ _ hr, if_pos rfl, sum_congr rfl (fun x hx => by
        rw [if_neg (ne_of_mem_erase hx)])]
      have := card_pos.2 ⟨r, hr⟩
      simp [card_erase_of_mem hr]
      omega
    rw [sum_sub_distrib, h1, h2, h3, sum_const, nsmul_eq_mul, mul_one]
    ring
  -- children of `X` inside and outside `X`
  have hA : A.card = Ain.card + (A.filter (fun w => w ∉ X)).card := by
    rw [← card_filter_add_card_filter_not (fun w => w ∈ X)]
    congr 2
    ext w; simp [A, Ain, and_comm]
  have hout : (A.filter (fun w => w ∉ X)).card ≤ (closedNbhd F X).card - X.card := by
    have hsub : A.filter (fun w => w ∉ X) ⊆ closedNbhd F X \ X := by
      intro w hw
      simp only [A, mem_filter, mem_univ, true_and] at hw
      rw [mem_sdiff, mem_closedNbhd]
      exact ⟨Or.inr ⟨_, hw.1.2, (par_spec hF r hw.1.1).1.symm⟩, hw.2⟩
    have := card_le_card hsub
    rwa [card_sdiff_of_subset (fun x hx => (mem_closedNbhd F X x).2 (Or.inl hx))] at this
  have hXN : X.card ≤ (closedNbhd F X).card :=
    card_le_card (fun x hx => (mem_closedNbhd F X x).2 (Or.inl hx))
  have hT : Ain.card + T.card = X.card := card_filter_add_card_filter_not _
  have hc : comp F X ≤ T.card := comp_le_tops hF r X
  rw [hdeg]
  omega


/-! ### Spanning trees from connected dominating sets -/

theorem leaf_iff {F : SimpleGraph V} {v : V} :
    Nat.card (F.neighborSet v) = 1 ↔ ∃ u, F.neighborSet v = {u} := by
  rw [Nat.card_coe_set_eq, Set.ncard_eq_one]

theorem spanningTree_of_CDS (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    ∃ F : SimpleGraph V, F ≤ G ∧ F.IsTree ∧
      (∀ v ∉ S, Nat.card (F.neighborSet v) = 1) ∧ Fintype.card V - S.card ≤ numLeaves F := by
  classical
  obtain ⟨hconn, hdom⟩ := hS
  have hown : ∀ v, v ∉ S → ∃ u ∈ S, G.Adj v u := fun v hv => (hdom v).resolve_left hv
  let own : V → V := fun v => if hv : v ∈ S then v else Classical.choose (hown v hv)
  have own_spec : ∀ v (hv : v ∉ S), own v ∈ S ∧ G.Adj v (own v) := fun v hv => by
    simp only [own, dif_neg hv]; exact Classical.choose_spec (hown v hv)
  -- `G[S]` together with one edge from each outside vertex to its owner
  let R : V → V → Prop := fun u v => G.Adj u v ∧
    ((u ∈ S ∧ v ∈ S) ∨ (u ∉ S ∧ v = own u) ∨ (v ∉ S ∧ u = own v))
  let G' : SimpleGraph V :=
    { Adj := R
      symm := ⟨fun u v h => ⟨h.1.symm, by tauto⟩⟩
      loopless := ⟨fun u h => G.loopless.irrefl u h.1⟩ }
  have hG' : ∀ u v, G'.Adj u v ↔ R u v := fun _ _ => Iff.rfl
  have hG'G : G' ≤ G := fun u v h => ((hG' u v).1 h).1
  obtain ⟨⟨s0, hs0⟩⟩ := hconn.nonempty
  have hφ : ∀ a b : (S : Set V), (G.induce (S : Set V)).Adj a b → G'.Adj a.1 b.1 :=
    fun a b h => (hG' _ _).2 ⟨by simpa using h, Or.inl ⟨a.2, b.2⟩⟩
  let φ : G.induce (S : Set V) →g G' := ⟨Subtype.val, fun {a b} h => hφ a b h⟩
  have hreachS : ∀ u ∈ S, G'.Reachable u s0 := fun u hu =>
    (hconn.preconnected ⟨u, hu⟩ ⟨s0, hs0⟩).map φ
  have hreach : ∀ u, G'.Reachable u s0 := by
    intro u
    by_cases hu : u ∈ S
    · exact hreachS u hu
    · exact (Adj.reachable ((hG' _ _).2 ⟨(own_spec u hu).2, Or.inr (Or.inl ⟨hu, rfl⟩)⟩)).trans
        (hreachS _ (own_spec u hu).1)
  have hG'conn : G'.Connected :=
    (connected_iff _).2 ⟨fun u v => (hreach u).trans (hreach v).symm, ⟨s0⟩⟩
  obtain ⟨T, hTG', hT⟩ := hG'conn.exists_isTree_le
  have hleaf : ∀ v ∉ S, Nat.card (T.neighborSet v) = 1 := by
    intro v hv
    have hsub : T.neighborSet v ⊆ {own v} := by
      intro w hw
      rcases ((hG' _ _).1 (hTG' hw)).2 with h | h | h
      · exact absurd h.1 hv
      · exact h.2
      · exact absurd ((own_spec w h.1).1) (h.2 ▸ hv)
    have hne : own v ∈ T.neighborSet v := by
      obtain ⟨p⟩ := hT.connected v (own v)
      have hnil : ¬ p.Nil := fun h => hv (h.eq ▸ (own_spec v hv).1)
      have h := p.adj_snd hnil
      have hw : p.snd = own v := hsub h
      rw [← hw]; exact h
    rw [leaf_iff]
    exact ⟨own v, Set.Subset.antisymm hsub (Set.singleton_subset_iff.2 hne)⟩
  refine ⟨T, hTG'.trans hG'G, hT, hleaf, ?_⟩
  unfold numLeaves
  calc Fintype.card V - S.card = (univ \ S).card := by rw [card_univ_sdiff]
    _ ≤ _ := card_le_card fun v hv => mem_filter.2 ⟨mem_univ _, hleaf v (mem_sdiff.1 hv).2⟩

/-- In a spanning tree with at least 3 vertices, the non-leaves form a connected dominating
set. -/
theorem nonleaves_isCDS (G : SimpleGraph V) (hn : 3 ≤ Fintype.card V)
    (F : SimpleGraph V) (hFG : F ≤ G) (hF : F.IsTree) :
    IsCDS G (univ.filter (fun v => ¬ Nat.card (F.neighborSet v) = 1)) := by
  set S := univ.filter (fun v => ¬ Nat.card (F.neighborSet v) = 1) with hSdef
  have memS : ∀ v, v ∈ S ↔ ¬ Nat.card (F.neighborSet v) = 1 := by simp [hSdef]
  -- the neighbour of a leaf is not a leaf
  have hnb : ∀ v u, F.neighborSet v = {u} → u ∈ S := by
    intro v u hv
    rw [memS, leaf_iff]
    rintro ⟨w, hu⟩
    have hvu : F.Adj v u := by
      have : u ∈ F.neighborSet v := by rw [hv]; rfl
      exact this
    have hw : w = v := by
      have : v ∈ F.neighborSet u := hvu.symm
      rw [hu] at this; exact this.symm
    subst hw
    have hall : ∀ x, x ∈ ({w, u} : Set V) := eq_univ_of_closed hF.connected {w, u} w
      (Set.mem_insert _ _) (by
        rintro a (rfl | rfl) b hab
        · have : b ∈ F.neighborSet a := hab
          rw [hv] at this; exact Or.inr this
        · have : b ∈ F.neighborSet a := hab
          rw [hu] at this; exact Or.inl this)
    have : (univ : Finset V) ⊆ {w, u} := fun x _ => by
      have := hall x
      simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this
      simp [this]
    have := card_le_card this
    rw [card_univ] at this
    have := card_le_two (a := w) (b := u)
    omega
  have hdom : ∀ v, v ∈ S ∨ ∃ u ∈ S, G.Adj v u := by
    intro v
    by_cases hv : v ∈ S
    · exact Or.inl hv
    · rw [memS, not_not, leaf_iff] at hv
      obtain ⟨u, hu⟩ := hv
      have hvu : F.Adj v u := by
        have : u ∈ F.neighborSet v := by rw [hu]; rfl
        exact this
      exact Or.inr ⟨u, hnb v u hu, hFG hvu⟩
  refine ⟨?_, hdom⟩
  -- connectivity: walks in `F` between non-leaves can be shortcut past leaves
  have hwalk : ∀ m, ∀ a b (p : F.Walk a b) (ha : a ∈ S) (hb : b ∈ S), p.length = m →
      (G.induce (S : Set V)).Reachable ⟨a, ha⟩ ⟨b, hb⟩ := by
    intro m
    induction m using Nat.strong_induction_on with
    | _ m ih =>
      intro a b p ha hb hm
      cases p with
      | nil => exact Reachable.refl _
      | @cons _ c _ h q =>
        by_cases hc : c ∈ S
        · have hadj : (G.induce (S : Set V)).Adj ⟨a, ha⟩ ⟨c, hc⟩ := by simpa using hFG h
          exact hadj.reachable.trans (ih q.length (by simp at hm; omega) c b q hc hb rfl)
        · rw [memS, not_not, leaf_iff] at hc
          obtain ⟨u, hu⟩ := hc
          have hca : u = a := by
            have : a ∈ F.neighborSet c := h.symm
            rw [hu] at this; exact this.symm
          cases q with
          | nil =>
            exact absurd (hnb _ _ hu) (by
              rw [hca, memS, not_not]
              rw [memS] at hb
              exact absurd (by rw [leaf_iff]; exact ⟨u, hu⟩) hb)
          | @cons _ d _ h' q' =>
            have hd : d = a := by
              have : d ∈ F.neighborSet c := h'
              rw [hu] at this; rw [← hca]; exact this
            subst hd
            exact ih q'.length (by simp at hm; omega) _ b q' ha hb rfl
  rw [connected_iff]
  refine ⟨fun x y => ?_, ?_⟩
  · obtain ⟨p⟩ := hF.connected x.1 y.1
    exact hwalk _ x.1 y.1 p x.2 y.2 rfl
  · obtain ⟨v⟩ : Nonempty V := ⟨(Fintype.card_pos_iff.1 (by omega)).some⟩
    rcases hdom v with h | ⟨u, hu, -⟩
    · exact ⟨⟨v, h⟩⟩
    · exact ⟨⟨u, hu⟩⟩

theorem numLeaves_add_card (F : SimpleGraph V) :
    numLeaves F + (univ.filter (fun v => ¬ Nat.card (F.neighborSet v) = 1)).card
      = Fintype.card V := by
  unfold numLeaves
  rw [card_filter_add_card_filter_not, card_univ]

/-! ### 1. `lem:cds-maxleaf` -/

theorem numLeaves_le (G : SimpleGraph V) (hn : 3 ≤ Fintype.card V)
    (F : SimpleGraph V) (hFG : F ≤ G) (hF : F.IsTree) :
    numLeaves F ≤ Fintype.card V - γc G := by
  have hS := nonleaves_isCDS G hn F hFG hF
  have hγ : γc G ≤ (univ.filter (fun v => ¬ Nat.card (F.neighborSet v) = 1)).card :=
    Nat.sInf_le ⟨_, hS, rfl⟩
  have := numLeaves_add_card F
  omega

theorem maxLeaf_eq (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (hn : 3 ≤ Fintype.card V) :
    IsGreatest {ℓ | ∃ F : SimpleGraph V, F ≤ G ∧ F.IsTree ∧ numLeaves F = ℓ}
      (Fintype.card V - γc G) := by
  refine ⟨?_, ?_⟩
  · obtain ⟨T0, hT0G, hT0⟩ := hG.exists_isTree_le
    have hne : {s | ∃ S, IsCDS G S ∧ S.card = s}.Nonempty :=
      ⟨_, _, nonleaves_isCDS G hn T0 hT0G hT0, rfl⟩
    obtain ⟨S, hS, hSc⟩ := Nat.sInf_mem hne
    obtain ⟨F, hFG, hF, -, hle⟩ := spanningTree_of_CDS G hG S hS
    refine ⟨F, hFG, hF, le_antisymm (numLeaves_le G hn F hFG hF) ?_⟩
    change Fintype.card V - sInf _ ≤ _
    rwa [← hSc]
  · rintro ℓ ⟨F, hFG, hF, rfl⟩
    exact numLeaves_le G hn F hFG hF

/-- With at most two vertices, two vertices that differ from `v` are equal. -/
theorem eq_of_ne_of_card_le_two (hn : Fintype.card V ≤ 2) {v x y : V} (hx : x ≠ v) (hy : y ≠ v) :
    x = y := by
  by_contra hxy
  have h3 : ({v, x, y} : Finset V).card = 3 :=
    Finset.card_eq_three.mpr ⟨v, x, y, hx.symm, hy.symm, hxy, rfl⟩
  have := Finset.card_le_univ ({v, x, y} : Finset V)
  omega

/-- In a connected graph, a vertex with another vertex in the graph has a neighbour. -/
theorem exists_adj_of_connected {F : SimpleGraph V} (hF : F.Connected) {v w : V} (hvw : v ≠ w) :
    ∃ x, F.Adj v x := by
  obtain ⟨p⟩ := hF.preconnected v w
  cases p with
  | nil => exact absurd rfl hvw
  | cons h _ => exact ⟨_, h⟩

/-- `lem:cds-maxleaf`, the case `n ≤ 2`: the only spanning tree of `G` is `G` itself, with no leaf
if `n = 1` and two leaves if `n = 2`. -/
theorem maxLeaf_small (G : SimpleGraph V) (hG : G.Connected) (hn : Fintype.card V ≤ 2) :
    G.IsTree ∧ (∀ F : SimpleGraph V, F ≤ G → F.IsTree → F = G) ∧
      (Fintype.card V = 1 → numLeaves G = 0) ∧ (Fintype.card V = 2 → numLeaves G = 2) := by
  have key : ∀ F : SimpleGraph V, F ≤ G → F.IsTree → F = G := by
    intro F hFG hF
    ext u v
    constructor
    · intro h
      exact hFG h
    · intro h
      obtain ⟨x, hx⟩ := exists_adj_of_connected hF.connected (G.ne_of_adj h)
      have hxv : x = v :=
        eq_of_ne_of_card_le_two hn (F.ne_of_adj hx).symm (G.ne_of_adj h).symm
      rw [← hxv]
      exact hx
  obtain ⟨T, hTG, hT⟩ := hG.exists_isTree_le
  have hGt : G.IsTree := by
    rw [← key T hTG hT]
    exact hT
  refine ⟨hGt, key, ?_, ?_⟩
  · intro h1
    unfold numLeaves
    rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
    intro v _ hv
    obtain ⟨u, hu⟩ := leaf_iff.mp hv
    have hmem : u ∈ G.neighborSet v := by
      rw [hu]
      exact Set.mem_singleton u
    have hadj : G.Adj v u := (G.mem_neighborSet v u).mp hmem
    exact G.ne_of_adj hadj (Fintype.card_le_one_iff.mp (by omega) v u)
  · intro h2
    unfold numLeaves
    rw [Finset.filter_true_of_mem, Finset.card_univ, h2]
    intro v _
    obtain ⟨w, hw⟩ := Fintype.exists_ne_of_one_lt_card (by omega : 1 < Fintype.card V) v
    obtain ⟨x, hx⟩ := exists_adj_of_connected hGt.connected hw.symm
    refine leaf_iff.mpr ⟨x, ?_⟩
    ext y
    simp only [SimpleGraph.mem_neighborSet, Set.mem_singleton_iff]
    constructor
    · intro hy
      exact eq_of_ne_of_card_le_two hn (G.ne_of_adj hy).symm (G.ne_of_adj hx).symm
    · rintro rfl
      exact hx

/-! ### 3. `lem:cds-pointwise` -/

theorem pointwise (G : SimpleGraph V) [DecidableRel G.Adj] (hn : 2 ≤ Fintype.card V)
    (S : Finset V) (hS : IsCDS G S)
    (F : SimpleGraph V) [DecidableRel F.Adj] (hFG : F ≤ G) (hF : F.IsTree)
    (hleaf : ∀ v ∉ S, F.degree v = 1) :
    ∑ u ∈ S, ((F.degree u : ℤ) - 1) = Fintype.card V - 2 ∧
    ∀ X ⊆ S, X.Nonempty →
      1 + ∑ x ∈ X, ((F.degree x : ℤ) - 1) ≤ ((closedNbhd G X).card : ℤ) - comp G X := by
  refine ⟨?_, fun X _ hX => ?_⟩
  · have h1 : ∑ v, (F.degree v : ℤ) = 2 * ((Fintype.card V : ℤ) - 1) := by
      have := sum_degrees_eq_twice_card_edges F
      have h2 := hF.card_edgeFinset
      have : ∑ v, (F.degree v : ℤ) = 2 * (F.edgeFinset.card : ℤ) := by exact_mod_cast this
      rw [this]
      have : (F.edgeFinset.card : ℤ) + 1 = Fintype.card V := by exact_mod_cast h2
      linarith
    have h2 : ∑ v ∈ Sᶜ, (F.degree v : ℤ) = (Fintype.card V : ℤ) - S.card := by
      rw [sum_congr rfl fun v hv => by rw [hleaf v (mem_compl.1 hv)]]
      simp only [Nat.cast_one, sum_const, nsmul_eq_mul, mul_one]
      rw [card_compl, Nat.cast_sub (card_le_univ S)]
    have h3 := sum_add_sum_compl S (fun v => (F.degree v : ℤ))
    rw [sum_sub_distrib, sum_const, nsmul_eq_mul, mul_one]
    linarith
  · have h1 := tree_inequality F hF X hX
    have h2 : (closedNbhd F X).card ≤ (closedNbhd G X).card := card_le_card (closedNbhd_mono hFG X)
    have h3 := comp_le_comp_of_le hFG X
    have : ((closedNbhd F X).card : ℤ) - comp F X ≤ ((closedNbhd G X).card : ℤ) - comp G X := by
      push_cast; omega
    linarith

/-! ### 4. `lem:cds-C` -/

theorem choose_pred_mul (s t : ℕ) (ht1 : 1 ≤ t) (hts : t ≤ s) :
    ((s - 1).choose (t - 1) : ℝ) * s = (s.choose t : ℝ) * t := by
  obtain ⟨s', rfl⟩ : ∃ s', s = s' + 1 := ⟨s - 1, by omega⟩
  obtain ⟨t', rfl⟩ : ∃ t', t = t' + 1 := ⟨t - 1, by omega⟩
  have := Nat.add_one_mul_choose_eq s' t'
  simp only [Nat.add_sub_cancel]
  rw [mul_comm]
  exact_mod_cast this

theorem mean_terminals (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (hn : 2 ≤ Fintype.card V) (S : Finset V) (hS : IsCDS G S) (t : ℕ)
    (ht1 : 1 ≤ t) (hts : t ≤ S.card) :
    1 + (t : ℝ) * (Fintype.card V - 2) / S.card
      ≤ (∑ X ∈ S.powersetCard t, (((closedNbhd G X).card : ℝ) - comp G X))
          / S.card.choose t
    ∧ (∑ X ∈ S.powersetCard t, (termCount G X : ℝ)) / S.card.choose t
      ≤ Fintype.card V - 1 - (t : ℝ) * (Fintype.card V - 2) / S.card := by
  classical
  obtain ⟨F, hFG, hF, hleafF, -⟩ := spanningTree_of_CDS G hG S hS
  have hleaf : ∀ v ∉ S, F.degree v = 1 := fun v hv => by
    rw [← card_neighborSet_eq_degree, ← Nat.card_eq_fintype_card]; exact hleafF v hv
  obtain ⟨-, hpt⟩ := pointwise G hn S hS F hFG hF hleaf
  have hw := (pointwise G hn S hS F hFG hF hleaf).1
  set s := S.card with hs
  set P := S.powersetCard t
  set w : V → ℝ := fun x => (F.degree x : ℝ) - 1
  have hs0 : (0:ℝ) < s := by exact_mod_cast (show 0 < s by omega)
  have hN : (0:ℝ) < s.choose t := by exact_mod_cast Nat.choose_pos hts
  -- pointwise bound, summed
  have hX : ∀ X ∈ P, 1 + ∑ x ∈ X, w x ≤ ((closedNbhd G X).card : ℝ) - comp G X := by
    intro X hX
    rw [mem_powersetCard] at hX
    have hne : X.Nonempty := card_pos.1 (by omega)
    have := hpt X hX.1 hne
    have : ((1 + ∑ x ∈ X, ((F.degree x : ℤ) - 1) : ℤ) : ℝ)
        ≤ ((((closedNbhd G X).card : ℤ) - comp G X : ℤ) : ℝ) := by exact_mod_cast this
    push_cast at this
    exact this
  -- double counting
  have hcount : ∀ u ∈ S, (P.filter (fun X => u ∈ X)).card = (s - 1).choose (t - 1) := by
    intro u hu
    have := card_filter_powersetCard_subset {u} S t (singleton_subset_iff.2 hu)
      (by simp; omega)
    simp only [singleton_subset_iff, card_singleton] at this
    exact this
  have hdouble : ∑ X ∈ P, ∑ x ∈ X, w x = (s - 1).choose (t - 1) * ∑ u ∈ S, w u := by
    have : ∀ X ∈ P, ∑ x ∈ X, w x = ∑ u ∈ S, if u ∈ X then w u else 0 := by
      intro X hX
      rw [← sum_filter, filter_mem_eq_inter, inter_eq_right.2 (mem_powersetCard.1 hX).1]
    rw [sum_congr rfl this, sum_comm, mul_sum]
    refine sum_congr rfl fun u hu => ?_
    rw [← sum_filter, sum_const, nsmul_eq_mul, hcount u hu, mul_comm]
  have hwS : ∑ u ∈ S, w u = (Fintype.card V : ℝ) - 2 := by
    have : ((∑ u ∈ S, ((F.degree u : ℤ) - 1) : ℤ) : ℝ) = (((Fintype.card V : ℤ) - 2 : ℤ) : ℝ) := by
      rw [hw]
    push_cast at this
    exact this
  have hchoose : ((s - 1).choose (t - 1) : ℝ) * s = (s.choose t : ℝ) * t :=
    choose_pred_mul s t ht1 hts
  have hlow : (s.choose t : ℝ) + (s - 1).choose (t - 1) * ((Fintype.card V : ℝ) - 2)
      ≤ ∑ X ∈ P, (((closedNbhd G X).card : ℝ) - comp G X) := by
    calc (s.choose t : ℝ) + (s - 1).choose (t - 1) * ((Fintype.card V : ℝ) - 2)
        = ∑ X ∈ P, (1 + ∑ x ∈ X, w x) := by
          rw [sum_add_distrib, hdouble, hwS, sum_const, card_powersetCard, nsmul_eq_mul, mul_one]
      _ ≤ _ := sum_le_sum hX
  have hfirst : 1 + (t : ℝ) * (Fintype.card V - 2) / s
      ≤ (∑ X ∈ P, (((closedNbhd G X).card : ℝ) - comp G X)) / s.choose t := by
    rw [le_div_iff₀ hN]
    calc (1 + (t : ℝ) * (Fintype.card V - 2) / s) * s.choose t
        = (s.choose t : ℝ) + (s - 1).choose (t - 1) * ((Fintype.card V : ℝ) - 2) := by
          field_simp
          linear_combination (-((Fintype.card V : ℝ) - 2)) * hchoose
      _ ≤ _ := hlow
  refine ⟨hfirst, ?_⟩
  have hterm : ∀ X ∈ P, (termCount G X : ℝ)
      = Fintype.card V - (((closedNbhd G X).card : ℝ) - comp G X) := by
    intro X _
    unfold termCount
    rw [Nat.cast_add, Nat.cast_sub (card_le_univ _)]
    ring
  rw [sum_congr rfl hterm, sum_sub_distrib, sum_const, card_powersetCard, nsmul_eq_mul,
    sub_div, mul_div_cancel_left₀ _ hN.ne']
  linarith

/-! ### 5. `lem:rst-E` -/

theorem tree_reduction (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 : {v // v ∉ S} → S) (ho : ∀ v, G.Adj v.1 (o v).1) :
    let ν : S → ℕ := fun u => (univ.filter (fun v => o v = u)).card
    (∀ X : Finset S, termCount G (X.map (Function.Embedding.subtype _))
                       ≤ treePotential F ν X) ∧
    ∀ y : ℝ, 0 ≤ y →
      treeW F ν y ≤ ∑ X ∈ S.powerset, y ^ X.card * (1/2 : ℝ) ^ termCount G X := by
  classical
  intro ν
  have hpot : ∀ X : Finset S, termCount G (X.map (Function.Embedding.subtype _))
      ≤ treePotential F ν X := by
    intro X
    set Xv := X.map (Function.Embedding.subtype _) with hXv
    set N := closedNbhd G Xv
    have memXv : ∀ v : S, v.1 ∈ Xv ↔ v ∈ X := fun v => by simp [hXv]
    -- (1) outside vertices not dominated by `X` have their owner outside `X`
    set B := univ.filter (fun w : {v // v ∉ S} => w.1 ∉ N)
    have hB : (univ.filter (fun w : V => w ∉ S ∧ w ∉ N)) = B.map (Function.Embedding.subtype _) := by
      ext w; simp [B, and_comm]
    have hBsub : B ⊆ univ.filter (fun w => o w ∉ X) := by
      intro w hw
      simp only [B, mem_filter, mem_univ, true_and] at hw ⊢
      intro hoX
      apply hw
      rw [mem_closedNbhd]
      exact Or.inr ⟨(o w).1, (memXv _).2 hoX, (ho w).symm⟩
    have hsumν : ∑ v ∈ univ \ X, ν v = (univ.filter (fun w => o w ∉ X)).card := by
      rw [card_eq_sum_card_fiberwise (f := o) (t := univ \ X)
        (fun w hw => by simpa using hw)]
      refine sum_congr rfl fun v hv => ?_
      simp only [ν]
      congr 1
      ext w
      simp only [mem_filter, mem_univ, true_and]
      constructor
      · intro h; exact ⟨h ▸ (mem_sdiff.1 hv).2, h⟩
      · exact fun h => h.2
    have h1 : (univ.filter (fun w : V => w ∉ S ∧ w ∉ N)).card ≤ ∑ v ∈ univ \ X, ν v := by
      rw [hB, card_map, hsumν]; exact card_le_card hBsub
    -- (2) solution vertices not dominated by `X` are not dominated within `F`
    set C := univ.filter (fun v : S => v.1 ∉ N)
    have hC : (univ.filter (fun w : V => w ∈ S ∧ w ∉ N)) = C.map (Function.Embedding.subtype _) := by
      ext w; simp [C, and_comm]
    have h2 : (univ.filter (fun w : V => w ∈ S ∧ w ∉ N)).card
        ≤ (univ.filter (fun v => v ∉ X ∧ ∀ u, F.Adj v u → u ∉ X)).card := by
      rw [hC, card_map]
      apply card_le_card
      intro v hv
      simp only [C, mem_filter, mem_univ, true_and] at hv ⊢
      refine ⟨fun hvX => hv ((mem_closedNbhd G Xv v.1).2 (Or.inl ((memXv v).2 hvX))), ?_⟩
      intro u hvu huX
      apply hv
      rw [mem_closedNbhd]
      have : (G.induce (S : Set V)).Adj v u := hFG hvu
      exact Or.inr ⟨u.1, (memXv u).2 huX, (by simpa using this : G.Adj v.1 u.1).symm⟩
    -- (3) components
    have h3 : comp G Xv ≤ Nat.card (F.induce (X : Set S)).ConnectedComponent := by
      unfold comp
      let f : F.induce (X : Set S) →g G.induce (Xv : Set V) :=
        ⟨fun x => ⟨x.1.1, (memXv x.1).2 x.2⟩, fun {a b} h => by
          have : (G.induce (S : Set V)).Adj a.1 b.1 := hFG h
          simpa using this⟩
      apply card_cc_le_of_surjective f
      intro x
      have hx : x.1 ∈ X.map (Function.Embedding.subtype _) := x.2
      obtain ⟨v, hvX, hv⟩ := mem_map.1 hx
      exact ⟨⟨v, hvX⟩, Subtype.ext hv⟩
    -- assemble
    have hsplit : Fintype.card V - N.card = (univ.filter (fun w : V => w ∉ S ∧ w ∉ N)).card
        + (univ.filter (fun w : V => w ∈ S ∧ w ∉ N)).card := by
      rw [← card_univ_sdiff, ← card_filter_add_card_filter_not (s := univ \ N) (fun w => w ∈ S),
        add_comm]
      congr 2 <;> ext w <;> simp [and_comm]
    unfold termCount treePotential
    rw [hsplit]
    omega
  refine ⟨hpot, fun y hy => ?_⟩
  unfold treeW
  have hle : ∀ X ∈ (univ : Finset S).powerset, y ^ X.card * (1/2 : ℝ) ^ treePotential F ν X
      ≤ y ^ X.card * (1/2 : ℝ) ^ termCount G (X.map (Function.Embedding.subtype _)) := by
    intro X _
    exact mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one (by norm_num) (by norm_num) (hpot X))
      (pow_nonneg hy _)
  refine (sum_le_sum hle).trans (le_of_eq ?_)
  refine sum_nbij' (fun X => X.map (Function.Embedding.subtype _))
    (fun Y => Y.subtype (fun x => x ∈ S)) ?_ ?_ ?_ ?_ ?_
  · intro X _
    rw [mem_powerset]
    intro x hx
    rw [mem_map] at hx
    obtain ⟨v, -, rfl⟩ := hx
    exact v.2
  · intro Y _
    exact mem_powerset.2 (subset_univ _)
  · intro X _
    ext x; simp
  · intro Y hY
    rw [mem_powerset] at hY
    exact subtype_map_of_mem hY
  · intro X _
    rw [card_map]

/-! ### 6. Joint corollary with the RS-θ antinorm certificates -/

/-- The common step: a tree bound on every tree turns into a bound on `W_S(y)` for every
connected dominating set `S`. -/
theorem moment_bound_of_tree_bound.{u} (y c e₁ e₂ : ℝ) (hy : 0 ≤ y)
    (htree : ∀ (U : Type u) [Fintype U] [DecidableEq U] (T : SimpleGraph U) [DecidableRel T.Adj],
      T.IsTree → ∀ ν : U → ℕ, c * e₁ ^ Fintype.card U * e₂ ^ (∑ u, ν u) ≤ treeW T ν y)
    {V : Type u} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (S : Finset V) (hS : IsCDS G S) :
    c * e₁ ^ S.card * e₂ ^ (Fintype.card V - S.card)
      ≤ ∑ X ∈ S.powerset, y ^ X.card * (1/2 : ℝ) ^ termCount G X := by
  classical
  obtain ⟨F, hFG, hF⟩ := hS.1.exists_isTree_le
  have hown : ∀ v : {v // v ∉ S}, ∃ u : S, G.Adj v.1 u.1 := by
    intro v
    rcases hS.2 v.1 with h | ⟨u, hu, huv⟩
    · exact absurd h v.2
    · exact ⟨⟨u, hu⟩, huv⟩
  choose o ho using hown
  have hred := (tree_reduction G hG S hS F hFG hF o ho).2 y hy
  have hb := htree S F hF (fun u => (univ.filter (fun v => o v = u)).card)
  have hcard : Fintype.card S = S.card := Fintype.card_coe S
  have hsum : ∑ u : S, (univ.filter (fun v : {v // v ∉ S} => o v = u)).card
      = Fintype.card V - S.card := by
    rw [← card_eq_sum_card_fiberwise (fun v _ => mem_univ (o v)), card_univ,
      Fintype.card_subtype_compl, Fintype.card_coe]
  rw [hcard, hsum] at hb
  exact hb.trans hred

/-- The joint corollary for certificate 0. -/
theorem rstheta_moment_bound_0
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    (6212/10000 : ℝ) * (747593601/960952792 : ℝ) ^ S.card
        * (512099210/652701491 : ℝ) ^ (Fintype.card V - S.card)
      ≤ ∑ X ∈ S.powerset, (69/200 : ℝ) ^ X.card * (1/2 : ℝ) ^ termCount G X :=
  moment_bound_of_tree_bound _ _ _ _ (by norm_num)
    (fun _ _ _ T _ hT ν => rstheta_tree_bound_0 T hT ν) G hG S hS

/-- The joint corollary for certificate 1. -/
theorem rstheta_moment_bound_1
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected)
    (S : Finset V) (hS : IsCDS G S) :
    (6293/10000 : ℝ) * (248231700/312721579 : ℝ) ^ S.card
        * (568097827/739289481 : ℝ) ^ (Fintype.card V - S.card)
      ≤ ∑ X ∈ S.powerset, (17/50 : ℝ) ^ X.card * (1/2 : ℝ) ^ termCount G X :=
  moment_bound_of_tree_bound _ _ _ _ (by norm_num)
    (fun _ _ _ T _ hT ν => rstheta_tree_bound_1 T hT ν) G hG S hS

end MaxLeafFormal.CDS