MaxLeafFormal.CCGibbs

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

Statements of the paper formalised here: Lemma 11.2, Lemma 11.3.

import MaxLeafFormal.CCRate
import MaxLeafFormal.Rooted
import MaxLeafFormal.Antinorm3

/-!
# The tree partition function: `lem:cc-gibbs` and `lem:cc-path`

The paper's `def:cc-Z`, `lem:cc-gibbs` and `lem:cc-path`.

Proof routes. `cc_gibbs` follows this route: the subtree sums `g0`, `g1` of a
rooted tree (the subtree structure of `Antinorm3`), and the logarithmic potential
`Ψ = π₀ log g(0) + π₁ log g(1)`, which gains `log λ - π₁ log ζ` at every edge by two weighted
Jensen steps for `log` (`key_step`), with the stochastic matrix and the stationary law of the
Doob transform of `M_ζ`. `cc_path` uses the same split along the path and a scalar recursion for
the gap `(1 + ζ) λ^m - 𝒵`.
-/

namespace MaxLeafFormal.CCGibbs

open Finset SimpleGraph
open MaxLeafFormal.CCRate (spr spr_root)

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

open Classical in
/-- `e(F[X])`: the number of edges of `F` with both ends in `X` (`def:cc-Z`). -/
noncomputable def eIn (F : SimpleGraph V) (X : Finset V) : ℕ :=
  (F.edgeFinset.filter (fun e => ∀ v ∈ e, v ∈ X)).card

/-- `𝒵_F(ζ) = ∑_{X ⊆ V(F)} ζ^{|X|} 2^{e(F[X])}` (`def:cc-Z`). -/
noncomputable def Zpart (F : SimpleGraph V) (ζ : ℝ) : ℝ :=
  ∑ X ∈ (univ : Finset V).powerset, ζ ^ X.card * (2 : ℝ) ^ eIn F X

/-! ### Edge counts -/

omit [Fintype V] [DecidableEq V] in

theorem sym2_forall_mem_iff {p : V → Prop} (a b : V) :
    (∀ x ∈ s(a, b), p x) ↔ p a ∧ p b := by
  constructor
  · intro h
    exact ⟨h a (Sym2.mem_mk_left a b), h b (Sym2.mem_mk_right a b)⟩
  · rintro ⟨ha, hb⟩ x hx
    rcases Sym2.mem_iff.mp hx with rfl | rfl
    · exact ha
    · exact hb

theorem eIn_empty (F : SimpleGraph V) : eIn F ∅ = 0 := by
  classical
  unfold eIn
  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
  intro e _ h
  induction e using Sym2.ind with
  | _ a b => simpa using h a (Sym2.mem_mk_left a b)

theorem eIn_singleton (F : SimpleGraph V) (v : V) : eIn F {v} = 0 := by
  classical
  unfold eIn
  rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff]
  intro e he h
  induction e using Sym2.ind with
  | _ a b =>
    have ha : a ∈ ({v} : Finset V) := h a (Sym2.mem_mk_left a b)
    have hb : b ∈ ({v} : Finset V) := h b (Sym2.mem_mk_right a b)
    rw [Finset.mem_singleton] at ha hb
    have hadj : F.Adj a b := by simpa using he
    rw [ha, hb] at hadj
    simp at hadj

/-- Edge count of a union of two pieces `Y ⊆ A`, `Z ⊆ B` of disjoint sets joined by the single
edge `v w`. -/
theorem eIn_union {F : SimpleGraph V} {A B Y Z : Finset V} {v w : V} (hAB : Disjoint A B)
    (hY : Y ⊆ A) (hZ : Z ⊆ B) (hv : v ∈ A) (hw : w ∈ B) (hvw : F.Adj v w)
    (hedge : ∀ a ∈ A, ∀ b ∈ B, F.Adj a b → a = v ∧ b = w) :
    eIn F (Y ∪ Z) = eIn F Y + eIn F Z + if v ∈ Y ∧ w ∈ Z then 1 else 0 := by
  classical
  unfold eIn
  have hdisj : Disjoint (F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Y))
      (F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Z)) := by
    rw [Finset.disjoint_left]
    intro e he1 he2
    rw [Finset.mem_filter] at he1 he2
    induction e using Sym2.ind with
    | _ a b =>
      exact Finset.disjoint_left.mp hAB (hY (he1.2 a (Sym2.mem_mk_left a b)))
        (hZ (he2.2 a (Sym2.mem_mk_left a b)))
  have hsplit : F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Y ∪ Z) =
      (F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Y) ∪
        F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Z)) ∪
      (if v ∈ Y ∧ w ∈ Z then {s(v, w)} else ∅) := by
    ext e
    induction e using Sym2.ind with
    | _ a b =>
      by_cases hc : v ∈ Y ∧ w ∈ Z
      · simp only [Finset.mem_filter, Finset.mem_union, SimpleGraph.mem_edgeFinset,
          SimpleGraph.mem_edgeSet, sym2_forall_mem_iff, if_pos hc, Finset.mem_singleton]
        constructor
        · rintro ⟨hadj, ha | ha, hb | hb⟩
          · exact Or.inl (Or.inl ⟨hadj, ha, hb⟩)
          · obtain ⟨h1, h2⟩ := hedge a (hY ha) b (hZ hb) hadj
            exact Or.inr (by rw [h1, h2])
          · obtain ⟨h1, h2⟩ := hedge b (hY hb) a (hZ ha) hadj.symm
            exact Or.inr (by rw [← h1, ← h2]; exact Sym2.eq_swap)
          · exact Or.inl (Or.inr ⟨hadj, ha, hb⟩)
        · rintro ((⟨hadj, ha, hb⟩ | ⟨hadj, ha, hb⟩) | heq)
          · exact ⟨hadj, Or.inl ha, Or.inl hb⟩
          · exact ⟨hadj, Or.inr ha, Or.inr hb⟩
          · rcases Sym2.eq_iff.mp heq with ⟨h1, h2⟩ | ⟨h1, h2⟩
            · subst h1
              subst h2
              exact ⟨hvw, Or.inl hc.1, Or.inr hc.2⟩
            · subst h1
              subst h2
              exact ⟨hvw.symm, Or.inr hc.2, Or.inl hc.1⟩
      · simp only [Finset.mem_filter, Finset.mem_union, SimpleGraph.mem_edgeFinset,
          SimpleGraph.mem_edgeSet, sym2_forall_mem_iff, if_neg hc]
        constructor
        · rintro ⟨hadj, ha | ha, hb | hb⟩
          · exact Or.inl (Or.inl ⟨hadj, ha, hb⟩)
          · obtain ⟨h1, h2⟩ := hedge a (hY ha) b (hZ hb) hadj
            exact (hc ⟨by rw [← h1]; exact ha, by rw [← h2]; exact hb⟩).elim
          · obtain ⟨h1, h2⟩ := hedge b (hY hb) a (hZ ha) hadj.symm
            exact (hc ⟨by rw [← h1]; exact hb, by rw [← h2]; exact ha⟩).elim
          · exact Or.inl (Or.inr ⟨hadj, ha, hb⟩)
        · rintro ((⟨hadj, ha, hb⟩ | ⟨hadj, ha, hb⟩) | heq)
          · exact ⟨hadj, Or.inl ha, Or.inl hb⟩
          · exact ⟨hadj, Or.inr ha, Or.inr hb⟩
          · simp at heq
  have hdisjR : Disjoint
      (F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Y) ∪
        F.edgeFinset.filter (fun e => ∀ x ∈ e, x ∈ Z))
      (if v ∈ Y ∧ w ∈ Z then {s(v, w)} else ∅) := by
    split_ifs with hc
    · rw [Finset.disjoint_singleton_right]
      intro h
      rcases Finset.mem_union.mp h with h | h
      · rw [Finset.mem_filter] at h
        exact Finset.disjoint_left.mp hAB (hY (h.2 w (Sym2.mem_mk_right v w))) hw
      · rw [Finset.mem_filter] at h
        exact Finset.disjoint_left.mp hAB hv (hZ (h.2 v (Sym2.mem_mk_left v w)))
    · simp
  rw [hsplit, Finset.card_union_of_disjoint hdisjR, Finset.card_union_of_disjoint hdisj]
  split_ifs <;> simp

