Charging deleted marked clauses to actual counting insertions

The deletion-charge argument of Appendix A.2, Lemma A.3 and (A.3) [OAI26c] 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.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_mem_counting_node_subset {V : Type u_1} [DecidableEq V] (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

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 Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_deleted_marked_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (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 : ℕ) : {C ∈ ψ m | C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)}.card ≤ ∑ i ∈ Finset.Ico 1 j, 2 * θ (j - i) * {D ∈ countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0) | D.card = i}.card

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.