Depth and Leaf-Count Bounds for Counting Sparsification

We connect the actual counting-path insertion and petal-step bounds of CountingPathBounds (Appendix A.2, Lemma A.3 on p. 46 and the path budgets of Appendix A.3 on p. 46 of [OAI26c]) to the prefix words of a CountingBranchingRule, and combine a leaf-only petal-step injection (a library adaptation of §A.3's depth-and-B-positions node encoding on p. 46) with the geometric binomial-tail bound Cslib.sum_choose_le_two_pow_div_add_one and the first-success threshold base countingThresholdBase of CountingParameters (pp. 46–47) to bound the number of leaf words of any counting-sparsification tree.

For a CountingBranchingRule (fun r => M ^ r) V σ starting from a state s whose clause set R.toClauseSet s is Reduced, nontautological, of width at most k, and supported on a finite variable set declared of size N = declared.card:

• every node word w has length at most countingDepthCoeff k M * N, where countingDepthCoeff k M = 4 * ∑ r < k - 1, (3 * M) ^ r;
• every node word w has M * #{i < w.length | w[i] = true} ≤ countingBChoiceCoeff k * N, where countingBChoiceCoeff k = 4 * ∑ r < k - 1, 3 ^ r;
• as a library adaptation of §A.3's (Cn + 1) * ∑ choose node bound (p. 46), leafhood rules out trailing-false ambiguity so two leaf words with true steps at the same positions are equal (CountingBranchingRule.IsLeafWord.eq_of_getD_eq); any finset W of leaf words therefore injects into the subsets of range (countingDepthCoeff k M * N) of cardinality at most countingBChoiceCoeff k * N / M without a separate depth factor, giving the pure binomial-sum leaf bound W.card ≤ ∑ j ≤ countingBChoiceCoeff k * N / M, (countingDepthCoeff k M * N).choose j (CountingBranchingRule.card_le_of_isLeafWord);
• under the integer parameter budget countingBChoiceCoeff k ≤ M and B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M (for 2 ≤ k, with 1 ≤ B), and in particular unconditionally at M = countingThresholdBase k B, W.card ≤ 2 ^ (N / B + 1) (CountingBranchingRule.card_le_two_pow_of_isLeafWord, CountingBranchingRule.card_le_two_pow_thresholdBase).

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.eq_of_getD_eq: two leaf words with true steps at the same positions are equal.
• Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.length_le, Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.length_le: linear depth bound along node and leaf words.
• Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.mul_card_le, Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.mul_card_le: M-scaled petal-step budget along node and leaf words.
• Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_of_isLeafWord: binomial-sum bound on any finset of leaf words.
• Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_of_isLeafWord, Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_thresholdBase: exponential bound 2 ^ (declared.card / B + 1) on any finset of leaf words under the integer parameter budget and at countingThresholdBase k B.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.2 (Lemma A.3, p. 46) and Appendix A.3 (pp. 46–47)

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff_eq_zero {k : ℕ} (hk : k ≤ 1) (M : ℕ) : countingDepthCoeff k M = 0

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingBChoiceCoeff_eq_zero {k : ℕ} (hk : k ≤ 1) : countingBChoiceCoeff k = 0

Prefix paths and leaf-count bounds for a counting branching rule

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.eq_of_getD_eq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} {s : σ} {w w' : List Bool} (hw : R.IsLeafWord s w) (hw' : R.IsLeafWord s w') (h : ∀ (i : ℕ), w.getD i false = w'.getD i false) : w = w'

Leaf words are determined by their petal steps. Two leaf words with true steps at the same positions are equal.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.exists_choice_seq_of_isNodeWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (s : σ) {w : List Bool} (hw : R.IsNodeWord s w) : ∃ (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)), (∀ i < w.length, R.toClauseSet (R.walk s (List.take (i + 1) w)) = countingChild (R.toClauseSet (R.walk s (List.take i w))) (c i) (H i) (w.getD i false)) ∧ ∀ i < w.length, Choice θ (R.toClauseSet (R.walk s (List.take i w))) (c i) (H i)

Every node word w of a counting branching rule induces a sequence of valid choices (c i, H i) along its prefixes w.take i.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.length_le {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {w : List Bool} (hw : R.IsNodeWord s w) : w.length ≤ countingDepthCoeff k M * declared.card

Node words are short. From a reduced, nontautological clause set of width ≤ k over declared, every node word has length at most countingDepthCoeff k M * declared.card.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.mul_card_le {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {w : List Bool} (hw : R.IsNodeWord s w) : M * {i ∈ Finset.range w.length | w.getD i false = true}.card ≤ countingBChoiceCoeff k * declared.card

Node words have few petal steps. From a reduced, nontautological clause set of width ≤ k over declared, every node word satisfies M * #{i < w.length | w.getD i false = true} ≤ countingBChoiceCoeff k * declared.card.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.length_le {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {w : List Bool} (hw : R.IsLeafWord s w) : w.length ≤ countingDepthCoeff k M * declared.card

Leaf words are short. From a reduced, nontautological clause set of width ≤ k over declared, every leaf word has length at most countingDepthCoeff k M * declared.card.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.mul_card_le {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {w : List Bool} (hw : R.IsLeafWord s w) : M * {i ∈ Finset.range w.length | w.getD i false = true}.card ≤ countingBChoiceCoeff k * declared.card

Leaf words have few petal steps. From a reduced, nontautological clause set of width ≤ k over declared, every leaf word satisfies M * #{i < w.length | w.getD i false = true} ≤ countingBChoiceCoeff k * declared.card.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_of_isLeafWord {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) : W.card ≤ ∑ j ∈ Finset.range (countingBChoiceCoeff k * declared.card / M + 1), (countingDepthCoeff k M * declared.card).choose j

Binomial-sum leaf-word bound. From a reduced, nontautological clause set of width ≤ k over declared, any finset W of leaf words has cardinality at most ∑_{j ≤ countingBChoiceCoeff k * declared.card / M} (countingDepthCoeff k M * declared.card).choose j.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_of_isLeafWord {V : Type u_1} [DecidableEq V] {σ : Type u_2} {M k : ℕ} (hM : 2 ≤ M) {R : CountingBranchingRule (fun (r : ℕ) => M ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {B : ℕ} (hB : 1 ≤ B) (hbudget : 2 ≤ k → countingBChoiceCoeff k ≤ M ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M) (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) : W.card ≤ 2 ^ (declared.card / B + 1)

Exponential leaf-word bound. Under the integer parameter budget countingBChoiceCoeff k ≤ M and B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M (for 2 ≤ k, with 1 ≤ B), any finset W of leaf words has cardinality at most 2 ^ (declared.card / B + 1).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_thresholdBase {V : Type u_1} [DecidableEq V] {σ : Type u_2} {k B : ℕ} (hB : 1 ≤ B) {R : CountingBranchingRule (fun (r : ℕ) => countingThresholdBase k B ^ r) V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) : W.card ≤ 2 ^ (declared.card / B + 1)

Unconditional exponential leaf-word bound at countingThresholdBase k B. For any 1 ≤ B and any counting branching rule R at M = countingThresholdBase k B, any finset W of leaf words from a reduced, nontautological clause set of width ≤ k over declared has cardinality at most 2 ^ (declared.card / B + 1).