Immediate survival in counting sparsification

Appendix A.1, Lemma A.1 [OAI26c] shows that the heart and petals are new and survive immediate reduction. For the B-child, nontautology prevents its additional negated-heart units from subsuming a petal. This module proves that fact for the actual countingChild, and preserves the pointwise absence of complementary literals along actual counting paths.

The local result needs only a heavy heart, positive thresholds and a reduced nontautological parent; neither priority in Choice is needed. At width at least two, the full counting payload consists of the heart or petals, so all its clauses survive and are absent from the current node. The root-subclause invariant additionally excludes the root along a path. The resulting equality identifies these insertion events with new clauses present in the next node. It does not sum events or prove the complete Appendix A.2 recurrence, depth, leaf count or native runtime.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_countingChild: preservation at one step.
• Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_counting_node: path preservation.
• Cslib.Logic.PL.ClauseSet.Sparsification.intro_subset_countingChild: heart and petal survival.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro_filter_eq_node_sdiff: higher-width insertion events are exactly the new marked clauses present in the next node.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.1, Lemma A.1

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_countingChild {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (r : ℕ), 1 ≤ θ r) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (h : Heavy θ ψ c H) (b : Bool) (C : Finset (Literal V)) : C ∈ countingChild ψ c H b → ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C

A proper heavy-heart step preserves the absence of complementary literals within each clause. This concerns clauses individually, not consistency between different unit clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_counting_node {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)) (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) {t : ℕ} (ht : t ≤ N) (C : Finset (Literal V)) : C ∈ ψ t → ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C

Nontautology at the root is preserved along actual counting children. There is no finite ambient variable type or satisfiability premise, and heaviness suffices in place of Choice.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.intro_subset_countingChild {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (r : ℕ), 1 ≤ θ r) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hred : Reduced ψ) (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (h : Heavy θ ψ c H) (b : Bool) : intro ψ c H b ⊆ countingChild ψ c H b

Every heart or petal survives immediate counting reduction. This includes unit petals but does not refer to the B-child's additional negated-heart units. Nontautology prevents those units from subsuming any petal.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.notMem_of_mem_intro {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (r : ℕ), 1 ≤ θ r) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hred : Reduced ψ) (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal V)} (ha : a ∈ intro ψ c H b) : a ∉ ψ

Every heart or petal is absent from a reduced parent. This newness fact does not require nontautology; the strict flower superset already rules out membership in the old antichain.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_intro_of_mem_countingIntro {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} {b : Bool} {a : Finset (Literal V)} (ha : a ∈ countingIntro ψ c H b) (ha2 : 2 ≤ a.card) : a ∈ intro ψ c H b

At width at least two, the counting payload contains only the heart or petals. The B-child's negated-heart units have width one and are excluded by this hypothesis.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro_filter_eq_node_sdiff {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)) (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) {m : ℕ} (hm : m < N) {j : ℕ} (hj : 2 ≤ j) : {x ∈ countingIntro (ψ m) (c m) (H m) (b m) | x.card = j} = {x ∈ ψ (m + 1) \ (ψ m ∪ ψ 0) | x.card = j}

Along an actual counting path, every width-j ≥ 2 payload clause survives and is absent from both the current node and the root. Thus its insertion event is exactly a new marked clause present in the next node. No survival or insertion-balance premise is assumed.