Cumulative counting-sparsification insertions

Appendix A.2, Lemma A.3 and equation (A.3) [OAI26c] bound actual insertion events along every path prefix. countingInsertionCount sums the new payload at each step, excluding clauses already in the current node or the root. It does not deduplicate events across steps or discard insertions whose clauses are later deleted.

For widths at least two, immediate survival gives the exact balance between cumulative insertions, present marked clauses and cumulative deletions. Summing the marked-occurrence bound over the two literals per declared variable bounds present clauses. Summing the one-step deletion charge then gives (A.3). Units are handled by the existing unit-event budget, including B-negated-heart units. No tree, potential, search algorithm, depth, leaf-count or native-resource result is asserted.

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount: cumulative insertion events.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_eq_present_add_deleted: exact higher-width event balance.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_one_le: unit-event budget.
• Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_marked_le: present-clause bound.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_rec: recurrence (A.3).
• Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_pow: Lemma A.3's closed bound.

References

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

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

The number of width-j insertion events in the first N steps. Each summand excludes both the current node and the initial root; a later deletion does not erase the earlier event.

@[simp]

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_zero {V : Type u_1} [DecidableEq V] (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) (j : ℕ) : countingInsertionCount 0 ψ c H b j = 0

The empty path prefix has no insertion events, regardless of its root.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.support_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)) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {t : ℕ} (ht : t ≤ N) (C : Finset (Literal V)) : C ∈ ψ t → ∀ l ∈ C, l.1 ∈ declared

Along actual heavy-heart counting steps, every literal remains on a declared root variable. This does not require a finite ambient variable type, reducedness or nontautology.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_one_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)) (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) : countingInsertionCount N ψ c H b 1 ≤ 2 * declared.card

Unit events, including the negated-heart units, have total at most two per declared variable. The root-excluding count is bounded by the existing current-excluding unit-event API.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_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)) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {t j : ℕ} (ht : t ≤ N) (hj : 2 ≤ j) : {C ∈ ψ t | C ∉ ψ 0 ∧ C.card = j}.card ≤ 4 * declared.card * θ (j - 1)

At any counting node, the present marked width-j ≥ 2 clauses number at most 4 * declared.card * θ (j - 1). Both Choice priorities are used by the occurrence supplier.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_eq_present_add_deleted {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) {j : ℕ} (hj : 2 ≤ j) : countingInsertionCount N ψ c H b j = {C ∈ ψ N | C ∉ ψ 0 ∧ C.card = j}.card + ∑ m ∈ Finset.range N, {C ∈ ψ m | C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)}.card

For widths at least two, insertion events telescope exactly into currently present marked clauses plus deletion events. Events are counted at their steps, without a no-reinsertion premise. Immediate survival and root exclusion are derived from the actual counting path.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sum_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)) (j : ℕ) : ∑ m ∈ Finset.range N, {C ∈ ψ m | C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)}.card ≤ 2 * ∑ i ∈ Finset.Ico 1 j, θ (j - i) * countingInsertionCount N ψ c H b i

Summing the actual one-step deletion charges gives the deletion term of (A.3). This part requires both Choice priorities and reducedness, but not nontautology.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_rec {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)) (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {j : ℕ} (hj : 2 ≤ j) : countingInsertionCount N ψ c H b j ≤ 4 * declared.card * θ (j - 1) + 2 * ∑ i ∈ Finset.Ico 1 j, θ (j - i) * countingInsertionCount N ψ c H b i

Equation (A.3) for actual cumulative insertion events along any legal counting-path prefix. The hypotheses assert actual steps, choices and root invariants; neither the balance nor its target bounds are assumptions. Units have the sharper bound countingInsertionCount_one_le.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_pow {V : Type u_1} [DecidableEq V] {M : ℕ} (hM : 2 ≤ M) (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 (fun (r : ℕ) => M ^ r) (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {j : ℕ} (hj : 1 ≤ j) : countingInsertionCount N ψ c H b j ≤ 4 * (3 * M) ^ (j - 1) * declared.card

Lemma A.3: for thresholds θ r = M ^ r, every path prefix has at most 4 * (3 * M) ^ (j - 1) * declared.card width-j insertion events. This holds for all j ≥ 1, in particular the manuscript's range 1 ≤ j < k for width-k roots. The proof does not divide by the declared-variable count, so it includes zero variables and zero-length prefixes.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_pow_of_card_le {V : Type u_1} [DecidableEq V] {M : ℕ} (hM : 2 ≤ M) (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 (fun (r : ℕ) => M ^ r) (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {n : ℕ} (hn : declared.card ≤ n) {j : ℕ} (hj : 1 ≤ j) : countingInsertionCount N ψ c H b j ≤ 4 * (3 * M) ^ (j - 1) * n

The closed insertion bound also holds for any declared-variable budget above the finite support's cardinality. No inhabitance or positivity of that budget is required.