Marked clause occurrences in counting sparsification

Appendix A.2, Lemma A.2 [OAI26c] bounds the marked clauses still present at a node. A clause present in the root is excluded. This is distinct from the sum of insertion events in CountingUnits: a higher-width clause may later be deleted.

The minimum-width and maximum-heart priorities of Choice control the old clauses and the new petals, respectively. This follows the existing proof of Path.card_newContaining_lt Calabro, Lemma 5.9, applied directly to counting steps. The B-child's additional negated-heart units have width one and cannot enter the filter considered here, whose width is at least two. No decision-path Refines or tree-size theorem is transferred.

This present-clause upper bound requires positive thresholds and valid choices, but not root reducedness or nontautology. Those stronger conditions remain relevant to later immediate-survival and deletion-charge arguments. No higher-width insertion-event, depth, leaf or runtime bound is asserted here.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.card_lt_of_mem_countingIntro: payload widths decrease.
• Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_newContaining_lt: marked-present bound.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_lt_of_mem_countingIntro {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) {b : Bool} {C : Finset (Literal V)} (hC : C ∈ countingIntro ψ c H b) : C.card < c

Every counting payload clause is smaller than the selected width, including negated units.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_newContaining_lt {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)) {t j : ℕ} (ht : t ≤ N) {S : Finset (Literal V)} (hS : 1 ≤ S.card) (hSj : S.card < j) : {C ∈ ψ t | C ∉ ψ 0 ∧ C.card = j ∧ S ⊆ C}.card < 2 * θ (j - S.card)

At every prefix of an actual counting path, fewer than 2 * θ (j - |S|) root-absent clauses of width j containing a fixed nonempty proper literal set S are present.

The selected choices retain both priority conditions. The additional B-units are explicitly excluded using j ≥ 2. Root clauses remain excluded, and no ambient finite variable type or resource assumption is needed. This counts clauses currently present, not all insertion events.