First-success geometric thresholds for counting sparsification

For fixed width k ≥ 2 and inverse error budget B ≥ 1, Appendix A.3 of [OAI26c] tests dyadic threshold bases M in increasing order. The exact test is Γ ≤ M and B * Γ * ⌈log₂ (4 * C * M)⌉ ≤ M, where C = 4 ∑ r < k - 1, (3 * M) ^ r and Γ = 4 ∑ r < k - 1, 3 ^ r. countingThresholdBase implements this first-success search. The parameters depend only on k and B, before any input formula or variable budget.

An explicit successful candidate proves termination and the sharp bound M = O_k(B log(2B)); that candidate does not replace the first-success output. Widths zero and one have empty coefficient sums and use the separate default M = 2. The same total default is used at B = 0, which is outside the positive-error-budget specification.

This module proves numerical selection and size bounds, not a native bit-cost certificate, tree-word counting, or the complete counting sparsification theorem.

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff: the source coefficient C.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingBChoiceCoeff: the source coefficient Γ.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase: the first successful dyadic base.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff_le_mul_pow: the degree-k - 2 bound on the depth coefficient in terms of the threshold base.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_spec: the exact integer test.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_first: dyadic minimality.
• Cslib.Logic.PL.ClauseSet.Sparsification.exists_countingThresholdBase_le_mul_clog: the sharp size dependence on the inverse error budget.
• Cslib.Logic.PL.ClauseSet.Sparsification.isBigO_countingThresholdBase: the real logarithmic bound.
• Cslib.Logic.PL.ClauseSet.Sparsification.exists_clog_countingThresholdBase_le: a logarithmic bound on the number of dyadic candidates tested.
• Cslib.Logic.PL.ClauseSet.Sparsification.sum_choose_le_countingThresholdBase: the all-input-size numerical binomial-tail bound for the selected parameter.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.3, pp. 46–47

def Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff (k M : ℕ) : ℕ

The linear path-depth coefficient C in Appendix A.3.

def Cslib.Logic.PL.ClauseSet.Sparsification.countingBChoiceCoeff (k : ℕ) : ℕ

The coefficient Γ in the weighted B-choice bound of Appendix A.3.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.four_le_countingDepthCoeff {k M : ℕ} (hk : 2 ≤ k) : 4 ≤ countingDepthCoeff k M

The depth coefficient is at least four once width two is allowed.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.four_le_countingBChoiceCoeff {k : ℕ} (hk : 2 ≤ k) : 4 ≤ countingBChoiceCoeff k

The B-choice coefficient is at least four once width two is allowed.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff_le_mul_pow {k M : ℕ} (hM : 1 ≤ M) : countingDepthCoeff k M ≤ countingBChoiceCoeff k * M ^ (k - 2)

The geometric depth coefficient has degree at most k - 2 in a positive threshold base. The coefficient depends only on the fixed width, including the empty sums at widths zero and one.

@[reducible, inline]

abbrev Cslib.Logic.PL.ClauseSet.Sparsification.CountingExponentAccepts (k B m : ℕ) : Prop

Acceptance predicate for a candidate dyadic exponent m at width k and parameter B.

def Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase (k B : ℕ) : ℕ

The first dyadic M ≥ Γ passing Appendix A.3's exact test for error budget σ = 1/B. Widths at most one and the out-of-domain input B = 0 use the total default 2. The existence proof only bounds the search: Nat.find executes the decidable tests from exponent zero upward.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_spec {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) : countingBChoiceCoeff k ≤ countingThresholdBase k B ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (countingThresholdBase k B) * countingThresholdBase k B) ≤ countingThresholdBase k B

The selected dyadic base passes both exact integer tests.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_first {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) : ∃ (m : ℕ), countingThresholdBase k B = 2 ^ m ∧ ∀ j < m, ¬(countingBChoiceCoeff k ≤ 2 ^ j ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ j) * 2 ^ j) ≤ 2 ^ j)

The returned base is dyadic and every earlier power of two fails the exact test.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_eq_two_pow {k B m : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) (hpass : countingBChoiceCoeff k ≤ 2 ^ m ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤ 2 ^ m) (hfirst : ∀ j < m, ¬(countingBChoiceCoeff k ≤ 2 ^ j ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ j) * 2 ^ j) ≤ 2 ^ j)) : countingThresholdBase k B = 2 ^ m

A passing candidate with no earlier success computes the selected threshold base. This permits finite evaluation proofs without unfolding the termination argument of Nat.find.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_of_lt_two {k : ℕ} (hk : k < 2) (B : ℕ) : countingThresholdBase k B = 2

Widths zero and one use M = 2 separately from the geometric search.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_zero (k : ℕ) : countingThresholdBase k 0 = 2

The inverse error budget zero is outside the specification and uses the total default.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_countingThresholdBase_le_mul_clog {k : ℕ} (hk : 2 ≤ k) : ∃ (A : ℕ), ∀ (B : ℕ), 1 ≤ B → countingThresholdBase k B ≤ A * B * (Nat.clog 2 B + 1)

The first-success base has the sharp B log(2B) dependence. The constant depends only on the fixed width; the proof supplies the explicit constant 2 ^ (offset k + 2).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.isBigO_countingThresholdBase {k : ℕ} (hk : 2 ≤ k) : (fun (B : ℕ) => ↑(countingThresholdBase k B)) =O[Filter.atTop] fun (B : ℕ) => ↑B * Real.log (2 * ↑B)

For fixed width the first-success parameter is O(B log(2B)) as B tends to infinity.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_clog_countingThresholdBase_le {k : ℕ} (hk : 2 ≤ k) : ∃ (D : ℕ), ∀ (B : ℕ), 1 ≤ B → Nat.clog 2 (countingThresholdBase k B) ≤ D + 2 * Nat.clog 2 B

The selected exponent is at most D + 2 * ⌈log₂ B⌉, for a width-dependent constant D. Thus testing exponents from zero through the first success uses at most this bound plus one tests. This is a count of candidates, not a native bit-operation bound.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sum_choose_le_countingThresholdBase {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) (N : ℕ) : ∑ j ∈ Finset.range (countingBChoiceCoeff k * N / countingThresholdBase k B + 1), (countingDepthCoeff k (countingThresholdBase k B) * N).choose j ≤ 2 ^ (N / B + 1)

The selected geometric parameter gives the rounded binomial-tail bound for every variable budget N, including zero. This is only a numerical bound; counting tree words is separate.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.two_le_countingThresholdBase (k B : ℕ) : 2 ≤ countingThresholdBase k B

Every selected base, including the total defaults, is at least two.