Depth and B-choice budgets for actual counting paths

Appendix A.3 [OAI26c], printed p.46, obtains depth C * n and at most Γ * n / M B-choices from actual insertion events, where C = 4 * ∑ r < k - 1, (3 * M) ^ r and Γ = 4 * ∑ r < k - 1, 3 ^ r. Here the B-budget is stated as M * #B ≤ Γ * n, without division.

Every step inserts a genuinely new heart or petal of width between one and k - 1; every B-step of petal width j inserts at least M ^ j such clauses. Summing these lower bounds against the cumulative insertion bounds proves both budgets. There is no replacement by distinct-clause counts and no assumed path-length bound. The empty sums at k ≤ 1 force zero steps. No ambient finite variable type or positivity of the declared-variable count is needed.

The input is the existing Nat-indexed actual counting path. Tree/search clients can obtain it from successive word prefixes and their branching rule's choice witnesses. Node/leaf-word counting, effective parameter selection and native resource bounds remain separate consumer obligations.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.card_le_counting_node: root width is preserved.
• Cslib.Logic.PL.ClauseSet.Sparsification.counting_new_nonempty: every step inserts a new clause.
• Cslib.Logic.PL.ClauseSet.Sparsification.counting_length_le_sum_insertions: depth lower charge.
• Cslib.Logic.PL.ClauseSet.Sparsification.mul_card_counting_petalSteps_le: B-step lower charge.
• Cslib.Logic.PL.ClauseSet.Sparsification.counting_length_le: the C * n depth bound.
• Cslib.Logic.PL.ClauseSet.Sparsification.mul_card_counting_B_le: the Γ * n weighted B-budget.
• Cslib.Logic.PL.ClauseSet.Sparsification.counting_path_budgets_of_card_le: declared-budget form.

References

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_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)) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) {t : ℕ} (ht : t ≤ N) (C : Finset (Literal V)) : C ∈ ψ t → C.card ≤ k

All clauses along an actual heavy-heart counting path retain the root width bound. The payload-width theorem includes the additional negated-heart units.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.counting_selected_width_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)) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) {m : ℕ} (hm : m < N) : c m ≤ k

Every selected width is at most the root width bound.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.intro_subset_counting_new {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)) {m : ℕ} (hm : m < N) : intro (ψ m) (c m) (H m) (b m) ⊆ countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0)

Every heart/petal is genuinely new, including width-one petals. This excludes the current node and root using reducedness and root-subclause witnesses, without nontautology.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.counting_new_nonempty {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)) {m : ℕ} (hm : m < N) : Finset.Nonempty (countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0))

Every legal counting step has at least one insertion absent from current and root. The witness is a heart or petal, so already-present B-negated units do not affect this fact.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_mem_Ico_of_mem_countingIntro {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)) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) {m : ℕ} (hm : m < N) {C : Finset (Literal V)} (hC : C ∈ countingIntro (ψ m) (c m) (H m) (b m)) : C.card ∈ Finset.Ico 1 k

Every actual payload width lies in [1,k), where k bounds the root widths.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.counting_length_le_sum_insertions {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)) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) : N ≤ ∑ j ∈ Finset.Ico 1 k, countingInsertionCount N ψ c H b j

Charging each step to its nonempty insertion batch bounds path length by the sum of width-indexed event counts. No deduplication across steps or terminal-sparsity premise is used.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mul_card_counting_petalSteps_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)) (j : ℕ) : θ j * {m ∈ Finset.range N | b m = true ∧ c m - (H m).card = j}.card ≤ countingInsertionCount N ψ c H b j

A B-step of petal width j inserts at least θ j new width-j clauses. Summing these per-step contributions gives a lower bound on actual cumulative insertion events, including j=1.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.counting_length_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) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) : N ≤ (4 * ∑ r ∈ Finset.range (k - 1), (3 * M) ^ r) * declared.card

Actual counting paths have depth at most C * declared.card, with the source's C = 4 * ∑ r < k - 1, (3 * M) ^ r. At k ≤ 1 the empty sum forces zero steps.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mul_card_counting_petalSteps_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) : M * {m ∈ Finset.range N | b m = true ∧ c m - (H m).card = j}.card ≤ 4 * 3 ^ (j - 1) * declared.card

At each fixed petal width, the B-step budget keeps one factor of M after canceling a positive power of M. There is no division by the number of declared variables.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mul_card_counting_B_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) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) : M * {m ∈ Finset.range N | b m = true}.card ≤ (4 * ∑ r ∈ Finset.range (k - 1), 3 ^ r) * declared.card

The source's weighted B-choice budget: M * #B ≤ Γ * declared.card, where Γ = 4 * ∑ r < k - 1, 3 ^ r. This includes k ≤ 1 and zero declared variables.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.counting_path_budgets_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) {k : ℕ} (hk : ∀ C ∈ ψ 0, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {n : ℕ} (hn : declared.card ≤ n) : N ≤ (4 * ∑ r ∈ Finset.range (k - 1), (3 * M) ^ r) * n ∧ M * {m ∈ Finset.range N | b m = true}.card ≤ (4 * ∑ r ∈ Finset.range (k - 1), 3 ^ r) * n

Both actual path budgets hold for any declared-variable budget above the finite support's cardinality, including zero. The B-budget retains the source's exact coefficient Γ.