theorem sym2_pair_map {α β : Type*} (f : α → β) (x y : α) :
    Sym2.map f s(x, y) = s(f x, f y) := rfl

omit [Fintype V] [DecidableEq V] in

theorem sym2_map_mem_edgeSet_iff {W : Type*} {F : SimpleGraph V} {G : SimpleGraph W}
    (σ : V ≃ W) (hσ : ∀ a b, F.Adj a b ↔ G.Adj (σ a) (σ b)) (a : Sym2 V) :
    Sym2.map σ a ∈ G.edgeSet ↔ a ∈ F.edgeSet := by
  refine Sym2.inductionOn a (fun x y => ?_)
  simp only [sym2_pair_map, SimpleGraph.mem_edgeSet]
  exact (hσ x y).symm

omit [Fintype V] [DecidableEq V] in

theorem sym2_map_symm_map {W : Type*} (σ : V ≃ W) (b : Sym2 W) :
    Sym2.map σ (Sym2.map σ.symm b) = b := by
  refine Sym2.inductionOn b (fun x y => ?_)
  simp only [sym2_pair_map, Equiv.apply_symm_apply]

omit [Fintype V] [DecidableEq V] in

theorem sym2_symm_map_map {W : Type*} (σ : V ≃ W) (a : Sym2 V) :
    Sym2.map σ.symm (Sym2.map σ a) = a := by
  refine Sym2.inductionOn a (fun x y => ?_)
  simp only [sym2_pair_map, Equiv.symm_apply_apply]

open Classical in
theorem eIn_map_equiv {W : Type*} [Fintype W] [DecidableEq W]
    {F : SimpleGraph V} {G : SimpleGraph W}
    (σ : V ≃ W) (hσ : ∀ a b, F.Adj a b ↔ G.Adj (σ a) (σ b)) (X : Finset V) :
    eIn G (X.map σ.toEmbedding) = eIn F X := by
  unfold eIn
  symm
  refine Finset.card_nbij' (Sym2.map σ) (Sym2.map σ.symm) ?_ ?_ ?_ ?_
  · intro a ha
    obtain ⟨ha1, ha2⟩ := Finset.mem_filter.mp ha
    apply Finset.mem_filter.mpr
    refine ⟨SimpleGraph.mem_edgeFinset.mpr
      ((sym2_map_mem_edgeSet_iff σ hσ a).mpr (SimpleGraph.mem_edgeFinset.mp ha1)),
      fun v hv => ?_⟩
    obtain ⟨c, hc, rfl⟩ := Sym2.mem_map.mp hv
    exact Finset.mem_map_of_mem _ (ha2 c hc)
  · intro b hb
    obtain ⟨hb1, hb2⟩ := Finset.mem_filter.mp hb
    apply Finset.mem_filter.mpr
    have hb' : Sym2.map σ.symm b ∈ F.edgeSet :=
      (sym2_map_mem_edgeSet_iff σ hσ (Sym2.map σ.symm b)).mp (by
        rw [sym2_map_symm_map]
        exact SimpleGraph.mem_edgeFinset.mp hb1)
    refine ⟨SimpleGraph.mem_edgeFinset.mpr hb', fun v hv => ?_⟩
    obtain ⟨c, hc, rfl⟩ := Sym2.mem_map.mp hv
    obtain ⟨x, hx, hxc⟩ := Finset.mem_map.mp (hb2 c hc)
    rw [← hxc]
    simpa using hx
  · intro a _
    exact sym2_symm_map_map σ a
  · intro b _
    exact sym2_map_symm_map σ b

theorem pg_two_edge (e : Sym2 (Fin 2)) : e ∈ (pathGraph 2).edgeSet → e = s(0, 1) := by
  refine Sym2.inductionOn e (fun x y => ?_)
  intro he
  have hadj : (pathGraph 2).Adj x y := (SimpleGraph.mem_edgeSet _).mp he
  have hne : x ≠ y := hadj.ne
  fin_cases x <;> fin_cases y <;>
    first
    | exact (hne rfl).elim
    | rfl
    | exact Sym2.eq_swap

open Classical in
/-- Filter membership for the edge filter of `eIn`, stated generically. -/
theorem mem_filter_edges (s : Finset (Sym2 V)) (X : Finset V) (e : Sym2 V) :
    e ∈ s.filter (fun e => ∀ v ∈ e, v ∈ X) ↔ e ∈ s ∧ ∀ v ∈ e, v ∈ X :=
  Finset.mem_filter

open Classical in
/-- `eIn` depends only on the edge set, given as a finset. -/
theorem eIn_eq_filter_of_edges (F : SimpleGraph V) (s : Finset (Sym2 V))
    (hs : ∀ e, e ∈ F.edgeSet ↔ e ∈ s) (X : Finset V) :
    eIn F X = (s.filter (fun e => ∀ v ∈ e, v ∈ X)).card := by
  unfold eIn
  congr 1
  ext e
  rw [mem_filter_edges, mem_filter_edges, SimpleGraph.mem_edgeFinset, hs]

open Classical in
theorem eIn_pg2 (X : Finset (Fin 2)) :
    eIn (pathGraph 2) X = if (0 ∈ X ∧ 1 ∈ X) then 1 else 0 := by
  have adj01 : (pathGraph 2).Adj 0 1 := by simp [SimpleGraph.pathGraph_adj]
  have hs : ∀ e, e ∈ (pathGraph 2).edgeSet ↔ e ∈ ({s(0, 1)} : Finset (Sym2 (Fin 2))) := by
    intro e
    rw [Finset.mem_singleton]
    constructor
    · exact pg_two_edge e
    · rintro rfl
      exact (SimpleGraph.mem_edgeSet _).mpr adj01
  rw [eIn_eq_filter_of_edges _ _ hs X]
  split_ifs with h
  · rw [Finset.card_eq_one]
    refine ⟨s(0, 1), ?_⟩
    ext e
    rw [mem_filter_edges]
    simp only [Finset.mem_singleton]
    constructor
    · rintro ⟨h', _⟩
      exact h'
    · rintro rfl
      refine ⟨rfl, fun v hv => ?_⟩
      rcases Sym2.mem_iff.mp hv with rfl | rfl
      · exact h.1
      · exact h.2
  · rw [Finset.card_eq_zero]
    ext e
    rw [mem_filter_edges, Finset.mem_singleton]
    constructor
    · rintro ⟨rfl, hP⟩
      exact (h ⟨hP 0 (Sym2.mem_mk_left _ _), hP 1 (Sym2.mem_mk_right _ _)⟩).elim
    · intro hm
      simp at hm

/-! ### The closed form `λ = spr ζ` and the weights of the potential -/

theorem one_add_le_spr (ζ : ℝ) : 1 + ζ ≤ spr ζ := by
  have h1 : Real.sqrt 1 ≤ Real.sqrt (1 + 4 * ζ ^ 2) :=
    Real.sqrt_le_sqrt (by nlinarith [sq_nonneg ζ])
  rw [Real.sqrt_one] at h1
  unfold spr
  linarith

