diff --git a/Complexity.lean b/Complexity.lean
index 5222071544..e4ad5726fc 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2180,6 +2180,7 @@ public import Complexity.Logics.Propositional.ClauseSet.Basic
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingDeletion
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingUnits
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.List
diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingDeletion.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingDeletion.lean
new file mode 100644
index 0000000000..62acd241ea
--- /dev/null
+++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingDeletion.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences
+public import Mathlib.Order.Interval.Finset.Nat
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Algebra.Group.Action.Defs
+
+/-!
+# Charging deleted marked clauses to actual counting insertions
+
+The deletion-charge argument of Appendix A.2, Lemma A.3 and (A.3) [OpenAI2026ETH] assigns
+a removed marked width-`j` clause to a new strict subclause inserted in that step.
+The present-clause bound supplies at most `2 * θ (j - i)` recipients for a width-`i` insertion.
+
+Here the donor is proved absent from both the current node and the root. Every root clause has a
+current subclause, directly from the actual reduction steps; a root donor would contradict current
+reducedness. This is not the decision-path `Refines` property. The actual counting payload includes
+the B-child's negated-heart units.
+
+This bounds deletion of clauses present before one step. It does not assert immediate survival of
+new higher-width payload clauses, nor the complete insertion recurrence or a depth/leaf/runtime
+bound. Nontautology is not needed for this one-step old-clause charge; its role in immediate
+survival and the later insertion-event balance remains separate.
+
+## Main results
+
+* `Cslib.Logic.PL.ClauseSet.Sparsification.exists_mem_counting_node_subset`: root witnesses persist.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_deleted_marked_le`: deletion charge.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.ClauseSet.Sparsification
+
+open Finset
+
+variable {V : Type*} [DecidableEq V]
+
+/-- Every root clause contains a clause of each later node of an actual counting path.
+This direction of containment holds for reduction after additions, including negated units. -/
+theorem exists_mem_counting_node_subset
+    (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool)
+    (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i))
+    {t : ℕ} (ht : t ≤ N) {C : Finset (Literal V)} (hC : C ∈ ψ 0) :
+    ∃ D ∈ ψ t, D ⊆ C := by
+  suffices ∀ t, t ≤ N → ∃ D ∈ ψ t, D ⊆ C from this t ht
+  intro t
+  induction t with
+  | zero => exact fun _ => ⟨C, hC, subset_rfl⟩
+  | succ t ih =>
+    intro ht
+    obtain ⟨D, hD, hDC⟩ := ih (by omega)
+    rw [hstep t (by omega), countingChild_eq_reduce_union]
+    obtain ⟨E, hE, hED⟩ := exists_mem_reduce_subset
+      (ψ := ψ t ∪ countingIntro (ψ t) (c t) (H t) (b t)) (mem_union_left _ hD)
+    exact ⟨E, hE, hED.trans hDC⟩
+
+/-- The width-`j` marked clauses deleted at one actual counting step can be charged to that step's
+new marked insertion events of smaller width, with the source's `2 * θ (j - i)` charge bound.
+
+The occurrence bound is derived from the actual path and both `Choice` priorities, not supplied
+as a hypothesis. The insertion batch excludes clauses in the current node OR the root. No finite
+ambient variable type, model count or native resource bound is assumed. -/
+theorem card_counting_deleted_marked_le {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r)
+    (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool)
+    (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i))
+    (hchoice : ∀ i < N, Choice θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0))
+    {m : ℕ} (hm : m < N) (j : ℕ) :
+    ((ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)).card ≤
+      ∑ i ∈ Ico 1 j, 2 * θ (j - i) *
+        (((countingIntro (ψ m) (c m) (H m) (b m)) \ (ψ m ∪ ψ 0)).filter
+          fun D => D.card = i).card := by
+  let I := countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0)
+  set E := (ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)
+  change E.card ≤ ∑ i ∈ Ico 1 j, 2 * θ (j - i) * (I.filter fun D => D.card = i).card
+  have hredm : Reduced (ψ m) := by
+    cases m with
+    | zero => exact hred
+    | succ m =>
+      rw [hstep m (by omega), countingChild_eq_reduce_union]
+      exact reduced_reduce _
+  have hcover : E ⊆ (I.filter (·.card < j)).biUnion fun D =>
+      (ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ D ⊆ C := by
+    intro C hC
+    obtain ⟨hCψ, hCroot, hCj, hCgone⟩ := mem_filter.mp hC
+    rw [hstep m hm, countingChild_eq_reduce_union] at hCgone
+    obtain ⟨D, hD, hDC⟩ := exists_ssubset_of_notMem_reduce hredm hCψ hCgone
+    have hDψ : D ∉ ψ m := fun h => hredm C hCψ D h hDC
+    have hDroot : D ∉ ψ 0 := by
+      intro hD0
+      obtain ⟨F, hF, hFD⟩ := exists_mem_counting_node_subset N ψ c H b hstep hm.le hD0
+      exact hredm C hCψ F hF (Finset.ssubset_of_subset_of_ssubset hFD hDC)
+    have hDI : D ∈ I := by
+      refine mem_sdiff.mpr ⟨hD, ?_⟩
+      exact fun h => (mem_union.mp h).elim hDψ hDroot
+    refine mem_biUnion.mpr ⟨D, mem_filter.mpr ⟨hDI, ?_⟩, ?_⟩
+    · exact hCj ▸ card_lt_card hDC
+    · exact mem_filter.mpr ⟨hCψ, hCroot, hCj, hDC.subset⟩
+  have hmaps : ∀ D ∈ I.filter (·.card < j), D.card ∈ Ico 1 j := by
+    intro D hD
+    obtain ⟨hDI, hDj⟩ := mem_filter.mp hD
+    have hDpos := countingIntro_nonempty (hchoice m hm).1.1 (hchoice m hm).1.2.1
+      (mem_sdiff.mp hDI).1
+    rw [← card_pos] at hDpos
+    exact mem_Ico.mpr ⟨by omega, hDj⟩
+  have hsum : (∑ D ∈ I.filter (·.card < j),
+      ((ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ D ⊆ C).card) ≤
+      ∑ i ∈ Ico 1 j, 2 * θ (j - i) * (I.filter fun D => D.card = i).card := by
+    calc
+      _ ≤ ∑ D ∈ I.filter (·.card < j), 2 * θ (j - D.card) := by
+        refine sum_le_sum fun D hD => ?_
+        exact (card_counting_newContaining_lt hθ N ψ c H b hstep hchoice hm.le
+          (mem_Ico.mp (hmaps D hD)).1 (mem_filter.mp hD).2).le
+      _ = ∑ i ∈ Ico 1 j, ∑ D ∈ (I.filter (·.card < j)).filter (·.card = i),
+          2 * θ (j - i) := (sum_fiberwise_of_maps_to' hmaps fun i => 2 * θ (j - i)).symm
+      _ = ∑ i ∈ Ico 1 j, 2 * θ (j - i) * (I.filter fun D => D.card = i).card := by
+        refine sum_congr rfl fun i hi => ?_
+        have hij := (mem_Ico.mp hi).2
+        rw [sum_const, smul_eq_mul, mul_comm]
+        congr 2
+        ext D
+        simp only [mem_filter]
+        constructor
+        · rintro ⟨⟨hDI, -⟩, hDi⟩
+          exact ⟨hDI, hDi⟩
+        · rintro ⟨hDI, hDi⟩
+          exact ⟨⟨hDI, hDi ▸ hij⟩, hDi⟩
+  exact (card_le_card hcover).trans (card_biUnion_le.trans hsum)
+
+end Cslib.Logic.PL.ClauseSet.Sparsification
diff --git a/ComplexityTests/SparsificationCountingDeletion.lean b/ComplexityTests/SparsificationCountingDeletion.lean
new file mode 100644
index 0000000000..fe0a1f2d2e
--- /dev/null
+++ b/ComplexityTests/SparsificationCountingDeletion.lean
@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingDeletion
+
+public section
+
+open Cslib.Logic.PL
+open ClauseSet.Sparsification Finset
+
+namespace ComplexityTests.SparsificationCountingDeletion
+
+-- A negated-heart unit deletes a clause outside the selected flower.
+theorem negated_unit_deletes_unselected_pair : {(0, false), (1, true)} ∉ countingChild
+    ({{(0, false), (1, true)}, {(0, true), (2, true)}, {(0, true), (3, true)}} :
+      ClauseSet (Fin 4)) 2 {(0, true)} true := by decide
+
+private def θ (j : ℕ) := 2 ^ j
+
+private theorem θpos (j : ℕ) : 1 ≤ θ j := by
+  induction j with
+  | zero => decide
+  | succ j ih =>
+    change 1 ≤ 2 ^ (j + 1)
+    rw [pow_succ]
+    change 1 ≤ 2 ^ j at ih
+    omega
+
+private theorem θtwo {j : ℕ} (hj : 0 < j) : 2 ≤ θ j := by
+  cases j with
+  | zero => omega
+  | succ j =>
+    change 2 ≤ 2 ^ (j + 1)
+    rw [pow_succ]
+    have := θpos j
+    change 1 ≤ 2 ^ j at this
+    omega
+
+-- A heavy flower contains two different clauses. Their common width establishes the minimum
+-- priority, and the intersection cap establishes the maximum-heart priority.
+private theorem choice_of_pairs {V : Type*} [DecidableEq V]
+    {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hh : Heavy θ ψ c H)
+    (hw : ∀ C ∈ ψ, ∀ D ∈ ψ, C ≠ D → C.card = D.card → C.card = c)
+    (hinter : ∀ C ∈ ψ, ∀ D ∈ ψ, C ≠ D → (C ∩ D).card ≤ H.card) : Choice θ ψ c H := by
+  refine ⟨hh, ?_, ?_⟩
+  · intro c' H' hh'
+    have htwo : 2 ≤ (flower ψ c' H').card := (θtwo (Nat.sub_pos_of_lt hh'.2.1)).trans hh'.2.2
+    obtain ⟨C, hC, D, hD, hCD⟩ := one_lt_card.mp (by omega : 1 < (flower ψ c' H').card)
+    have hCc := (mem_flower.mp hC).2.1
+    have hDc := (mem_flower.mp hD).2.1
+    have := hw C (flower_subset _ _ _ hC) D (flower_subset _ _ _ hD) hCD (by omega)
+    omega
+  · intro H' hh'
+    have htwo : 2 ≤ (flower ψ c H').card := (θtwo (Nat.sub_pos_of_lt hh'.2.1)).trans hh'.2.2
+    obtain ⟨C, hC, D, hD, hCD⟩ := one_lt_card.mp (by omega : 1 < (flower ψ c H').card)
+    exact (card_le_card (subset_inter (mem_flower.mp hC).2.2 (mem_flower.mp hD).2.2)).trans
+      (hinter C (flower_subset _ _ _ hC) D (flower_subset _ _ _ hD) hCD)
+
+private def root : ClauseSet (Fin 9) :=
+  {{(1, true), (2, true)}, {(0, true), (1, false), (3, true)},
+    {(0, true), (1, true), (4, true)}, {(0, true), (5, true), (6, true)},
+    {(0, true), (7, true), (8, true)}}
+
+private def first := countingChild root 3 {(0, true)} true
+private def nodes (tail : Bool) (i : ℕ) :=
+  if i = 0 then root else if i = 1 then first else countingChild first 2 {(1, true)} tail
+private def sizes (i : ℕ) := if i = 0 then 3 else 2
+private def hearts (i : ℕ) : Finset (Literal (Fin 9)) :=
+  if i = 0 then {(0, true)} else {(1, true)}
+private def dirs (tail : Bool) (i : ℕ) := if i = 0 then true else tail
+
+private theorem firstChoice : Choice θ root 3 {(0, true)} := by
+  apply choice_of_pairs
+  · unfold Heavy; decide
+  · decide
+  · decide
+
+private theorem secondChoice : Choice θ first 2 {(1, true)} := by
+  refine ⟨?_, ?_, ?_⟩
+  · unfold Heavy; decide
+  · intro c H hh
+    have := hh.1
+    have := hh.2.1
+    omega
+  · intro H hh
+    have := hh.2.1
+    change H.card ≤ 1
+    omega
+
+private theorem steps (tail : Bool) : ∀ i < 2,
+    nodes tail (i + 1) = countingChild (nodes tail i) (sizes i) (hearts i) (dirs tail i) := by
+  intro i hi
+  have : i = 0 ∨ i = 1 := by omega
+  rcases this with rfl | rfl <;> rfl
+
+private theorem choices (tail : Bool) : ∀ i < 2,
+    Choice θ (nodes tail i) (sizes i) (hearts i) := by
+  intro i hi
+  have : i = 0 ∨ i = 1 := by omega
+  rcases this with rfl | rfl
+  · exact firstChoice
+  · exact secondChoice
+
+private theorem rootReduced : Reduced root := by unfold Reduced; decide
+
+-- Three width-two clauses disappear, but the initial root pair must not be counted as marked.
+example : (first.filter fun C => C.card = 2 ∧ C ∉ nodes true 2).card = 3 := by decide
+example : (first.filter fun C => C ∉ root ∧ C.card = 2 ∧ C ∉ nodes true 2).card = 2 := by decide
+
+-- The unselected marked pair has NO petal donor. The added negated-heart unit is indispensable.
+example : {(1, false), (3, true)} ∉ flower first 2 {(1, true)} := by decide
+example : ¬ ∃ D ∈ petals first 2 {(1, true)}, D ⊆ ({(1, false), (3, true)} :
+    Finset (Literal (Fin 9))) := by decide
+example : {(1, false)} ∈ countingIntro first 2 {(1, true)} true \ (first ∪ root) ∧
+    ({(1, false)} : Finset (Literal (Fin 9))) ⊂ {(1, false), (3, true)} := by decide
+
+example : ((countingIntro first 2 {(1, true)} true \ (first ∪ root)).filter
+    fun D => D.card = 1).card = 3 := by decide
+
+example : (first.filter fun C => C ∉ root ∧ C.card = 2 ∧ C ∉ nodes true 2).card ≤ 12 := by
+  exact card_counting_deleted_marked_le θpos 2 (nodes true) sizes hearts (dirs true)
+    (steps true) (choices true) rootReduced (m := 1) (by omega) 2
+
+example : (first.filter fun C => C ∉ root ∧ C.card = 2 ∧ C ∉ nodes false 2).card = 1 := by decide
+
+example : (first.filter fun C => C ∉ root ∧ C.card = 2 ∧ C ∉ nodes false 2).card ≤ 4 := by
+  exact card_counting_deleted_marked_le θpos 2 (nodes false) sizes hearts (dirs false)
+    (steps false) (choices false) rootReduced (m := 1) (by omega) 2
+
+-- Unit deletions have zero charge: Ico 1 1 is empty.
+example : (first.filter fun C => C ∉ root ∧ C.card = 1 ∧ C ∉ nodes true 2).card ≤ 0 := by
+  exact card_counting_deleted_marked_le θpos 2 (nodes true) sizes hearts (dirs true)
+    (steps true) (choices true) rootReduced (m := 1) (by omega) 1
+
+example : ∃ D ∈ nodes true 2, D ⊆ ({(0, true), (1, false), (3, true)} :
+    Finset (Literal (Fin 9))) :=
+  exists_mem_counting_node_subset 2 (nodes true) sizes hearts (dirs true) (steps true)
+    (t := 2) le_rfl (by decide)
+
+-- Empty variables and an empty root clause need no inhabitance at a zero-length prefix.
+example : ∃ D ∈ ({∅} : ClauseSet Empty), D ⊆ (∅ : Finset (Literal Empty)) :=
+  exists_mem_counting_node_subset 0 (fun _ => ({∅} : ClauseSet Empty)) id
+    (fun _ => ∅) (fun _ => false) (by intro i hi; omega) (t := 0) le_rfl (by decide)
+
+-- The FULL insertion balance still needs nontautology. In this reduced, legal-choice root,
+-- one newly introduced width-two petal is immediately removed by the added negated unit.
+private def tautRoot : ClauseSet (Fin 8) :=
+  {{(0, true), (0, false), (1, true)}, {(0, true), (2, true), (3, true)},
+    {(0, true), (4, true), (5, true)}, {(0, true), (6, true), (7, true)}}
+
+example : Reduced tautRoot := by unfold Reduced; decide
+example : Choice θ tautRoot 3 {(0, true)} := by
+  apply choice_of_pairs
+  · unfold Heavy; decide
+  · decide
+  · decide
+
+example : ((countingIntro tautRoot 3 {(0, true)} true \ tautRoot).filter
+    fun C => C.card = 2).card = 4 := by decide
+example : ((countingChild tautRoot 3 {(0, true)} true).filter
+    fun C => C ∉ tautRoot ∧ C.card = 2).card = 3 := by decide
+example : ∃ C ∈ tautRoot, ∃ l ∈ C, Std.Sat.Literal.negate l ∈ C := by decide
+
+end ComplexityTests.SparsificationCountingDeletion