Unit insertion accounting for counting sparsification

The width-one base case of Appendix A.2–A.3 [OAI26c] counts actual first-insertion events, including the negated-heart units of the counting B-child. A unit persists because its only strict subclause is empty, and a legal step does not introduce an empty clause. Thus unit insertions increase the number of units without deleting earlier units; they cannot be charged twice.

This module does not establish the higher-width deletion recurrence, depth, leaf-count or native runtime bounds. The counting-tree construction is separate.

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro: the actual clauses added by a step.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingUnitInsertions: its new unit clauses.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.card_units_countingChild: one-step unit accounting.
• Cslib.Logic.PL.ClauseSet.Sparsification.sum_countingUnitInsertions_le: unit insertion budget.

def Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Bool → ClauseSet V

The heart in the A-child, or the petals together with every negated-heart unit in the B-child. This records the payload before reduction, including clauses already present in the parent.

def Cslib.Logic.PL.ClauseSet.Sparsification.countingUnitInsertions {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (b : Bool) : ClauseSet V

New width-one payload clauses, excluding those already present immediately before the step. Their cardinalities are insertion events; a later sum must not silently deduplicate events.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingChild_eq_reduce_union {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (b : Bool) : countingChild ψ c H b = reduce (ψ ∪ countingIntro ψ c H b)

Both counting children use the payload recorded for insertion accounting.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro_nonempty {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hH : 1 ≤ H.card) (hproper : H.card < c) {b : Bool} {C : Finset (Literal V)} (hC : C ∈ countingIntro ψ c H b) : C.Nonempty

Every payload clause in a proper nonempty-heart step is nonempty.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.empty_notMem_countingChild {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hψ : ∅ ∉ ψ) (hH : 1 ≤ H.card) (hproper : H.card < c) (b : Bool) : ∅ ∉ countingChild ψ c H b

A step cannot introduce an empty clause when none was present.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_countingChild_unit_iff {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hψ : ∅ ∉ ψ) (hH : 1 ≤ H.card) (hproper : H.card < c) (b : Bool) {C : Finset (Literal V)} (hC : C.card = 1) : C ∈ countingChild ψ c H b ↔ C ∈ ψ ∨ C ∈ countingIntro ψ c H b

Existing units persist, and every payload unit survives immediate reduction. No nontautology assumption is needed for this width-one fact.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.units_countingChild {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hψ : ∅ ∉ ψ) (hH : 1 ≤ H.card) (hproper : H.card < c) (b : Bool) : {C ∈ countingChild ψ c H b | C.card = 1} = {C ∈ ψ | C.card = 1} ∪ countingUnitInsertions ψ c H b

Units after a step are precisely the existing units plus its new unit insertion batch.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_units_countingChild {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hψ : ∅ ∉ ψ) (hH : 1 ≤ H.card) (hproper : H.card < c) (b : Bool) : {C ∈ countingChild ψ c H b | C.card = 1}.card = {C ∈ ψ | C.card = 1}.card + Finset.card (countingUnitInsertions ψ c H b)

A counting step increases the number of units by exactly its number of new payload units. In particular the added negated-heart units receive the same charge as all other unit insertions.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sum_countingUnitInsertions_add_card_units {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)) (hproper : ∀ i < N, 1 ≤ (H i).card ∧ (H i).card < c i) (hψ : ∅ ∉ ψ 0) : ∑ i ∈ Finset.range N, Finset.card (countingUnitInsertions (ψ i) (c i) (H i) (b i)) + {C ∈ ψ 0 | C.card = 1}.card = {C ∈ ψ N | C.card = 1}.card

Unit insertion events telescope exactly to the final number of units minus the initial units. The step and proper-heart premises refer to actual counting children, not a supplied bound.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sum_countingUnitInsertions_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) : ∑ i ∈ Finset.range N, Finset.card (countingUnitInsertions (ψ i) (c i) (H i) (b i)) ≤ 2 * declared.card

The width-one base case of Appendix A.3: actual unit insertion events along a finite path have total at most twice the number of declared variables. This charges heart units, petal units and negated-heart units together, and excludes all units already present in the root.

The path consists of actual counting children with heavy proper hearts. Reducedness is needed only at the root: if a legal first step exists, its nonempty flower rules out an empty root clause. No finite ambient variable type, nontautology or native construction-cost premise is used.