MaxLeafFormal.LobsterGraph

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

Statements of the paper formalised here: Lemma 7.3, Proposition 7.9.

import MaxLeafFormal.Lobster
import MaxLeafFormal.CDS
import MaxLeafFormal.MLS
import MaxLeafFormal.RateAssembly

/-!
# Uniform lobsters: the graph side of `prop:rst-caterpillar`(c)

The proof of `prop:rst-caterpillar`(c): the identity `W_{S*}(y) = fᵀ M_y^{L-1} u_y` and the step
from the matrix inequalities of `MaxLeafFormal.Lobster` to the moments `μ_t(S*)`.
-/

namespace MaxLeafFormal.LobsterGraph

open Finset Matrix MaxLeafFormal.CDS MaxLeafFormal.MLS MaxLeafFormal.RateAssembly

/-! ### General results -/

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

/-- `lem:rst-E`, equality clause:
if `F = G[S]` and every vertex outside `S` has exactly one neighbour in `S` (its owner),
then `|Tm(J_X)| = Π_{F,ν}(X)` for every `X ⊆ S`. -/
theorem tree_reduction_eq (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V)
    (F : SimpleGraph S) (hFG : F = G.induce (S : Set V))
    (o : {v // v ∉ S} → S) (ho : ∀ v, G.Adj v.1 (o v).1)
    (huniq : ∀ (v : {v // v ∉ S}) (w : S), G.Adj v.1 w.1 → w = o v) :
    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 := by
  classical
  intro ν X
  have hadjF : ∀ a b : S, F.Adj a b ↔ G.Adj a.1 b.1 := by
    subst hFG; intro a b; exact Iff.rfl
  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]
  have memXv' : ∀ w : V, w ∈ Xv → ∃ h : w ∈ S, (⟨w, h⟩ : S) ∈ X := by
    intro w hw
    rw [hXv, mem_map] at hw
    obtain ⟨v, hv, rfl⟩ := hw
    exact ⟨v.2, hv⟩
  -- (1) outside vertices not dominated by `X` are exactly those whose owner is 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 hBeq : B = univ.filter (fun w => o w ∉ X) := by
    ext w
    simp only [B, mem_filter, mem_univ, true_and]
    constructor
    · intro hw hoX
      apply hw
      rw [mem_closedNbhd]
      exact Or.inr ⟨(o w).1, (memXv _).2 hoX, (ho w).symm⟩
    · intro hoX hw
      rw [mem_closedNbhd] at hw
      rcases hw with hw | ⟨x, hx, hxw⟩
      · obtain ⟨h, _⟩ := memXv' _ hw
        exact w.2 h
      · obtain ⟨h, hx'⟩ := memXv' _ hx
        have hxo := huniq w ⟨x, h⟩ hxw.symm
        rw [hxo] at hx'
        exact hoX hx'
  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, hBeq, hsumν]
  -- (2) solution vertices not dominated by `X` are exactly those 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]
    congr 1
    ext v
    simp only [C, mem_filter, mem_univ, true_and]
    constructor
    · intro 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]
      exact Or.inr ⟨u.1, (memXv u).2 huX, ((hadjF v u).1 hvu).symm⟩
    · rintro ⟨hvX, hnb⟩ hv
      rw [mem_closedNbhd] at hv
      rcases hv with hv | ⟨x, hx, hxv⟩
      · exact hvX ((memXv v).1 hv)
      · obtain ⟨h, hx'⟩ := memXv' _ hx
        exact hnb ⟨x, h⟩ ((hadjF v ⟨x, h⟩).2 hxv.symm) hx'
  -- (3) components: `F[X] ≅ G[X]`
  have h3 : CDS.comp G Xv = Nat.card (F.induce (X : Set S)).ConnectedComponent := by
    unfold CDS.comp
    let e : F.induce (X : Set S) ≃g G.induce (Xv : Set V) :=
      { toFun := fun x => ⟨x.1.1, (memXv x.1).2 x.2⟩
        invFun := fun y => ⟨⟨y.1, (memXv' y.1 y.2).1⟩, (memXv' y.1 y.2).2⟩
        left_inv := fun _ => rfl
        right_inv := fun _ => rfl
        map_rel_iff' := fun {a b} => (hadjF a.1 b.1).symm }
    exact (Nat.card_congr (SimpleGraph.Iso.connectedComponentEquiv e)).symm
  -- 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

/-- One term of `W_S`: `μ_t(S) y^t ≤ W_S(y)` for `y ≥ 0` (proof of `lem:fw-gf`). -/
theorem mu_mul_pow_le_W (g : Finset V → ℕ → ℝ) (S : Finset V) (k t : ℕ) (y : ℝ) (hy : 0 ≤ y) :
    mu g S k t * y ^ t ≤ W g S k y := by
  unfold MLS.mu MLS.W
  rw [sum_mul]
  calc ∑ X ∈ S.powersetCard t, (2:ℝ) ^ (-(g X (k - t))) * y ^ t
      = ∑ X ∈ S.powersetCard t, y ^ X.card * (2:ℝ) ^ (-(g X (k - X.card))) := by
        refine sum_congr rfl fun X hX => ?_
        rw [(mem_powersetCard.1 hX).2, mul_comm]
    _ ≤ ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(g X (k - X.card))) := by
        apply sum_le_sum_of_subset_of_nonneg
        · intro X hX
          exact mem_powerset.2 (mem_powersetCard.1 hX).1
        · intro X _ _
          exact mul_nonneg (pow_nonneg hy _) (Real.rpow_nonneg (by norm_num) _)

/-- A graph with a parent map `p` towards `r` that strictly lowers a rank, and whose edges are
exactly the parent edges, is a tree. -/
theorem isTree_of_parent (G : SimpleGraph V) (r : V) (p : V → V) (h : V → ℕ)
    (hadj : ∀ v w, G.Adj v w ↔ (v ≠ r ∧ p v = w) ∨ (w ≠ r ∧ p w = v))
    (hh : ∀ v, v ≠ r → h (p v) < h v) : G.IsTree := by
  have hreach : ∀ n, ∀ v, h v = n → G.Reachable v r := by
    intro n
    induction n using Nat.strong_induction_on with
    | _ n ih =>
      intro v hv
      by_cases hvr : v = r
      · subst hvr; exact SimpleGraph.Reachable.refl _
      · have hA : G.Adj v (p v) := (hadj v (p v)).2 (Or.inl ⟨hvr, rfl⟩)
        exact hA.reachable.trans (ih (h (p v)) (by rw [← hv]; exact hh v hvr) (p v) rfl)
  have hconn : G.Connected := by
    have : Nonempty V := ⟨r⟩
    exact SimpleGraph.Connected.mk fun u v => (hreach _ u rfl).trans (hreach _ v rfl).symm
  rw [SimpleGraph.isTree_iff_connected_and_card]
  refine ⟨hconn, ?_⟩
  have hcard : Nat.card {v : V // v ≠ r} = Nat.card G.edgeSet := by
    apply Nat.card_eq_of_bijective (fun v : {v : V // v ≠ r} =>
      (⟨s(v.1, p v.1), (hadj v.1 (p v.1)).2 (Or.inl ⟨v.2, rfl⟩)⟩ : G.edgeSet))
    constructor
    · rintro ⟨a, ha⟩ ⟨b, hb⟩ hab
      have hab' : s(a, p a) = s(b, p b) := congrArg Subtype.val hab
      rcases Sym2.eq_iff.1 hab' with ⟨h1, _⟩ | ⟨h1, h2⟩
      · exact Subtype.ext h1
      · exfalso
        have e1 := hh a ha
        have e2 := hh b hb
        rw [h2] at e1
        rw [← h1] at e2
        omega
    · rintro ⟨e, he⟩
      induction e using Sym2.ind with
      | h a b =>
        have he' := he
        rw [SimpleGraph.mem_edgeSet, hadj] at he'
        rcases he' with ⟨ha, hab⟩ | ⟨hb, hba⟩
        · exact ⟨⟨a, ha⟩, Subtype.ext (by simp only [hab])⟩
        · refine ⟨⟨b, hb⟩, Subtype.ext ?_⟩
          show s(b, p b) = s(a, b)
          rw [hba]
          exact Sym2.eq_swap
  rw [← hcard, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_subtype,
    filter_ne', card_erase_of_mem (mem_univ _), card_univ]
  have : 0 < Fintype.card V := Fintype.card_pos_iff.2 ⟨r⟩
  omega

/-- Under the hypotheses of `isTree_of_parent`, the rooting parent `CDS.par` is `p`. -/
theorem par_eq_of_parent {G : SimpleGraph V} (hG : G.IsTree) (r : V) (p : V → V) (h : V → ℕ)
    (hadj : ∀ v w, G.Adj v w ↔ (v ≠ r ∧ p v = w) ∨ (w ≠ r ∧ p w = v))
    (hh : ∀ v, v ≠ r → h (p v) < h v) : ∀ v, v ≠ r → CDS.par hG r v = p v := by
  have key : ∀ n, ∀ v, h v = n → v ≠ r → CDS.par hG r v = p v := by
    intro n
    induction n using Nat.strong_induction_on with
    | _ n ih =>
      intro v hn hv
      have hA : G.Adj v (p v) := (hadj v (p v)).2 (Or.inl ⟨hv, rfl⟩)
      rcases (CDS.adj_iff_par hG r).1 hA with ⟨_, h1⟩ | ⟨h1, h2⟩
      · exact h1
      · exfalso
        have h3 := ih (h (p v)) (by rw [← hn]; exact hh v hv) (p v) rfl h1
        rw [h3] at h2
        have e1 := hh (p v) h1
        rw [h2] at e1
        have e2 := hh v hv
        omega
  exact fun v hv => key _ v rfl hv

end General

/-- `C(n,t) y^t ≥ (1+y)^n / (n+1)` at `y = t/(n-t)`, for `t < n` (proof of `lem:fw-gf`,
as used in the proof of `prop:rst-caterpillar`). -/
theorem pow_le_choose_mul (n t : ℕ) (ht : t < n) :
    (1 + (t : ℝ) / ((n : ℝ) - t)) ^ n
      ≤ ((n : ℝ) + 1) * (n.choose t : ℝ) * ((t : ℝ) / ((n : ℝ) - t)) ^ t := by
  have htn : (t : ℝ) < n := by exact_mod_cast ht
  have hnt : (0 : ℝ) < (n : ℝ) - t := by linarith
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  generalize hy : (t : ℝ) / ((n : ℝ) - t) = y
  have hy0 : 0 ≤ y := hy ▸ div_nonneg (Nat.cast_nonneg _) hnt.le
  have hyb : y * ((n : ℝ) - t) = t := by rw [← hy]; exact div_mul_cancel₀ _ hnt.ne'
  -- the ratio of consecutive terms
  have hrat : ∀ s, s < n → (n.choose (s + 1) : ℝ) * y ^ (s + 1) * (((s : ℝ) + 1) * ((n : ℝ) - t))
      = (n.choose s : ℝ) * y ^ s * (((n : ℝ) - s) * t) := by
    intro s hs
    have h' : (n.choose (s + 1) : ℝ) * ((s : ℝ) + 1) = (n.choose s : ℝ) * ((n : ℝ) - s) := by
      have h2 : ((n.choose (s + 1) * (s + 1) : ℕ) : ℝ) = ((n.choose s * (n - s) : ℕ) : ℝ) := by
        rw [Nat.choose_succ_right_eq]
      push_cast [Nat.cast_sub hs.le] at h2
      exact h2
    calc (n.choose (s + 1) : ℝ) * y ^ (s + 1) * (((s : ℝ) + 1) * ((n : ℝ) - t))
        = ((n.choose (s + 1) : ℝ) * ((s : ℝ) + 1)) * y ^ s * (y * ((n : ℝ) - t)) := by ring
      _ = (n.choose s : ℝ) * y ^ s * (((n : ℝ) - s) * t) := by rw [h', hyb]; ring
  have hup : ∀ s, s < t → (n.choose s : ℝ) * y ^ s ≤ (n.choose (s + 1) : ℝ) * y ^ (s + 1) := by
    intro s hs
    have hs' : (s : ℝ) + 1 ≤ t := by exact_mod_cast hs
    have hpos : (0 : ℝ) < ((s : ℝ) + 1) * ((n : ℝ) - t) := mul_pos (by positivity) hnt
    have hst : ((s : ℝ) + 1) * ((n : ℝ) - t) ≤ ((n : ℝ) - s) * t := by
      nlinarith [mul_nonneg hn0 (by linarith : (0 : ℝ) ≤ t - s - 1)]
    have hf0 : 0 ≤ (n.choose s : ℝ) * y ^ s := mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hy0 _)
    refine le_of_mul_le_mul_right ?_ hpos
    rw [hrat s (by omega)]
    exact mul_le_mul_of_nonneg_left hst hf0
  have hdown : ∀ s, t ≤ s → s < n →
      (n.choose (s + 1) : ℝ) * y ^ (s + 1) ≤ (n.choose s : ℝ) * y ^ s := by
    intro s hs hsn
    have hs1 : (t : ℝ) ≤ s := by exact_mod_cast hs
    have hpos : (0 : ℝ) < ((s : ℝ) + 1) * ((n : ℝ) - t) := mul_pos (by positivity) hnt
    have hst : ((n : ℝ) - s) * t ≤ ((s : ℝ) + 1) * ((n : ℝ) - t) := by
      nlinarith [mul_nonneg hn0 (by linarith : (0 : ℝ) ≤ s - t)]
    have hf0 : 0 ≤ (n.choose s : ℝ) * y ^ s := mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hy0 _)
    refine le_of_mul_le_mul_right ?_ hpos
    rw [hrat s hsn]
    exact mul_le_mul_of_nonneg_left hst hf0
  have hle_up : ∀ d s, s + d = t → (n.choose s : ℝ) * y ^ s ≤ (n.choose t : ℝ) * y ^ t := by
    intro d
    induction d with
    | zero => intro s hs; rw [Nat.add_zero] at hs; subst hs; exact le_rfl
    | succ d ih => intro s hs; exact (hup s (by omega)).trans (ih (s + 1) (by omega))
  have hle_down : ∀ d, t + d ≤ n →
      (n.choose (t + d) : ℝ) * y ^ (t + d) ≤ (n.choose t : ℝ) * y ^ t := by
    intro d
    induction d with
    | zero => intro _; simp only [Nat.add_zero, le_refl]
    | succ d ih =>
      intro hd
      exact (hdown (t + d) (by omega) (by omega)).trans (ih (by omega))
  have hbound : ∀ s, s ≤ n → (n.choose s : ℝ) * y ^ s ≤ (n.choose t : ℝ) * y ^ t := by
    intro s hs
    rcases Nat.lt_or_ge s t with h | h
    · exact hle_up (t - s) s (by omega)
    · have := hle_down (s - t) (by omega)
      rwa [show t + (s - t) = s by omega] at this
  have hsum : (1 + y) ^ n = ∑ s ∈ range (n + 1), (n.choose s : ℝ) * y ^ s := by
    rw [add_comm (1 : ℝ) y, add_pow]
    refine sum_congr rfl fun s _ => ?_
    rw [one_pow, mul_one, mul_comm]
  rw [hsum]
  calc ∑ s ∈ range (n + 1), (n.choose s : ℝ) * y ^ s
      ≤ ∑ _s ∈ range (n + 1), (n.choose t : ℝ) * y ^ t :=
        sum_le_sum fun s hs => hbound s (Nat.lt_succ_iff.1 (mem_range.1 hs))
    _ = ((n : ℝ) + 1) * (n.choose t : ℝ) * y ^ t := by
        rw [sum_const, card_range, nsmul_eq_mul]; push_cast; ring

/-! ### The uniform (2,2)-lobster -/

/-- Edges inside one block: spine vertex 0, legs 1 and 2, claws 3, 4 (of leg 1), 5, 6 (of leg 2). -/
def lobEdge (a b : Fin 7) : Prop :=
  (a = 0 ∧ (b = 1 ∨ b = 2)) ∨ (a = 1 ∧ (b = 3 ∨ b = 4)) ∨ (a = 2 ∧ (b = 5 ∨ b = 6))

instance instDecidableRelLobEdge : DecidableRel lobEdge := fun a b => by
  unfold lobEdge; infer_instance

/-- Block edges, and the spine edges `x_i x_{i+1}` of `Λ_L`. -/
def lobRel (L : ℕ) (p q : Fin L × Fin 7) : Prop :=
  (p.1 = q.1 ∧ lobEdge p.2 q.2) ∨ (p.2 = 0 ∧ q.2 = 0 ∧ p.1.val + 1 = q.1.val)

instance instDecidableRelLobRel (L : ℕ) : DecidableRel (lobRel L) := fun p q => by
  unfold lobRel; infer_instance

/-- `Λ_L`. -/
def Lam (L : ℕ) : SimpleGraph (Fin L × Fin 7) := SimpleGraph.fromRel (lobRel L)

instance instDecidableRelLamAdj (L : ℕ) : DecidableRel (Lam L).Adj := fun p q =>
  decidable_of_iff (p ≠ q ∧ (lobRel L p q ∨ lobRel L q p)) (SimpleGraph.fromRel_adj _ p q).symm

/-- `S*`: the spine vertices and the legs. -/
def Sstar (L : ℕ) : Finset (Fin L × Fin 7) := univ ×ˢ ({0, 1, 2} : Finset (Fin 7))

/-- `F = Λ_L[S*]`, the caterpillar. -/
def lobF (L : ℕ) : SimpleGraph (Sstar L) := (Lam L).induce (Sstar L : Set (Fin L × Fin 7))

/-- `ν`: 2 at the legs, 0 on the spine. -/
def lobNu (L : ℕ) (v : Sstar L) : ℕ := if v.1.2 = 0 then 0 else 2

/-- `n = 7L`. -/
theorem card_Lam (L : ℕ) : Fintype.card (Fin L × Fin 7) = 7 * L := by
  rw [Fintype.card_prod, Fintype.card_fin, Fintype.card_fin, mul_comm]

/-- `|S*| = 3L`. -/
theorem card_Sstar (L : ℕ) : (Sstar L).card = 3 * L := by
  have h3 : ({0, 1, 2} : Finset (Fin 7)).card = 3 := by decide
  unfold Sstar
  rw [card_product, card_univ, Fintype.card_fin, h3, mul_comm]

/-! #### Helpers: coordinates -/

theorem mem_Sstar {L : ℕ} (p : Fin L × Fin 7) : p ∈ Sstar L ↔ p.2.val ≤ 2 := by
  have h : ∀ a : Fin 7, (a = 0 ∨ a = 1 ∨ a = 2 ↔ a.val ≤ 2) := by decide
  simp only [Sstar, mem_product, mem_univ, true_and, mem_insert, mem_singleton]
  exact h p.2

theorem sstar_eq_iff {L : ℕ} (v w : Sstar L) :
    v = w ↔ v.1.1.val = w.1.1.val ∧ v.1.2.val = w.1.2.val := by
  rw [Subtype.ext_iff, Prod.ext_iff, Fin.ext_iff, Fin.ext_iff]

theorem out_eq_iff {L : ℕ} (v w : {v // v ∉ Sstar L}) :
    v = w ↔ v.1.1.val = w.1.1.val ∧ v.1.2.val = w.1.2.val := by
  rw [Subtype.ext_iff, Prod.ext_iff, Fin.ext_iff, Fin.ext_iff]

/-- The vertex `(i, a)` of `S*` (block `i`, role `a ≤ 2`). -/
def lobV (L i a : ℕ) (hi : i < L) (ha : a ≤ 2) : Sstar L :=
  ⟨(⟨i, hi⟩, ⟨a, by omega⟩), (mem_Sstar _).2 ha⟩

@[simp] theorem lobV_blk (L i a : ℕ) (hi : i < L) (ha : a ≤ 2) : (lobV L i a hi ha).1.1.val = i :=
  rfl

@[simp] theorem lobV_role (L i a : ℕ) (hi : i < L) (ha : a ≤ 2) :
    (lobV L i a hi ha).1.2.val = a := rfl

/-- The claw `(i, c)` (block `i`, role `3 ≤ c ≤ 6`), outside `S*`. -/
def lobO (L i c : ℕ) (hi : i < L) (hc : 3 ≤ c) (hc' : c < 7) : {v // v ∉ Sstar L} :=
  ⟨(⟨i, hi⟩, ⟨c, hc'⟩), fun h => absurd ((mem_Sstar _).1 h) (by show ¬ c ≤ 2; omega)⟩

@[simp] theorem lobO_blk (L i c : ℕ) (hi : i < L) (hc : 3 ≤ c) (hc' : c < 7) :
    (lobO L i c hi hc hc').1.1.val = i := rfl

@[simp] theorem lobO_role (L i c : ℕ) (hi : i < L) (hc : 3 ≤ c) (hc' : c < 7) :
    (lobO L i c hi hc hc').1.2.val = c := rfl

theorem lobNu_eq (L : ℕ) (v : Sstar L) : lobNu L v = if v.1.2.val = 0 then 0 else 2 := by
  unfold lobNu
  by_cases h : v.1.2.val = 0 <;> simp [h, Fin.ext_iff]

/-- Adjacency in `Λ_L`, in coordinates. -/
theorem lam_adj_iff (L : ℕ) (p q : Fin L × Fin 7) : (Lam L).Adj p q ↔
    (p.1.val = q.1.val ∧
      ((p.2.val = 0 ∧ (q.2.val = 1 ∨ q.2.val = 2)) ∨ (p.2.val = 1 ∧ (q.2.val = 3 ∨ q.2.val = 4)) ∨
       (p.2.val = 2 ∧ (q.2.val = 5 ∨ q.2.val = 6)) ∨ (q.2.val = 0 ∧ (p.2.val = 1 ∨ p.2.val = 2)) ∨
       (q.2.val = 1 ∧ (p.2.val = 3 ∨ p.2.val = 4)) ∨ (q.2.val = 2 ∧ (p.2.val = 5 ∨ p.2.val = 6)))) ∨
    (p.2.val = 0 ∧ q.2.val = 0 ∧ (p.1.val + 1 = q.1.val ∨ q.1.val + 1 = p.1.val)) := by
  have hE : ∀ a b : Fin 7, lobEdge a b ↔ ((a.val = 0 ∧ (b.val = 1 ∨ b.val = 2)) ∨
      (a.val = 1 ∧ (b.val = 3 ∨ b.val = 4)) ∨ (a.val = 2 ∧ (b.val = 5 ∨ b.val = 6))) := by
    unfold lobEdge; decide
  have h0 : ∀ a : Fin 7, a = 0 ↔ a.val = 0 := by decide
  show (SimpleGraph.fromRel (lobRel L)).Adj p q ↔ _
  rw [SimpleGraph.fromRel_adj]
  simp only [lobRel, hE, h0, ne_eq, Prod.ext_iff, Fin.ext_iff]
  omega

theorem lobF_adj (L : ℕ) (v w : Sstar L) : (lobF L).Adj v w ↔ (Lam L).Adj v.1 w.1 := Iff.rfl

/-- Adjacency in `F = Λ_L[S*]`, in coordinates. -/
theorem lobF_adj_val (L : ℕ) (v w : Sstar L) : (lobF L).Adj v w ↔
    (v.1.1.val = w.1.1.val ∧ ((v.1.2.val = 0 ∧ w.1.2.val ≠ 0) ∨ (w.1.2.val = 0 ∧ v.1.2.val ≠ 0))) ∨
    (v.1.2.val = 0 ∧ w.1.2.val = 0 ∧ (v.1.1.val + 1 = w.1.1.val ∨ w.1.1.val + 1 = v.1.1.val)) := by
  have hv := (mem_Sstar v.1).1 v.2
  have hw := (mem_Sstar w.1).1 w.2
  rw [lobF_adj, lam_adj_iff]
  omega

/-! #### Helpers: the rooting of `F` at `x_L = (L-1, 0)` -/

/-- The root `x_L`. -/
def lobRoot (L : ℕ) (hL : 1 ≤ L) : Sstar L := lobV L (L - 1) 0 (by omega) (Nat.zero_le _)

/-- The parent towards the root: the next spine vertex, or the spine vertex of a leg. -/
def lobP (L : ℕ) (v : Sstar L) : Sstar L :=
  if h : v.1.2.val = 0 ∧ v.1.1.val + 1 < L then lobV L (v.1.1.val + 1) 0 h.2 (Nat.zero_le _)
  else lobV L v.1.1.val 0 v.1.1.isLt (Nat.zero_le _)

theorem lobP_role (L : ℕ) (v : Sstar L) : (lobP L v).1.2.val = 0 := by
  unfold lobP; split_ifs <;> rfl

theorem lobP_blk (L : ℕ) (v : Sstar L) :
    (v.1.2.val = 0 ∧ v.1.1.val + 1 < L ∧ (lobP L v).1.1.val = v.1.1.val + 1) ∨
    (¬ (v.1.2.val = 0 ∧ v.1.1.val + 1 < L) ∧ (lobP L v).1.1.val = v.1.1.val) := by
  unfold lobP
  split_ifs with h
  · exact Or.inl ⟨h.1, h.2, rfl⟩
  · exact Or.inr ⟨h, rfl⟩

/-- A rank that `lobP` lowers. -/
def lobRank (L : ℕ) (v : Sstar L) : ℕ := 2 * (L - v.1.1.val) + (if v.1.2.val = 0 then 0 else 1)

theorem lobRank_lt (L : ℕ) (hL : 1 ≤ L) (v : Sstar L) (hv : v ≠ lobRoot L hL) :
    lobRank L (lobP L v) < lobRank L v := by
  rw [ne_eq, sstar_eq_iff] at hv
  simp only [lobRoot, lobV_blk, lobV_role] at hv
  have h1 := lobP_blk L v
  have h2 := lobP_role L v
  have h3 := v.1.1.isLt
  unfold lobRank
  split_ifs <;> omega

theorem lobF_adj_iff (L : ℕ) (hL : 1 ≤ L) (v w : Sstar L) :
    (lobF L).Adj v w ↔ (v ≠ lobRoot L hL ∧ lobP L v = w) ∨ (w ≠ lobRoot L hL ∧ lobP L w = v) := by
  have hv := (mem_Sstar v.1).1 v.2
  have hw := (mem_Sstar w.1).1 w.2
  have hv' := v.1.1.isLt
  have hw' := w.1.1.isLt
  have pv := lobP_blk L v
  have pw := lobP_blk L w
  have rv := lobP_role L v
  have rw' := lobP_role L w
  rw [lobF_adj_val]
  simp only [ne_eq, sstar_eq_iff, lobRoot, lobV_blk, lobV_role]
  omega

/-- `G[S*]` is a tree. -/
theorem lobF_isTree (L : ℕ) (hL : 1 ≤ L) : (lobF L).IsTree :=
  isTree_of_parent (lobF L) (lobRoot L hL) (lobP L) (lobRank L) (lobF_adj_iff L hL)
    (lobRank_lt L hL)

theorem lob_par (L : ℕ) (hL : 1 ≤ L) (v : Sstar L) (hv : v ≠ lobRoot L hL) :
    CDS.par (lobF_isTree L hL) (lobRoot L hL) v = lobP L v :=
  par_eq_of_parent (lobF_isTree L hL) (lobRoot L hL) (lobP L) (lobRank L) (lobF_adj_iff L hL)
    (lobRank_lt L hL) v hv

/-! #### Helpers: the owner map (each claw is owned by its leg) -/

/-- The owner of a claw: its leg. -/
def lobOwner (L : ℕ) (v : {v // v ∉ Sstar L}) : Sstar L :=
  lobV L v.1.1.val (if v.1.2.val ≤ 4 then 1 else 2) v.1.1.isLt (by split_ifs <;> omega)

theorem lobOwner_blk (L : ℕ) (v : {v // v ∉ Sstar L}) : (lobOwner L v).1.1.val = v.1.1.val := rfl

theorem lobOwner_role (L : ℕ) (v : {v // v ∉ Sstar L}) :
    (lobOwner L v).1.2.val = if v.1.2.val ≤ 4 then 1 else 2 := rfl

theorem lobOwner_adj (L : ℕ) (v : {v // v ∉ Sstar L}) : (Lam L).Adj v.1 (lobOwner L v).1 := by
  have h1 : ¬ v.1.2.val ≤ 2 := fun h => v.2 ((mem_Sstar v.1).2 h)
  have h2 := v.1.2.isLt
  rw [lam_adj_iff, lobOwner_blk, lobOwner_role]
  split_ifs <;> omega

theorem lobOwner_uniq (L : ℕ) (v : {v // v ∉ Sstar L}) (w : Sstar L)
    (h : (Lam L).Adj v.1 w.1) : w = lobOwner L v := by
  have h1 : ¬ v.1.2.val ≤ 2 := fun h => v.2 ((mem_Sstar v.1).2 h)
  have h2 := v.1.2.isLt
  have h3 := (mem_Sstar w.1).1 w.2
  rw [lam_adj_iff] at h
  rw [sstar_eq_iff, lobOwner_blk, lobOwner_role]
  split_ifs <;> omega

theorem lobOwner_card (L : ℕ) (u : Sstar L) :
    (univ.filter (fun v : {v // v ∉ Sstar L} => lobOwner L v = u)).card = lobNu L u := by
  have hu := (mem_Sstar u.1).1 u.2
  have hb := u.1.1.isLt
  rw [lobNu_eq]
  split_ifs with h0
  · rw [card_eq_zero, filter_eq_empty_iff]
    intro v _ hv
    rw [sstar_eq_iff, lobOwner_blk, lobOwner_role] at hv
    split_ifs at hv <;> omega
  · rw [card_eq_two]
    refine ⟨lobO L u.1.1.val (2 * u.1.2.val + 1) hb (by omega) (by omega),
      lobO L u.1.1.val (2 * u.1.2.val + 2) hb (by omega) (by omega), ?_, ?_⟩
    · rw [Ne, out_eq_iff, lobO_blk, lobO_blk, lobO_role, lobO_role]
      omega
    · ext v
      have hv1 : ¬ v.1.2.val ≤ 2 := fun h => v.2 ((mem_Sstar v.1).2 h)
      have hv2 := v.1.2.isLt
      simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton, out_eq_iff,
        sstar_eq_iff, lobOwner_blk, lobOwner_role, lobO_blk, lobO_role]
      split_ifs <;> omega

/-- `lem:rst-E` holds with equality on `Λ_L`, with `ν = 2` at the legs and `0` on the spine
Also true at `L = 0` (both sides `0`). -/
theorem lob_termCount_eq (L : ℕ) (X : Finset (Sstar L)) :
    termCount (Lam L) (X.map (Function.Embedding.subtype _))
      = treePotential (lobF L) (lobNu L) X := by
  rw [tree_reduction_eq (Lam L) (Sstar L) (lobF L) rfl (lobOwner L) (lobOwner_adj L)
    (lobOwner_uniq L) X]
  congr 1
  funext u
  exact lobOwner_card L u

/-- `W_{S*} = W_{F,ν}`. Also true at `L = 0` (both sides `1`). -/
theorem lobW_eq_treeW (L : ℕ) (y : ℝ) :
    W (gT (Lam L)) (Sstar L) (3 * L) y = treeW (lobF L) (lobNu L) y := by
  rw [RateAssembly.W_gT]
  unfold treeW
  symm
  refine sum_nbij' (fun X => X.map (Function.Embedding.subtype _))
    (fun Y => Y.subtype (fun x => x ∈ Sstar L)) ?_ ?_ ?_ ?_ ?_
  · 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, lob_termCount_eq]

/-! #### Helpers: the messages along the spine -/

/-- The vertices of `S*` in blocks `≤ i`. -/
def lobBlk (L i : ℕ) : Finset (Sstar L) := univ.filter (fun v => v.1.1.val ≤ i)

/-- The vertices of `S*` in block `i`. -/
def lobBlkA (L i : ℕ) : Finset (Sstar L) := univ.filter (fun v => v.1.1.val = i)

theorem lobBlk_zero (L : ℕ) : lobBlk L 0 = lobBlkA L 0 := by
  ext v; simp [lobBlk, lobBlkA]

theorem lobBlk_succ (L i : ℕ) : lobBlk L (i + 1) = lobBlkA L (i + 1) ∪ lobBlk L i := by
  ext v; simp only [lobBlk, lobBlkA, mem_filter, mem_univ, true_and, mem_union]; omega

theorem lobBlk_last (L : ℕ) : lobBlk L (L - 1) = univ := by
  ext v
  have := v.1.1.isLt
  simp only [lobBlk, mem_filter, mem_univ, true_and, iff_true]
  omega

theorem lob_par_role (L : ℕ) (hL : 1 ≤ L) (u : Sstar L) (hu : u ≠ lobRoot L hL) :
    (CDS.par (lobF_isTree L hL) (lobRoot L hL) u).1.2.val = 0 := by
  rw [lob_par L hL u hu]; exact lobP_role L u

/-- The message of one block, `ψ = Init(0) ∘ Init(2) ∘ Init(2) = u_y`. -/
theorem lob_triple_A (L : ℕ) (hL : 1 ≤ L) [DecidableRel (lobF L).Adj] (y : ℝ) (i : ℕ)
    (hi : i < L) :
    Antinorm3.triple (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y (lobBlkA L i)
      (lobV L i 0 hi (Nat.zero_le _)) = Lobster.toT (Lobster.u y) := by
  have hA : lobBlkA L i = ({lobV L i 0 hi (Nat.zero_le _)} ∪ {lobV L i 1 hi (by norm_num)})
      ∪ {lobV L i 2 hi le_rfl} := by
    ext v
    have := (mem_Sstar v.1).1 v.2
    simp only [lobBlkA, mem_filter, mem_univ, true_and, mem_union, mem_singleton, sstar_eq_iff,
      lobV_blk, lobV_role]
    omega
  have hr1 : lobV L i 1 hi (by norm_num) ≠ lobRoot L hL := by
    simp only [lobRoot, ne_eq, sstar_eq_iff, lobV_blk, lobV_role]; omega
  have hr2 : lobV L i 2 hi le_rfl ≠ lobRoot L hL := by
    simp only [lobRoot, ne_eq, sstar_eq_iff, lobV_blk, lobV_role]; omega
  have hp1 : CDS.par (lobF_isTree L hL) (lobRoot L hL) (lobV L i 1 hi (by norm_num))
      = lobV L i 0 hi (Nat.zero_le _) := by
    rw [lob_par L hL _ hr1, sstar_eq_iff]
    have h1 := lobP_blk L (lobV L i 1 hi (by norm_num))
    have h2 := lobP_role L (lobV L i 1 hi (by norm_num))
    simp only [lobV_blk, lobV_role] at h1 h2 ⊢; omega
  have hp2 : CDS.par (lobF_isTree L hL) (lobRoot L hL) (lobV L i 2 hi le_rfl)
      = lobV L i 0 hi (Nat.zero_le _) := by
    rw [lob_par L hL _ hr2, sstar_eq_iff]
    have h1 := lobP_blk L (lobV L i 2 hi le_rfl)
    have h2 := lobP_role L (lobV L i 2 hi le_rfl)
    simp only [lobV_blk, lobV_role] at h1 h2 ⊢; omega
  -- first split: `A = {x, ℓ₁}`, `B = {ℓ₂}`
  have d1 : Disjoint ({lobV L i 0 hi (Nat.zero_le _)} ∪ {lobV L i 1 hi (by norm_num)})
      ({lobV L i 2 hi le_rfl} : Finset (Sstar L)) := by
    refine disjoint_left.2 fun a ha hb => ?_
    simp only [mem_union, mem_singleton, sstar_eq_iff, lobV_blk, lobV_role] at ha hb; omega
  have e1 : ∀ a ∈ ({lobV L i 0 hi (Nat.zero_le _)} ∪ {lobV L i 1 hi (by norm_num)} :
      Finset (Sstar L)), ∀ b ∈ ({lobV L i 2 hi le_rfl} : Finset (Sstar L)),
      (lobF L).Adj a b → a = lobV L i 0 hi (Nat.zero_le _) ∧ b = lobV L i 2 hi le_rfl := by
    intro a ha b hb hab
    rw [lobF_adj_val] at hab
    simp only [mem_union, mem_singleton, sstar_eq_iff, lobV_blk, lobV_role] at ha hb ⊢; omega
  have b1 : ∀ u ∈ ({lobV L i 2 hi le_rfl} : Finset (Sstar L)), u ≠ lobV L i 2 hi le_rfl →
      u ≠ lobRoot L hL ∧ CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∈
        ({lobV L i 2 hi le_rfl} : Finset (Sstar L)) :=
    fun u hu hne => absurd (mem_singleton.1 hu) hne
  have a1 : ∀ u ∈ ({lobV L i 0 hi (Nat.zero_le _)} ∪ {lobV L i 1 hi (by norm_num)} :
      Finset (Sstar L)), u ≠ lobRoot L hL → CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∉
        ({lobV L i 2 hi le_rfl} : Finset (Sstar L)) := by
    intro u _ hu
    have := lob_par_role L hL u hu
    rw [mem_singleton, sstar_eq_iff, lobV_blk, lobV_role]
    omega
  -- second split: `A = {x}`, `B = {ℓ₁}`
  have d2 : Disjoint ({lobV L i 0 hi (Nat.zero_le _)} : Finset (Sstar L))
      {lobV L i 1 hi (by norm_num)} := by
    rw [disjoint_singleton, ne_eq, sstar_eq_iff, lobV_blk, lobV_role, lobV_blk, lobV_role]
    omega
  have e2 : ∀ a ∈ ({lobV L i 0 hi (Nat.zero_le _)} : Finset (Sstar L)),
      ∀ b ∈ ({lobV L i 1 hi (by norm_num)} : Finset (Sstar L)),
      (lobF L).Adj a b → a = lobV L i 0 hi (Nat.zero_le _) ∧ b = lobV L i 1 hi (by norm_num) :=
    fun a ha b hb _ => ⟨mem_singleton.1 ha, mem_singleton.1 hb⟩
  have b2 : ∀ u ∈ ({lobV L i 1 hi (by norm_num)} : Finset (Sstar L)),
      u ≠ lobV L i 1 hi (by norm_num) →
      u ≠ lobRoot L hL ∧ CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∈
        ({lobV L i 1 hi (by norm_num)} : Finset (Sstar L)) :=
    fun u hu hne => absurd (mem_singleton.1 hu) hne
  have a2 : ∀ u ∈ ({lobV L i 0 hi (Nat.zero_le _)} : Finset (Sstar L)), u ≠ lobRoot L hL →
      CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∉
        ({lobV L i 1 hi (by norm_num)} : Finset (Sstar L)) := by
    intro u _ hu
    have := lob_par_role L hL u hu
    rw [mem_singleton, sstar_eq_iff, lobV_blk, lobV_role]
    omega
  rw [hA, Antinorm3.triple_split (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y d1
      (mem_union_left _ (mem_singleton_self _)) (mem_singleton_self _) hr2 hp2 e1 b1 a1,
    Antinorm3.triple_split (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y d2
      (mem_singleton_self _) (mem_singleton_self _) hr1 hp1 e2 b2 a2,
    Antinorm3.triple_single, Antinorm3.triple_single, Antinorm3.triple_single, Lobster.u_eq,
    lobNu_eq, lobNu_eq, lobNu_eq, lobV_role, lobV_role, lobV_role]
  rfl

/-- The message of the blocks `≤ i` at `x_i` is `M_y^i u_y`. -/
theorem lob_triple_blk (L : ℕ) (hL : 1 ≤ L) [DecidableRel (lobF L).Adj] (y : ℝ) (i : ℕ)
    (hi : i < L) :
    Antinorm3.triple (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y (lobBlk L i)
      (lobV L i 0 hi (Nat.zero_le _)) = Lobster.toT (Lobster.M y ^ i *ᵥ Lobster.u y) := by
  induction i with
  | zero =>
    rw [lobBlk_zero, pow_zero, Matrix.one_mulVec]
    exact lob_triple_A L hL y 0 hi
  | succ i ih =>
    have hi' : i < L := by omega
    have hwr : lobV L i 0 hi' (Nat.zero_le _) ≠ lobRoot L hL := by
      simp only [lobRoot, ne_eq, sstar_eq_iff, lobV_blk, lobV_role]; omega
    have hpw : CDS.par (lobF_isTree L hL) (lobRoot L hL) (lobV L i 0 hi' (Nat.zero_le _))
        = lobV L (i + 1) 0 hi (Nat.zero_le _) := by
      rw [lob_par L hL _ hwr, sstar_eq_iff]
      have h1 := lobP_blk L (lobV L i 0 hi' (Nat.zero_le _))
      have h2 := lobP_role L (lobV L i 0 hi' (Nat.zero_le _))
      simp only [lobV_blk, lobV_role, true_and] at h1 h2 ⊢; omega
    have hAB : Disjoint (lobBlkA L (i + 1)) (lobBlk L i) := by
      refine disjoint_left.2 fun a ha hb => ?_
      simp only [lobBlkA, lobBlk, mem_filter, mem_univ, true_and] at ha hb
      omega
    have hv : lobV L (i + 1) 0 hi (Nat.zero_le _) ∈ lobBlkA L (i + 1) := by
      simp only [lobBlkA, mem_filter, mem_univ, true_and, lobV_blk]
    have hw : lobV L i 0 hi' (Nat.zero_le _) ∈ lobBlk L i := by
      simp only [lobBlk, mem_filter, mem_univ, true_and, lobV_blk, le_refl]
    have hedge : ∀ a ∈ lobBlkA L (i + 1), ∀ b ∈ lobBlk L i, (lobF L).Adj a b →
        a = lobV L (i + 1) 0 hi (Nat.zero_le _) ∧ b = lobV L i 0 hi' (Nat.zero_le _) := by
      intro a ha b hb hab
      rw [lobF_adj_val] at hab
      simp only [lobBlkA, lobBlk, mem_filter, mem_univ, true_and] at ha hb
      simp only [sstar_eq_iff, lobV_blk, lobV_role]
      omega
    have hB : ∀ u ∈ lobBlk L i, u ≠ lobV L i 0 hi' (Nat.zero_le _) →
        u ≠ lobRoot L hL ∧ CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∈ lobBlk L i := by
      intro u hu hne
      simp only [lobBlk, mem_filter, mem_univ, true_and] at hu ⊢
      have hur : u ≠ lobRoot L hL := by
        simp only [lobRoot, ne_eq, sstar_eq_iff, lobV_blk, lobV_role]; omega
      refine ⟨hur, ?_⟩
      rw [lob_par L hL u hur]
      have := lobP_blk L u
      rw [ne_eq, sstar_eq_iff, lobV_blk, lobV_role] at hne
      omega
    have hA : ∀ u ∈ lobBlkA L (i + 1), u ≠ lobRoot L hL →
        CDS.par (lobF_isTree L hL) (lobRoot L hL) u ∉ lobBlk L i := by
      intro u hu hur
      rw [lob_par L hL u hur]
      simp only [lobBlkA, lobBlk, mem_filter, mem_univ, true_and] at hu ⊢
      have := lobP_blk L u
      omega
    rw [lobBlk_succ, Antinorm3.triple_split (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y hAB hv
      hw hwr hpw hedge hB hA, lob_triple_A L hL y (i + 1) hi, ih hi', ← Lobster.M_mulVec,
      Matrix.mulVec_mulVec, ← pow_succ']

/-- `W_{F,ν}(y) = fin(M_y^{L-1} u_y)` (`lem:rst-treerec` on `G[S*]`). -/
theorem lob_treeW_eq (L : ℕ) (hL : 1 ≤ L) (y : ℝ) :
    treeW (lobF L) (lobNu L) y = Lobster.f ⬝ᵥ (Lobster.M y ^ (L - 1) *ᵥ Lobster.u y) := by
  classical
  have key := lob_triple_blk L hL y (L - 1) (by omega)
  rw [lobBlk_last] at key
  have key' : Antinorm3.triple (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y univ (lobRoot L hL)
      = Lobster.toT (Lobster.M y ^ (L - 1) *ᵥ Lobster.u y) := key
  rw [Antinorm3.treeW_eq_fin (lobF_isTree L hL) (lobRoot L hL) (lobNu L) y, key', Lobster.f_dot]
  rfl

/-- **The identity** `W_{S*}(y) = fᵀ M_y^{L-1} u_y`. -/
theorem lobW_eq_matrix (L : ℕ) (hL : 1 ≤ L) (y : ℝ) :
    W (gT (Lam L)) (Sstar L) (3 * L) y = Lobster.f ⬝ᵥ (Lobster.M y ^ (L - 1) *ᵥ Lobster.u y) := by
  rw [lobW_eq_treeW, lob_treeW_eq L hL y]

/-- `prop:rst-caterpillar`(c), first bound: `μ_t(S*)/C(n,t) ≤ (n+1) 1.71927^{-n}` for `0 ≤ t ≤ n`. -/
theorem lob_moments_upper (L : ℕ) (hL : 1 ≤ L) (t : ℕ) (ht : t ≤ 7 * L) :
    mu (gT (Lam L)) (Sstar L) (3 * L) t / ((7 * L).choose t : ℝ)
      ≤ (((7 * L : ℕ) : ℝ) + 1) / (171927 / 100000 : ℝ) ^ (7 * L) := by
  have hB : (0 : ℝ) < (171927 / 100000 : ℝ) ^ (7 * L) := by positivity
  have hC : (0 : ℝ) < ((7 * L).choose t : ℝ) := by exact_mod_cast Nat.choose_pos ht
  by_cases h3' : 3 * L < t
  · have h3 := h3'
    have h0 : mu (gT (Lam L)) (Sstar L) (3 * L) t = 0 := by
      unfold MLS.mu
      refine sum_eq_zero fun X hX => ?_
      exfalso
      have h1 := card_le_card (mem_powersetCard.1 hX).1
      rw [(mem_powersetCard.1 hX).2, card_Sstar] at h1
      omega
    rw [h0, zero_div]
    positivity
  · have h3 : t ≤ 3 * L := not_lt.1 h3'
    have htn : t < 7 * L := by omega
    have hnt : (0 : ℝ) < ((7 * L : ℕ) : ℝ) - t := by
      have : (t : ℝ) < ((7 * L : ℕ) : ℝ) := by exact_mod_cast htn
      linarith
    set y : ℝ := (t : ℝ) / (((7 * L : ℕ) : ℝ) - t) with hy
    have hy0 : 0 ≤ y := div_nonneg (Nat.cast_nonneg _) hnt.le
    have hy34 : y ≤ 3 / 4 := by
      rw [hy, div_le_iff₀ hnt]
      have h1 : (t : ℝ) ≤ 3 * L := by exact_mod_cast h3
      push_cast
      linarith
    have hyt : 0 < y ^ t := by
      rcases Nat.eq_zero_or_pos t with h | h
      · rw [h, pow_zero]; exact one_pos
      · exact pow_pos (div_pos (by exact_mod_cast h) hnt) _
    have h1 : mu (gT (Lam L)) (Sstar L) (3 * L) t * y ^ t
        ≤ Lobster.f ⬝ᵥ (Lobster.M y ^ (L - 1) *ᵥ Lobster.u y) := by
      rw [← lobW_eq_matrix L hL y]
      exact mu_mul_pow_le_W _ _ _ _ _ hy0
    have h2 := Lobster.lobster_lower L hL y ⟨hy0, hy34⟩
    have h3' : (1 + y) ^ (7 * L) ≤ (((7 * L : ℕ) : ℝ) + 1) * ((7 * L).choose t : ℝ) * y ^ t :=
      pow_le_choose_mul (7 * L) t htn
    have key : mu (gT (Lam L)) (Sstar L) (3 * L) t * y ^ t * (171927 / 100000 : ℝ) ^ (7 * L)
        ≤ (((7 * L : ℕ) : ℝ) + 1) * ((7 * L).choose t : ℝ) * y ^ t := by
      have := (le_div_iff₀ hB).1 (h1.trans h2)
      linarith
    rw [div_le_div_iff₀ hC hB]
    have key2 : (mu (gT (Lam L)) (Sstar L) (3 * L) t * (171927 / 100000 : ℝ) ^ (7 * L)) * y ^ t
        ≤ ((((7 * L : ℕ) : ℝ) + 1) * ((7 * L).choose t : ℝ)) * y ^ t := by
      calc (mu (gT (Lam L)) (Sstar L) (3 * L) t * (171927 / 100000 : ℝ) ^ (7 * L)) * y ^ t
          = mu (gT (Lam L)) (Sstar L) (3 * L) t * y ^ t * (171927 / 100000 : ℝ) ^ (7 * L) := by
            ring
        _ ≤ _ := key
    exact le_of_mul_le_mul_right key2 hyt

/-- `prop:rst-caterpillar`(c), converse: `min_t C(n,t)/μ_t(S*) ≤ C · 1.71928^n`, without division. -/
theorem lob_moments_lower :
    ∃ C : ℝ, 0 < C ∧ ∀ L : ℕ, 1 ≤ L → ∃ t ≤ 3 * L,
      ((7 * L).choose t : ℝ)
        ≤ C * (171928 / 100000 : ℝ) ^ (7 * L) * mu (gT (Lam L)) (Sstar L) (3 * L) t := by
  obtain ⟨C, hC, hup⟩ := Lobster.lobster_upper
  refine ⟨C, hC, fun L hL => ?_⟩
  by_contra hcon
  simp only [not_exists, not_and, not_le] at hcon
  have h1 := hup L hL
  rw [← lobW_eq_matrix L hL, MLS.W_eq_sum_mu _ _ _ (card_Sstar L)] at h1
  have h2 : C * (171928 / 100000 : ℝ) ^ (7 * L) * ∑ t ∈ range (3 * L + 1),
        (3453 / 10000 : ℝ) ^ t * mu (gT (Lam L)) (Sstar L) (3 * L) t
      < ∑ t ∈ range (3 * L + 1), (3453 / 10000 : ℝ) ^ t * ((7 * L).choose t : ℝ) := by
    rw [mul_sum]
    apply sum_lt_sum_of_nonempty ⟨0, by simp⟩
    intro t ht
    have hyt : (0 : ℝ) < (3453 / 10000 : ℝ) ^ t := by positivity
    have := hcon t (Nat.lt_succ_iff.1 (mem_range.1 ht))
    calc C * (171928 / 100000 : ℝ) ^ (7 * L)
          * ((3453 / 10000 : ℝ) ^ t * mu (gT (Lam L)) (Sstar L) (3 * L) t)
        = (3453 / 10000 : ℝ) ^ t
          * (C * (171928 / 100000 : ℝ) ^ (7 * L) * mu (gT (Lam L)) (Sstar L) (3 * L) t) := by
          ring
      _ < (3453 / 10000 : ℝ) ^ t * ((7 * L).choose t : ℝ) := mul_lt_mul_of_pos_left this hyt
  have h3 : ∑ t ∈ range (3 * L + 1), (3453 / 10000 : ℝ) ^ t * ((7 * L).choose t : ℝ)
      ≤ (1 + 3453 / 10000 : ℝ) ^ (7 * L) := by
    rw [add_comm (1 : ℝ), add_pow]
    calc ∑ t ∈ range (3 * L + 1), (3453 / 10000 : ℝ) ^ t * ((7 * L).choose t : ℝ)
        ≤ ∑ t ∈ range (7 * L + 1), (3453 / 10000 : ℝ) ^ t * ((7 * L).choose t : ℝ) := by
          apply sum_le_sum_of_subset_of_nonneg
          · intro t ht
            simp only [mem_range] at ht ⊢
            omega
          · intro t _ _
            positivity
      _ = _ := by
          refine sum_congr rfl fun t _ => ?_
          rw [one_pow, mul_one]
  linarith

/-- `prop:rst-caterpillar`(c), the two bounds together. -/
theorem rst_caterpillar_c :
    (∀ L : ℕ, 1 ≤ L → ∀ t ≤ 7 * L,
      mu (gT (Lam L)) (Sstar L) (3 * L) t / ((7 * L).choose t : ℝ)
        ≤ (((7 * L : ℕ) : ℝ) + 1) / (171927 / 100000 : ℝ) ^ (7 * L)) ∧
    ∃ C : ℝ, 0 < C ∧ ∀ L : ℕ, 1 ≤ L → ∃ t ≤ 3 * L,
      ((7 * L).choose t : ℝ)
        ≤ C * (171928 / 100000 : ℝ) ^ (7 * L) * mu (gT (Lam L)) (Sstar L) (3 * L) t :=
  ⟨fun L hL t ht => lob_moments_upper L hL t ht, lob_moments_lower⟩

/-! ### Optional: graphs that agree with `Λ_L` at `S*` -/

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

/-- Two graphs with the same edges at every vertex of `S` have the same `|Tm(J_X)|` for `X ⊆ S`. -/
theorem termCount_congr (G H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj]
    (S : Finset V) (hGH : ∀ u ∈ S, ∀ v, G.Adj u v ↔ H.Adj u v) (X : Finset V) (hX : X ⊆ S) :
    termCount G X = termCount H X := by
  have hN : closedNbhd G X = closedNbhd H X := by
    ext v
    rw [mem_closedNbhd, mem_closedNbhd]
    constructor
    · rintro (h | ⟨x, hx, hxv⟩)
      · exact Or.inl h
      · exact Or.inr ⟨x, hx, (hGH x (hX hx) v).1 hxv⟩
    · rintro (h | ⟨x, hx, hxv⟩)
      · exact Or.inl h
      · exact Or.inr ⟨x, hx, (hGH x (hX hx) v).2 hxv⟩
  have hI : G.induce (X : Set V) = H.induce (X : Set V) := by
    ext a b
    exact hGH a.1 (hX (mem_coe.1 a.2)) b.1
  unfold termCount CDS.comp
  rw [hN, hI]

end Agree

/-- `prop:rst-caterpillar`(c) for every graph that agrees with `Λ_L` on all edges at `S*`
(added edges join two claws), as the paragraph after the proposition says. -/
theorem rst_caterpillar_c_of_agree :
    (∀ L : ℕ, 1 ≤ L → ∀ (G : SimpleGraph (Fin L × Fin 7)) [DecidableRel G.Adj],
      (∀ u ∈ Sstar L, ∀ v, G.Adj u v ↔ (Lam L).Adj u v) →
      ∀ t ≤ 7 * L,
        mu (gT G) (Sstar L) (3 * L) t / ((7 * L).choose t : ℝ)
          ≤ (((7 * L : ℕ) : ℝ) + 1) / (171927 / 100000 : ℝ) ^ (7 * L)) ∧
    ∃ C : ℝ, 0 < C ∧ ∀ L : ℕ, 1 ≤ L → ∀ (G : SimpleGraph (Fin L × Fin 7)) [DecidableRel G.Adj],
      (∀ u ∈ Sstar L, ∀ v, G.Adj u v ↔ (Lam L).Adj u v) →
      ∃ t ≤ 3 * L,
        ((7 * L).choose t : ℝ)
          ≤ C * (171928 / 100000 : ℝ) ^ (7 * L) * mu (gT G) (Sstar L) (3 * L) t := by
  have hmu : ∀ (L : ℕ) (G : SimpleGraph (Fin L × Fin 7)) [DecidableRel G.Adj],
      (∀ u ∈ Sstar L, ∀ v, G.Adj u v ↔ (Lam L).Adj u v) →
      ∀ t, mu (gT G) (Sstar L) (3 * L) t = mu (gT (Lam L)) (Sstar L) (3 * L) t := by
    intro L G _ hG t
    unfold MLS.mu RateAssembly.gT
    refine sum_congr rfl fun X hX => ?_
    rw [termCount_congr G (Lam L) (Sstar L) hG X (mem_powersetCard.1 hX).1]
  obtain ⟨C, hC, hlow⟩ := lob_moments_lower
  refine ⟨fun L hL G _ hG t ht => ?_, C, hC, fun L hL G _ hG => ?_⟩
  · rw [hmu L G hG t]
    exact lob_moments_upper L hL t ht
  · obtain ⟨t, ht, h⟩ := hlow L hL
    exact ⟨t, ht, by rw [hmu L G hG t]; exact h⟩

end MaxLeafFormal.LobsterGraph