theorem spr_pos_of_nonneg {ζ : ℝ} (hζ : 0 ≤ ζ) : 0 < spr ζ := by
  have := one_add_le_spr ζ
  linarith

lemma spr_gt {ζ : ℝ} (hζ : 0 < ζ) : 1 < spr ζ := by
  linarith [one_add_le_spr ζ]

/-- π₀ -/
noncomputable def piw (ζ : ℝ) : ℝ := ζ / (ζ + (spr ζ - 1) ^ 2)

/-- π₁ -/
noncomputable def piv (ζ : ℝ) : ℝ := (spr ζ - 1) ^ 2 / (ζ + (spr ζ - 1) ^ 2)

lemma pi_den_pos {ζ : ℝ} (hζ : 0 < ζ) : 0 < ζ + (spr ζ - 1) ^ 2 := by
  nlinarith [sq_nonneg (spr ζ - 1)]

theorem pi_facts {ζ : ℝ} (hζ : 0 < ζ) : 0 ≤ piw ζ ∧ 0 ≤ piv ζ ∧ piw ζ + piv ζ = 1 := by
  have hN := pi_den_pos hζ
  unfold piw piv
  refine ⟨div_nonneg hζ.le hN.le, div_nonneg (sq_nonneg _) hN.le, ?_⟩
  exact ((add_div _ _ _).symm).trans (div_self hN.ne')

/-- Two-point concavity of `log` (weighted Jensen). -/
theorem log_two_point {a b x y : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hx : 0 < x)
    (hy : 0 < y) : a * Real.log x + b * Real.log y ≤ Real.log (a * x + b * y) := by
  have h := (strictConcaveOn_log_Ioi.concaveOn).2 (Set.mem_Ioi.mpr hx) (Set.mem_Ioi.mpr hy) ha hb hab
  simpa only [smul_eq_mul] using h

lemma row0_log {l m b0 b1 : ℝ} (hl : 0 < l) (hm : 0 < m) (hsum : 1 / l + m / l = 1)
    (h0 : 0 < b0) (h1 : 0 < b1) :
    Real.log l + (1 / l) * Real.log b0 + (m / l) * Real.log b1 - (m / l) * Real.log m
      ≤ Real.log (b0 + b1) := by
  have hl0 : l ≠ 0 := hl.ne'
  have hm0 : m ≠ 0 := hm.ne'
  have key := log_two_point (a := 1 / l) (b := m / l) (x := l * b0) (y := l * b1 / m)
    (div_nonneg zero_le_one hl.le) (div_nonneg hm.le hl.le) hsum
    (mul_pos hl h0) (div_pos (mul_pos hl h1) hm)
  have e : 1 / l * (l * b0) + m / l * (l * b1 / m) = b0 + b1 := by
    field_simp
  rw [e, Real.log_mul hl0 h0.ne', Real.log_div (mul_ne_zero hl0 h1.ne') hm0,
    Real.log_mul hl0 h1.ne'] at key
  have hlog : Real.log l = (1 / l + m / l) * Real.log l := by rw [hsum, one_mul]
  have eq : Real.log l + (1 / l) * Real.log b0 + (m / l) * Real.log b1 - (m / l) * Real.log m
      = 1 / l * (Real.log l + Real.log b0) + m / l * (Real.log l + Real.log b1 - Real.log m) := by
    linear_combination hlog
  linarith [key, eq]

lemma row1_log {ζ l m b0 b1 : ℝ} (hζ : 0 < ζ) (hl : 0 < l) (hm : 0 < m)
    (hsum : ζ / (l * m) + 2 * ζ / l = 1) (h0 : 0 < b0) (h1 : 0 < b1) :
    Real.log l - Real.log ζ + (ζ / (l * m)) * Real.log m + (ζ / (l * m)) * Real.log b0
      + (2 * ζ / l) * Real.log b1 ≤ Real.log (b0 + 2 * b1) := by
  have hl0 : l ≠ 0 := hl.ne'
  have hm0 : m ≠ 0 := hm.ne'
  have hζ0 : ζ ≠ 0 := hζ.ne'
  have key := log_two_point (a := ζ / (l * m)) (b := 2 * ζ / l) (x := l * m * b0 / ζ)
    (y := l * b1 / ζ)
    (div_nonneg hζ.le (mul_pos hl hm).le) (div_nonneg (by linarith) hl.le) hsum
    (div_pos (mul_pos (mul_pos hl hm) h0) hζ) (div_pos (mul_pos hl h1) hζ)
  have e : ζ / (l * m) * (l * m * b0 / ζ) + 2 * ζ / l * (l * b1 / ζ) = b0 + 2 * b1 := by
    field_simp
  rw [e, Real.log_div (mul_ne_zero (mul_ne_zero hl0 hm0) h0.ne') hζ0,
    Real.log_mul (mul_ne_zero hl0 hm0) h0.ne', Real.log_mul hl0 hm0,
    Real.log_div (mul_ne_zero hl0 h1.ne') hζ0, Real.log_mul hl0 h1.ne'] at key
  have eq : ζ / (l * m) * (Real.log l + Real.log m + Real.log b0 - Real.log ζ)
      + 2 * ζ / l * (Real.log l + Real.log b1 - Real.log ζ)
      = Real.log l - Real.log ζ + (ζ / (l * m)) * Real.log m + (ζ / (l * m)) * Real.log b0
        + (2 * ζ / l) * Real.log b1 := by
    linear_combination (Real.log l - Real.log ζ) * hsum
  linarith [key, eq]

lemma coef_facts {ζ l : ℝ} (hζ : 0 < ζ) (hl : 1 < l) (hL : l ^ 2 - (1 + 2 * ζ) * l + ζ = 0) :
    ζ / (ζ + (l - 1) ^ 2) * (1 / l) + (l - 1) ^ 2 / (ζ + (l - 1) ^ 2) * (ζ / (l * (l - 1)))
        = ζ / (ζ + (l - 1) ^ 2) ∧
    ζ / (ζ + (l - 1) ^ 2) * ((l - 1) / l) + (l - 1) ^ 2 / (ζ + (l - 1) ^ 2) * (2 * ζ / l)
        = (l - 1) ^ 2 / (ζ + (l - 1) ^ 2) ∧
    -(ζ / (ζ + (l - 1) ^ 2) * ((l - 1) / l))
        + (l - 1) ^ 2 / (ζ + (l - 1) ^ 2) * (ζ / (l * (l - 1))) = 0 := by
  have hN : 0 < ζ + (l - 1) ^ 2 := by nlinarith [sq_nonneg (l - 1)]
  have hN0 : ζ + (l - 1) ^ 2 ≠ 0 := hN.ne'
  have hl0 : l ≠ 0 := (by linarith : (0:ℝ) < l).ne'
  have hm0 : l - 1 ≠ 0 := (by linarith : (0:ℝ) < l - 1).ne'
  refine ⟨?_, ?_, ?_⟩
  · field_simp <;> ring
  · rw [div_mul_div_comm, div_mul_div_comm, ← add_div,
      div_eq_div_iff (mul_ne_zero hN0 hl0) hN0]
    linear_combination (-(ζ + (l - 1) ^ 2) * (l - 1)) * hL
  · field_simp <;> ring

lemma jensen_combine {w v lL lz lb0 lb1 lm L0 L1 p00 p01 p10 p11 : ℝ}
    (hw : 0 ≤ w) (hv : 0 ≤ v) (hwv : w + v = 1)
    (c0 : w * p00 + v * p10 = w) (c1 : w * p01 + v * p11 = v)
    (c2 : -(w * p01) + v * p10 = 0)
    (R0 : lL + p00 * lb0 + p01 * lb1 - p01 * lm ≤ L0)
    (R1 : lL - lz + p10 * lm + p10 * lb0 + p11 * lb1 ≤ L1) :
    lL - v * lz + (w * lb0 + v * lb1) ≤ w * L0 + v * L1 := by
  have A := mul_le_mul_of_nonneg_left R0 hw
  have B := mul_le_mul_of_nonneg_left R1 hv
  have E : lL - v * lz + (w * lb0 + v * lb1)
      = w * (lL + p00 * lb0 + p01 * lb1 - p01 * lm)
        + v * (lL - lz + p10 * lm + p10 * lb0 + p11 * lb1) := by
    linear_combination (-lL) * hwv - lb0 * c0 - lb1 * c1 - lm * c2
  linarith [A, B, E]

theorem key_step {ζ : ℝ} (hζ : 0 < ζ) {b0 b1 : ℝ} (h0 : 0 < b0) (h1 : 0 < b1) :
    Real.log (spr ζ) - piv ζ * Real.log ζ + (piw ζ * Real.log b0 + piv ζ * Real.log b1)
      ≤ piw ζ * Real.log (b0 + b1) + piv ζ * Real.log (b0 + 2 * b1) := by
  have hgt := spr_gt hζ
  have hl : 0 < spr ζ := by linarith
  have hm : 0 < spr ζ - 1 := by linarith
  have hL := spr_root ζ
  obtain ⟨hw, hv, hwv⟩ := pi_facts hζ
  have hsum0 : 1 / spr ζ + (spr ζ - 1) / spr ζ = 1 := by
    rw [← add_div, div_eq_one_iff_eq hl.ne']
    ring
  have hsum1 : ζ / (spr ζ * (spr ζ - 1)) + 2 * ζ / spr ζ = 1 := by
    rw [div_add_div _ _ (mul_ne_zero hl.ne' hm.ne') hl.ne',
      div_eq_one_iff_eq (mul_ne_zero (mul_ne_zero hl.ne' hm.ne') hl.ne')]
    linear_combination (-(spr ζ)) * hL
  have R0 := row0_log hl hm hsum0 h0 h1
  have R1 := row1_log hζ hl hm hsum1 h0 h1
  have c0 : piw ζ * (1 / spr ζ) + piv ζ * (ζ / (spr ζ * (spr ζ - 1))) = piw ζ := by
    unfold piw piv
    exact (coef_facts hζ hgt hL).1
  have c1 : piw ζ * ((spr ζ - 1) / spr ζ) + piv ζ * (2 * ζ / spr ζ) = piv ζ := by
    unfold piw piv
    exact (coef_facts hζ hgt hL).2.1
  have c2 : -(piw ζ * ((spr ζ - 1) / spr ζ)) + piv ζ * (ζ / (spr ζ * (spr ζ - 1))) = 0 := by
    unfold piw piv
    exact (coef_facts hζ hgt hL).2.2
  exact jensen_combine hw hv hwv c0 c1 c2 R0 R1

theorem root_step {ζ : ℝ} (hζ : 0 < ζ) {p0 p1 : ℝ} (h0 : 0 < p0) (h1 : 0 < p1) :
    piw ζ * Real.log p0 + piv ζ * Real.log p1 ≤ Real.log (p0 + p1) := by
  obtain ⟨hw, hv, hwv⟩ := pi_facts hζ
  have hgt := spr_gt hζ
  have hm : 0 < spr ζ - 1 := by linarith
  have hN := pi_den_pos hζ
  have hwp : 0 < piw ζ := by unfold piw; exact div_pos hζ hN
  have hvp : 0 < piv ζ := by unfold piv; exact div_pos (pow_pos hm 2) hN
  have J := log_two_point hw hv hwv h0 h1
  have hw1 : piw ζ ≤ 1 := by linarith
  have hv1 : piv ζ ≤ 1 := by linarith
  have hle : piw ζ * p0 + piv ζ * p1 ≤ p0 + p1 := by
    nlinarith [mul_le_mul_of_nonneg_right hw1 h0.le, mul_le_mul_of_nonneg_right hv1 h1.le]
  have hpos : 0 < piw ζ * p0 + piv ζ * p1 := add_pos (mul_pos hwp h0) (mul_pos hvp h1)
  have hlog := Real.log_le_log hpos hle
  linarith [J, hlog]

theorem min_step {ζ : ℝ} (hζ : 0 < ζ) : Real.log (min 1 ζ) ≤ piv ζ * Real.log ζ := by
  obtain ⟨hw, hv, hwv⟩ := pi_facts hζ
  rcases le_total 1 ζ with h | h
  · rw [min_eq_left h, Real.log_one]
    exact mul_nonneg hv (Real.log_nonneg h)
  · rw [min_eq_right h]
    have hlog : Real.log ζ ≤ 0 := Real.log_nonpos hζ.le h
    have h3 : 0 ≤ piw ζ * (-Real.log ζ) := mul_nonneg hw (by linarith)
    have hp : piw ζ = 1 - piv ζ := by linarith
    rw [hp] at h3
    nlinarith [h3]

/-! ### Sums over the subsets of a vertex set, split on one vertex -/

section Sums

variable (F : SimpleGraph V) (ζ : ℝ)

/-- The weight `ζ^{|X|} 2^{e(F[X])}` of a set `X`. -/
noncomputable def tw (X : Finset V) : ℝ := ζ ^ X.card * (2 : ℝ) ^ eIn F X

/-- The sum of the weights of the subsets of `S` that avoid `v`. -/
noncomputable def g0 (S : Finset V) (v : V) : ℝ :=
  ∑ X ∈ S.powerset, if v ∈ X then 0 else tw F ζ X

/-- The sum of the weights of the subsets of `S` that contain `v`. -/
noncomputable def g1 (S : Finset V) (v : V) : ℝ :=
  ∑ X ∈ S.powerset, if v ∈ X then tw F ζ X else 0

theorem Zpart_eq_g (r : V) : Zpart F ζ = g0 F ζ univ r + g1 F ζ univ r := by
  unfold Zpart g0 g1
  rw [← sum_add_distrib]
  refine sum_congr rfl (fun X _ => ?_)
  unfold tw
  split_ifs <;> simp

theorem tw_nonneg (hζ : 0 ≤ ζ) (X : Finset V) : 0 ≤ tw F ζ X := by
  unfold tw; positivity

theorem tw_empty : tw F ζ ∅ = 1 := by simp [tw, eIn_empty]

theorem tw_singleton (v : V) : tw F ζ {v} = ζ := by simp [tw, eIn_singleton]

omit [Fintype V] in

theorem powerset_singleton' (v : V) : ({v} : Finset V).powerset = {∅, {v}} := by
  ext X; simp [subset_singleton_iff]

theorem g0_single (v : V) : g0 F ζ {v} v = 1 := by
  rw [g0, powerset_singleton', sum_pair (singleton_ne_empty v).symm]
  simp [tw_empty]

theorem g1_single (v : V) : g1 F ζ {v} v = ζ := by
  rw [g1, powerset_singleton', sum_pair (singleton_ne_empty v).symm]
  simp [tw_singleton]

theorem g0_pos (hζ : 0 ≤ ζ) (S : Finset V) (v : V) : 0 < g0 F ζ S v := by
  unfold g0
  have h := single_le_sum (f := fun X => if v ∈ X then 0 else tw F ζ X)
    (fun X _ => by split_ifs; exacts [le_rfl, tw_nonneg F ζ hζ X])
    (empty_mem_powerset S)
  simp only [notMem_empty, if_false, tw_empty] at h
  exact lt_of_lt_of_le one_pos h

theorem g1_pos (hζ : 0 < ζ) (S : Finset V) (v : V) (hv : v ∈ S) : 0 < g1 F ζ S v := by
  unfold g1
  have h := single_le_sum (f := fun X => if v ∈ X then tw F ζ X else 0)
    (fun X _ => by split_ifs; exacts [tw_nonneg F ζ hζ.le X, le_rfl])
    (mem_powerset.2 (singleton_subset_iff.2 hv))
  simp only [mem_singleton, if_true, tw_singleton] at h
  exact lt_of_lt_of_le hζ h

variable {F ζ}
variable {A B : Finset V} {v w : V} (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B)
  (hvw : F.Adj v w) (hedge : ∀ a ∈ A, ∀ b ∈ B, F.Adj a b → a = v ∧ b = w)

include hAB hv hw hvw hedge in

theorem tw_union {Y Z : Finset V} (hY : Y ⊆ A) (hZ : Z ⊆ B) :
    tw F ζ (Y ∪ Z) = tw F ζ Y * tw F ζ Z * (if v ∈ Y ∧ w ∈ Z then 2 else 1) := by
  have hYZ : Disjoint Y Z := disjoint_of_subset_left hY (disjoint_of_subset_right hZ hAB)
  unfold tw
  rw [card_union_of_disjoint hYZ, eIn_union hAB hY hZ hv hw hvw hedge]
  simp only [pow_add]
  split_ifs <;> ring

include hAB hv hw hvw hedge in

/-- Adding the part `B` (tracked vertex `w`) below the vertex `v` of the part `A`. -/
theorem g_union :
    g0 F ζ (A ∪ B) v = g0 F ζ A v * (g0 F ζ B w + g1 F ζ B w) ∧
    g1 F ζ (A ∪ B) v = g1 F ζ A v * (g0 F ζ B w + 2 * g1 F ζ B w) := by
  have hvB : v ∉ B := fun h => disjoint_left.1 hAB hv h
  constructor
  · unfold g0 g1
    rw [Antinorm3.sum_powerset_union hAB, ← sum_add_distrib, sum_mul_sum]
    refine sum_congr rfl (fun Y hY => sum_congr rfl (fun Z hZ => ?_))
    rw [mem_powerset] at hY hZ
    have hvZ : v ∉ Z := fun h => hvB (hZ h)
    rw [tw_union hAB hv hw hvw hedge hY hZ]
    by_cases hvY : v ∈ Y <;> by_cases hwZ : w ∈ Z <;>
      simp only [mem_union, hvY, hwZ, hvZ, and_self, and_true, true_and, and_false,
        false_and, or_true, true_or, or_false, false_or, ↓reduceIte] <;> ring
  · unfold g0 g1
    rw [Antinorm3.sum_powerset_union hAB, mul_sum, ← sum_add_distrib, sum_mul_sum]
    refine sum_congr rfl (fun Y hY => sum_congr rfl (fun Z hZ => ?_))
    rw [mem_powerset] at hY hZ
    have hvZ : v ∉ Z := fun h => hvB (hZ h)
    rw [tw_union hAB hv hw hvw hedge hY hZ]
    by_cases hvY : v ∈ Y <;> by_cases hwZ : w ∈ Z <;>
      simp only [mem_union, hvY, hwZ, hvZ, and_self, and_true, true_and, and_false,
        false_and, or_true, true_or, or_false, false_or, ↓reduceIte] <;> ring

end Sums

/-! ### `lem:cc-gibbs`: the subtree recursion with a logarithmic potential -/

section Gibbs

open MaxLeafFormal.Antinorm3 (D children mem_children D_eq not_mem_D_child D_disjoint D_edge
  self_mem_D card_D_child_lt D_root)
open MaxLeafFormal.CDS (par par_spec)

/-- The potential `Ψ_{S,v} = π₀ log g_{S,v}(0) + π₁ log g_{S,v}(1)`. -/
noncomputable def psi (F : SimpleGraph V) (ζ : ℝ) (S : Finset V) (v : V) : ℝ :=
  piw ζ * Real.log (g0 F ζ S v) + piv ζ * Real.log (g1 F ζ S v)

theorem psi_union {F : SimpleGraph V} {ζ : ℝ} (hζ : 0 < ζ) {A B : Finset V} {v w : V}
    (hAB : Disjoint A B) (hv : v ∈ A) (hw : w ∈ B) (hvw : F.Adj v w)
    (hedge : ∀ a ∈ A, ∀ b ∈ B, F.Adj a b → a = v ∧ b = w) :
    psi F ζ A v + psi F ζ B w + (Real.log (spr ζ) - piv ζ * Real.log ζ)
      ≤ psi F ζ (A ∪ B) v := by
  obtain ⟨h0, h1⟩ := g_union hAB hv hw hvw hedge
  have a0 := g0_pos F ζ hζ.le A v
  have a1 := g1_pos F ζ hζ A v hv
  have b0 := g0_pos F ζ hζ.le B w
  have b1 := g1_pos F ζ hζ B w hw
  have K := key_step hζ b0 b1
  unfold psi
  rw [h0, h1, Real.log_mul a0.ne' (add_pos b0 b1).ne',
    Real.log_mul a1.ne' (by linarith : (0:ℝ) < g0 F ζ B w + 2 * g1 F ζ B w).ne',
    mul_add, mul_add]
  linarith

theorem psi_D {F : SimpleGraph V} {ζ : ℝ} (hζ : 0 < ζ) (hF : F.IsTree) (r v : V) :
    ((D hF r v).card : ℝ) * Real.log (spr ζ) - (Real.log (spr ζ) - piv ζ * Real.log ζ)
      ≤ psi F ζ (D hF r v) v := by
  induction hn : (D hF r v).card using Nat.strong_induction_on generalizing v with
  | _ n ih =>
    subst hn
    have key : ∀ C ⊆ children hF r v,
        ((insert v (C.biUnion (D hF r))).card : ℝ) * Real.log (spr ζ)
            - (Real.log (spr ζ) - piv ζ * Real.log ζ)
          ≤ psi F ζ (insert v (C.biUnion (D hF r))) v := by
      intro C
      induction C using Finset.induction_on with
      | empty =>
        intro _
        simp only [biUnion_empty, insert_empty, card_singleton]
        unfold psi
        rw [g0_single, g1_single, Real.log_one]
        apply le_of_eq
        push_cast
        ring
      | insert w C hwC ihC =>
        intro hC
        have hw : w ∈ children hF r v := hC (mem_insert_self w C)
        have hCv : C ⊆ children hF r v := fun c hc => hC (mem_insert_of_mem hc)
        obtain ⟨hwr, hpw⟩ := (mem_children hF r).1 hw
        set A := insert v (C.biUnion (D hF r)) with hAdef
        have hAB : Disjoint A (D hF r w) := by
          rw [hAdef, disjoint_insert_left, disjoint_biUnion_left]
          refine ⟨not_mem_D_child hF r hw, fun c hc => D_disjoint hF r (hCv hc) hw ?_⟩
          rintro rfl; exact hwC hc
        have hU : insert v ((insert w C).biUnion (D hF r)) = A ∪ D hF r w := by
          rw [biUnion_insert, hAdef]
          ext u; simp only [mem_insert, mem_union]; tauto
        have hedge : ∀ a ∈ A, ∀ b ∈ D hF r w, F.Adj a b → a = v ∧ b = w := by
          intro a ha b hb hab
          obtain ⟨h1, h2⟩ := D_edge hF r hwr hb (fun h => disjoint_left.1 hAB ha h) hab
          exact ⟨h2.trans hpw, h1⟩
        have hvw : F.Adj v w := by rw [← hpw]; exact (par_spec hF r hwr).1.symm
        have hstep := psi_union hζ hAB (mem_insert_self v _) (self_mem_D hF r w) hvw hedge
        have h1 := ihC hCv
        have h2 := ih _ (card_D_child_lt hF r hw) w rfl
        rw [hU, card_union_of_disjoint hAB, Nat.cast_add, add_mul]
        linarith
    have := key (children hF r v) subset_rfl
    rwa [← D_eq] at this

end Gibbs

/-! ### `lem:cc-path`: the transfer recursion along a path -/

section Path

/-- The pair `(g_{P_m}(0), g_{P_m}(1))` of the path on `m + 1` vertices, tracked at its end. -/
noncomputable def tr (ζ : ℝ) : ℕ → ℝ × ℝ
  | 0 => (1, ζ)
  | m + 1 => ((tr ζ m).1 + (tr ζ m).2, ζ * ((tr ζ m).1 + 2 * (tr ζ m).2))

theorem path_g (n : ℕ) (ζ : ℝ) : ∀ m (hm : m < n + 1),
    g0 (pathGraph (n + 1)) ζ (univ.filter (fun i : Fin (n + 1) => i.val ≤ m)) ⟨m, hm⟩
        = (tr ζ m).1 ∧
    g1 (pathGraph (n + 1)) ζ (univ.filter (fun i : Fin (n + 1) => i.val ≤ m)) ⟨m, hm⟩
        = (tr ζ m).2 := by
  intro m
  induction m with
  | zero =>
    intro hm
    have hS : (univ.filter (fun i : Fin (n + 1) => i.val ≤ 0)) = {⟨0, hm⟩} := by
      ext i
      simp only [mem_filter, mem_univ, true_and, mem_singleton, Fin.ext_iff]
      omega
    rw [hS, g0_single, g1_single]
    simp [tr]
  | succ m ih =>
    intro hm
    obtain ⟨ih0, ih1⟩ := ih (by omega)
    have hS : univ.filter (fun i : Fin (n + 1) => i.val ≤ m + 1)
        = {(⟨m + 1, hm⟩ : Fin (n + 1))} ∪ univ.filter (fun i : Fin (n + 1) => i.val ≤ m) := by
      ext i
      simp only [mem_filter, mem_univ, true_and, mem_union, mem_singleton, Fin.ext_iff]
      omega
    have hAB : Disjoint ({(⟨m + 1, hm⟩ : Fin (n + 1))} : Finset (Fin (n + 1)))
        (univ.filter (fun i : Fin (n + 1) => i.val ≤ m)) := by
      simp
    have hvw : (pathGraph (n + 1)).Adj (⟨m + 1, hm⟩ : Fin (n + 1)) ⟨m, by omega⟩ :=
      pathGraph_adj.2 (Or.inr rfl)
    have hw : (⟨m, by omega⟩ : Fin (n + 1)) ∈ univ.filter (fun i : Fin (n + 1) => i.val ≤ m) :=
      mem_filter.2 ⟨mem_univ _, le_rfl⟩
    have hedge : ∀ a ∈ ({(⟨m + 1, hm⟩ : Fin (n + 1))} : Finset (Fin (n + 1))),
        ∀ b ∈ univ.filter (fun i : Fin (n + 1) => i.val ≤ m),
        (pathGraph (n + 1)).Adj a b → a = ⟨m + 1, hm⟩ ∧ b = ⟨m, by omega⟩ := by
      intro a ha b hb hab
      rw [mem_singleton] at ha
      subst ha
      have hb' := (mem_filter.1 hb).2
      rw [pathGraph_adj] at hab
      refine ⟨rfl, Fin.ext ?_⟩
      dsimp only at hab ⊢
      omega
    obtain ⟨e0, e1⟩ := g_union hAB (mem_singleton_self _) hw hvw hedge
    rw [hS, e0, e1, g0_single, g1_single, ih0, ih1]
    simp [tr]

theorem path_Z (n : ℕ) (ζ : ℝ) :
    Zpart (pathGraph (n + 1)) ζ = (tr ζ n).1 + (tr ζ n).2 := by
  rw [Zpart_eq_g _ ζ ⟨n, by omega⟩]
  have hU : (univ : Finset (Fin (n + 1))) = univ.filter (fun i : Fin (n + 1) => i.val ≤ n) :=
    (filter_true_of_mem (fun i _ => Fin.is_le i)).symm
  obtain ⟨h0, h1⟩ := path_g n ζ n (by omega)
  rw [hU, h0, h1]

/-- The gap `(1 + ζ) λ^m - 𝒵_{P_{m+1}}`. -/
noncomputable def Ep (ζ : ℝ) (m : ℕ) : ℝ := (1 + ζ) * spr ζ ^ m - ((tr ζ m).1 + (tr ζ m).2)

theorem Ep_one_nonneg {ζ : ℝ} (hζ : 0 ≤ ζ) : 0 ≤ Ep ζ 1 := by
  have hR := Real.sq_sqrt (show (0:ℝ) ≤ 1 + 4 * ζ ^ 2 by positivity)
  have hR0 := Real.sqrt_nonneg (1 + 4 * ζ ^ 2)
  have hX0 : 0 ≤ (1 + ζ) * Real.sqrt (1 + 4 * ζ ^ 2) := mul_nonneg (by linarith) hR0
  have hB0 : 0 ≤ 1 + ζ + 2 * ζ ^ 2 := by positivity
  have key : (1 + ζ + 2 * ζ ^ 2) ^ 2 ≤ ((1 + ζ) * Real.sqrt (1 + 4 * ζ ^ 2)) ^ 2 := by
    rw [mul_pow, hR]
    nlinarith [pow_nonneg hζ 3]
  have hle : 1 + ζ + 2 * ζ ^ 2 ≤ (1 + ζ) * Real.sqrt (1 + 4 * ζ ^ 2) := by
    nlinarith [key, hX0, hB0]
  simp only [Ep, tr, spr, pow_one]
  nlinarith [hle]

theorem tr_bound {ζ : ℝ} (hζ : 0 ≤ ζ) (n : ℕ) :
    (tr ζ n).1 + (tr ζ n).2 ≤ (1 + ζ) * spr ζ ^ n := by
  have hl := spr_pos_of_nonneg hζ
  have hz : ζ / spr ζ = 1 + 2 * ζ - spr ζ := by
    rw [div_eq_iff hl.ne']
    linear_combination spr_root ζ
  have hsum : spr ζ + ζ / spr ζ = 1 + 2 * ζ := by rw [hz]; ring
  have hprod : spr ζ * (ζ / spr ζ) = ζ := by rw [hz]; linear_combination -(spr_root ζ)
  have hμ : 0 ≤ ζ / spr ζ := div_nonneg hζ hl.le
  have hrec : ∀ m, Ep ζ (m + 1 + 1) = (1 + 2 * ζ) * Ep ζ (m + 1) - ζ * Ep ζ m := by
    intro m
    simp only [Ep, tr]
    linear_combination (1 + ζ) * spr ζ ^ m * spr_root ζ
  have hind : ∀ m, 0 ≤ Ep ζ m ∧ ζ / spr ζ * Ep ζ m ≤ Ep ζ (m + 1) := by
    intro m
    induction m with
    | zero =>
      have h0 : Ep ζ 0 = 0 := by simp [Ep, tr]
      rw [h0, mul_zero]
      exact ⟨le_rfl, Ep_one_nonneg hζ⟩
    | succ m ih =>
      obtain ⟨h0, h1⟩ := ih
      have hid : Ep ζ (m + 1 + 1) - ζ / spr ζ * Ep ζ (m + 1)
          = spr ζ * (Ep ζ (m + 1) - ζ / spr ζ * Ep ζ m) := by
        rw [hrec m]
        linear_combination (-(Ep ζ (m + 1))) * hsum + Ep ζ m * hprod
      refine ⟨by nlinarith [mul_nonneg hμ h0], ?_⟩
      nlinarith [mul_nonneg hl.le (sub_nonneg.2 h1)]
  have := (hind n).1
  unfold Ep at this
  linarith

end Path

/-! ### The fixed statements -/

/-- The partition function is invariant under graph isomorphism. -/
theorem Zpart_iso {W : Type*} [Fintype W] [DecidableEq W]
    {F : SimpleGraph V} {G : SimpleGraph W} (e : F ≃g G) (ζ : ℝ) :
    Zpart F ζ = Zpart G ζ := by
  unfold Zpart
  refine Finset.sum_nbij' (fun X => X.map e.toEquiv.toEmbedding)
    (fun Y => Y.map e.toEquiv.symm.toEmbedding) ?_ ?_ ?_ ?_ ?_
  · intro X _
    exact Finset.mem_powerset.mpr (Finset.subset_univ _)
  · intro Y _
    exact Finset.mem_powerset.mpr (Finset.subset_univ _)
  · intro X _
    have hid : e.toEquiv.toEmbedding.trans e.toEquiv.symm.toEmbedding
        = Function.Embedding.refl V := by
      ext a
      exact e.toEquiv.symm_apply_apply a
    rw [Finset.map_map, hid, Finset.map_refl]
  · intro Y _
    have hid : e.toEquiv.symm.toEmbedding.trans e.toEquiv.toEmbedding
        = Function.Embedding.refl W := by
      ext a
      exact e.toEquiv.apply_symm_apply a
    rw [Finset.map_map, hid, Finset.map_refl]
  · intro X _
    rw [Finset.card_map, eIn_map_equiv e.toEquiv (fun a b => e.map_adj_iff.symm) X]

/-- `lem:cc-gibbs` (Gibbs bound, after Csikvári and Lin). `k = Fintype.card V ≥ 1` by `hF`. -/
theorem cc_gibbs (F : SimpleGraph V) (hF : F.IsTree) (ζ : ℝ) (hζ : 0 < ζ) :
    min 1 ζ * spr ζ ^ (Fintype.card V - 1) ≤ Zpart F ζ := by
  obtain ⟨r⟩ := hF.connected.nonempty
  have hk : 1 ≤ Fintype.card V := Fintype.card_pos_iff.2 ⟨r⟩
  have hl : 0 < spr ζ := spr_pos_of_nonneg hζ.le
  have hpsi := psi_D hζ hF r r
  rw [Antinorm3.D_root hF r, card_univ] at hpsi
  have p0 := g0_pos F ζ hζ.le univ r
  have p1 := g1_pos F ζ hζ univ r (mem_univ r)
  have hroot := root_step hζ p0 p1
  have hmin := min_step hζ
  have hm : 0 < min 1 ζ := lt_min one_pos hζ
  unfold psi at hpsi
  rw [Zpart_eq_g F ζ r, ← Real.log_le_log_iff (mul_pos hm (pow_pos hl _)) (add_pos p0 p1),
    Real.log_mul hm.ne' (pow_pos hl _).ne', Real.log_pow, Nat.cast_sub hk, Nat.cast_one,
    sub_mul, one_mul]
  linarith

/-- `lem:cc-path` (Paths). -/
theorem cc_path (k : ℕ) (hk : 1 ≤ k) (F : SimpleGraph V) (e : F ≃g SimpleGraph.pathGraph k)
    (ζ : ℝ) (hζ : 0 ≤ ζ) :
    Zpart F ζ ≤ (1 + ζ) * spr ζ ^ (k - 1) ∧ (1 + ζ) * spr ζ ^ (k - 1) ≤ 2 * spr ζ ^ k := by
  obtain ⟨n, rfl⟩ : ∃ n, k = n + 1 := ⟨k - 1, by omega⟩
  have hl := spr_pos_of_nonneg hζ
  have h1 := one_add_le_spr ζ
  refine ⟨?_, ?_⟩
  · rw [Zpart_iso e, path_Z, Nat.add_sub_cancel]
    exact tr_bound hζ n
  · rw [Nat.add_sub_cancel, pow_succ]
    nlinarith [mul_le_mul_of_nonneg_left h1 (pow_pos hl n).le, pow_pos hl n]

/-! ### Optional parts -/

/-- The remarks after `def:cc-Z`. -/
theorem spr_facts :
    spr 0 = 1 ∧ ContinuousOn spr (Set.Ici 0) ∧ StrictMonoOn spr (Set.Ici 0) ∧
    (∀ ζ : ℝ, 0 < ζ → 1 < spr ζ) ∧ (∀ ζ : ℝ, (1 + 2 * ζ) / 2 ≤ spr ζ) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · unfold spr
    norm_num
  · have hc : Continuous spr := by
      unfold spr
      fun_prop
    exact hc.continuousOn
  · intro a ha b _ hab
    simp only [Set.mem_Ici] at ha
    have h1 : Real.sqrt (1 + 4 * a ^ 2) ≤ Real.sqrt (1 + 4 * b ^ 2) :=
      Real.sqrt_le_sqrt (by nlinarith)
    unfold spr
    linarith
  · intro ζ hζ
    have := one_add_le_spr ζ
    linarith
  · intro ζ
    have h1 := Real.sqrt_nonneg (1 + 4 * ζ ^ 2)
    unfold spr
    linarith

/-- `M_ζ` of `def:cc-Z`. -/
noncomputable def Mz (ζ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ := !![1, ζ; 1, 2 * ζ]

/-- `M_ζ` has characteristic polynomial `X² - (1 + 2ζ)X + ζ`, which factors over `ℝ` as
`(X - spr ζ)(X - ζ / spr ζ)` with `0 ≤ ζ / spr ζ ≤ spr ζ`: both eigenvalues are real and
nonnegative, and `spr ζ` is the largest. Every complex root of the characteristic polynomial has
modulus at most `spr ζ`, so `spr ζ` is also the spectral radius (`def:cc-Z`). -/
theorem spr_eigen (ζ : ℝ) (hζ : 0 ≤ ζ) :
    (Mz ζ).charpoly = Polynomial.X ^ 2 - Polynomial.C (1 + 2 * ζ) * Polynomial.X + Polynomial.C ζ ∧
    (Mz ζ).charpoly =
      (Polynomial.X - Polynomial.C (spr ζ)) * (Polynomial.X - Polynomial.C (ζ / spr ζ)) ∧
    0 ≤ ζ / spr ζ ∧ ζ / spr ζ ≤ spr ζ ∧
    ∀ μ : ℂ, Polynomial.aeval μ (Mz ζ).charpoly = 0 → ‖μ‖ ≤ spr ζ := by
  have hpos : 0 < spr ζ := spr_pos_of_nonneg hζ
  have hl : spr ζ ≠ 0 := ne_of_gt hpos
  have hz : ζ / spr ζ = 1 + 2 * ζ - spr ζ := by
    rw [div_eq_iff hl]
    linear_combination spr_root ζ
  have hsum : spr ζ + ζ / spr ζ = 1 + 2 * ζ := by
    rw [hz]
    ring
  have hprod : spr ζ * (ζ / spr ζ) = ζ := by
    rw [hz]
    linear_combination -(spr_root ζ)
  have h1 : (Mz ζ).charpoly =
      Polynomial.X ^ 2 - Polynomial.C (1 + 2 * ζ) * Polynomial.X + Polynomial.C ζ := by
    rw [Matrix.charpoly, Matrix.det_fin_two]
    simp [Mz, map_ofNat Polynomial.C 2]
    ring
  have hfac : (Mz ζ).charpoly =
      (Polynomial.X - Polynomial.C (spr ζ)) * (Polynomial.X - Polynomial.C (ζ / spr ζ)) := by
    rw [h1]
    have e1 : Polynomial.C (1 + 2 * ζ) = Polynomial.C (spr ζ) + Polynomial.C (ζ / spr ζ) := by
      rw [← Polynomial.C_add, hsum]
    have e2 : Polynomial.C ζ = Polynomial.C (spr ζ) * Polynomial.C (ζ / spr ζ) := by
      rw [← Polynomial.C_mul, hprod]
    rw [e1, e2]
    ring
  have hm0 : 0 ≤ ζ / spr ζ := div_nonneg hζ hpos.le
  have hm1 : ζ / spr ζ ≤ spr ζ := by
    rw [div_le_iff₀ hpos]
    nlinarith [mul_le_mul (one_add_le_spr ζ) (one_add_le_spr ζ) (by linarith) hpos.le,
      sq_nonneg ζ]
  have key : ∀ r : ℝ, 0 ≤ r → ‖algebraMap ℝ ℂ r‖ = r := fun r hr => by
    simp [abs_of_nonneg hr]
  refine ⟨h1, hfac, hm0, hm1, ?_⟩
  intro μ hμ
  rw [hfac] at hμ
  simp only [map_mul, map_sub, Polynomial.aeval_X, Polynomial.aeval_C, mul_eq_zero,
    sub_eq_zero] at hμ
  rcases hμ with h | h
  · have := key _ hpos.le
    rw [← h] at this
    exact this.le
  · have := key _ hm0
    rw [← h] at this
    linarith

open Classical in
/-- `eIn F X = |E(F[X])|` for Mathlib's induced subgraph. -/
theorem eIn_eq_induce (F : SimpleGraph V) (X : Finset V) :
    eIn F X = (F.induce (X : Set V)).edgeFinset.card := by
  unfold eIn
  symm
  refine Finset.card_bij (fun b _ => Sym2.map Subtype.val b) ?_ ?_ ?_
  · intro b
    refine Sym2.inductionOn b (fun x y => ?_)
    intro hb
    have h1 : (F.induce (X : Set V)).Adj x y :=
      (SimpleGraph.mem_edgeSet _).mp (SimpleGraph.mem_edgeFinset.mp hb)
    have hadj : F.Adj x.1 y.1 := h1
    simp only [Finset.mem_filter, SimpleGraph.mem_edgeFinset, sym2_pair_map,
      SimpleGraph.mem_edgeSet]
    refine ⟨hadj, fun v hv => ?_⟩
    rcases Sym2.mem_iff.mp hv with rfl | rfl
    · exact Finset.mem_coe.mp x.2
    · exact Finset.mem_coe.mp y.2
  · intro a₁ _ a₂ _ h
    exact Sym2.map.injective Subtype.val_injective h
  · intro a
    refine Sym2.inductionOn a (fun x y => ?_)
    intro ha
    have hF := Finset.mem_filter.mp ha
    have hx : x ∈ X := hF.2 x (Sym2.mem_mk_left x y)
    have hy : y ∈ X := hF.2 y (Sym2.mem_mk_right x y)
    have hadj : F.Adj x y :=
      (SimpleGraph.mem_edgeSet _).mp (SimpleGraph.mem_edgeFinset.mp hF.1)
    refine ⟨s(⟨x, hx⟩, ⟨y, hy⟩), ?_, ?_⟩
    · rw [SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet]
      exact hadj
    · rfl

/-- Paths minimize the partition function among trees with the same number of vertices, up to
the factor `min 1 ζ / (1 + ζ)` (`lem:cc-gibbs` and `lem:cc-path` combined). -/
theorem cc_path_min (F : SimpleGraph V) (hF : F.IsTree) (ζ : ℝ) (hζ : 0 < ζ) :
    min 1 ζ / (1 + ζ) * Zpart (SimpleGraph.pathGraph (Fintype.card V)) ζ ≤ Zpart F ζ := by
  obtain ⟨r⟩ := hF.connected.nonempty
  have hk : 1 ≤ Fintype.card V := Fintype.card_pos_iff.2 ⟨r⟩
  obtain ⟨hp, -⟩ := cc_path (Fintype.card V) hk (SimpleGraph.pathGraph (Fintype.card V))
    SimpleGraph.Iso.refl ζ hζ.le
  have hg := cc_gibbs F hF ζ hζ
  have hm : 0 ≤ min 1 ζ := le_min zero_le_one hζ.le
  have h1 : (0 : ℝ) < 1 + ζ := by linarith
  calc min 1 ζ / (1 + ζ) * Zpart (SimpleGraph.pathGraph (Fintype.card V)) ζ
      ≤ min 1 ζ / (1 + ζ) * ((1 + ζ) * spr ζ ^ (Fintype.card V - 1)) :=
        mul_le_mul_of_nonneg_left hp (div_nonneg hm h1.le)
    _ = min 1 ζ * spr ζ ^ (Fintype.card V - 1) := by field_simp
    _ ≤ Zpart F ζ := hg

/-- Sanity check of the definitions: computed directly from `eIn` and
`Zpart`, without the transfer recursion. -/
theorem Zpart_pathGraph_two (ζ : ℝ) :
    Zpart (SimpleGraph.pathGraph 2) ζ = 1 + 2 * ζ + 2 * ζ ^ 2 := by
  have hpow : (univ : Finset (Fin 2)).powerset = {∅, {0}, {1}, {0, 1}} := by decide
  have h1 : (∅ : Finset (Fin 2)) ∉ ({{0}, {1}, {0, 1}} : Finset (Finset (Fin 2))) := by
    decide
  have h2 : ({0} : Finset (Fin 2)) ∉ ({{1}, {0, 1}} : Finset (Finset (Fin 2))) := by
    decide
  have h3 : ({1} : Finset (Fin 2)) ∉ ({{0, 1}} : Finset (Finset (Fin 2))) := by decide
  have c01 : ({0, 1} : Finset (Fin 2)).card = 2 := by decide
  have v0 : eIn (SimpleGraph.pathGraph 2) ∅ = 0 := by
    rw [eIn_pg2]; decide
  have v1 : eIn (SimpleGraph.pathGraph 2) {0} = 0 := by
    rw [eIn_pg2]; decide
  have v2 : eIn (SimpleGraph.pathGraph 2) {1} = 0 := by
    rw [eIn_pg2]; decide
  have v3 : eIn (SimpleGraph.pathGraph 2) {0, 1} = 1 := by
    rw [eIn_pg2]; decide
  unfold Zpart
  rw [hpow, Finset.sum_insert h1, Finset.sum_insert h2, Finset.sum_insert h3,
    Finset.sum_singleton]
  simp only [v0, v1, v2, v3, Finset.card_empty, Finset.card_singleton, c01]
  ring

end MaxLeafFormal.CCGibbs