feat(fine-grained): bound scheduled counting depth uniformly

Complexity.lean

@@ -763,6 +763,7 @@ public import Complexity.Computability.Complexity.FineGrained
 public import Complexity.Computability.Complexity.FineGrained.Assignment
 public import Complexity.Computability.Complexity.FineGrained.BruteForce
 public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint
+public import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds
 public import Complexity.Computability.Complexity.FineGrained.CountingScale
 public import Complexity.Computability.Complexity.FineGrained.CountingSparsification
 public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch

Complexity/Computability/Complexity/FineGrained/CountingParameterBounds.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters
+import Mathlib.Tactic.IntervalCases
+
+/-!
+# Numerical depth bounds for the counting parameter schedule
+
+At the existing schedule `max 1 (ReplacementParams.numGroups N)`, the first-success dyadic
+base is at most `A * (Nat.clog 2 N + 1)` for one width-dependent constant `A`. Its geometric
+depth coefficient is therefore at most `D * (Nat.clog 2 N + 1) ^ (k - 2)`. Both constants are
+chosen before every `N`, including zero and the small sizes where the schedule is clamped to one.
+
+These are original all-input corollaries of the parameter estimates in Section 6.4 and
+Appendix A.3 of [OpenAI2026ETH], using the existing `numGroups_mul_clog_le_clog` estimate.
+They bound numerical values, independently of binary encoding lengths or parameter-computation
+cost. The final corollary charges an external unary declared size in a retained context/formula
+pair. No new schedule, traversal or native counting certificate is introduced.
+
+## Main results
+
+* `exists_countingThresholdBase_numGroups_le_clog`: one logarithmic numerical-base bound for all N.
+* `exists_countingDepthCoeff_numGroups_le_pow_clog`: one depth-coefficient bound with degree
+  `k - 2`.
+* `polyBounded_countingDepthCoeff_numGroups`: composition with a charged declared-size bound.
+* `polyBounded_countingDepthCoeff_numGroups_encPair`: the bound for a context, unary size
+  and input.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*, Section 6.4, pp. 43–44 and
+  Appendix A.3, pp. 46–47][OpenAI2026ETH]
+-/
+
+public section
+
+namespace Cslib.Complexity.SubexponentialSAT.SparseCountingScale
+
+open ReplacementParams Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM
+
+private theorem max_one_numGroups_mul_clog_le (n : ℕ) :
+    max 1 (numGroups n) * (Nat.clog 2 (max 1 (numGroups n)) + 1) ≤ Nat.clog 2 n + 1 := by
+  by_cases hn : 5 ≤ n
+  · by_cases hs : 1 ≤ numGroups n
+    · rw [max_eq_right hs]
+      calc numGroups n * (Nat.clog 2 (numGroups n) + 1)
+          ≤ numGroups n * (Nat.clog 2 (2 * numGroups n) + 1) :=
+            Nat.mul_le_mul_left _ (Nat.add_le_add_right
+              (Nat.clog_mono_right 2 (by omega)) 1)
+        _ ≤ Nat.clog 2 n := numGroups_mul_clog_le_clog hn
+        _ ≤ Nat.clog 2 n + 1 := Nat.le_succ _
+    · have hs0 : numGroups n = 0 := by omega
+      simp [hs0]
+  · have hn' : n < 5 := by omega
+    interval_cases n
+    · decide
+    · decide
+    · decide
+    · rw [show numGroups 3 = 1 from (numGroups_eq_iff (by decide)).mpr (by decide)]
+      decide
+    · rw [show numGroups 4 = 1 from (numGroups_eq_iff (by decide)).mpr (by decide)]
+      decide
+
+/-- For fixed width at least two, the same constant bounds the numerical first-success base
+at every declared size. The clamped schedule includes sizes where `numGroups` is zero. -/
+theorem exists_countingThresholdBase_numGroups_le_clog {k : ℕ} (hk : 2 ≤ k) :
+    ∃ A : ℕ, ∀ n : ℕ,
+      countingThresholdBase k (max 1 (numGroups n)) ≤ A * (Nat.clog 2 n + 1) := by
+  obtain ⟨A, hA⟩ := exists_countingThresholdBase_le_mul_clog hk
+  refine ⟨A, fun n => (hA _ (le_max_left _ _)).trans ?_⟩
+  rw [Nat.mul_assoc]
+  exact Nat.mul_le_mul_left A (max_one_numGroups_mul_clog_le n)
+
+/-- One constant and the fixed degree `k - 2` bound the numerical depth coefficient for all
+declared sizes. In particular, width two has degree zero. -/
+theorem exists_countingDepthCoeff_numGroups_le_pow_clog {k : ℕ} (hk : 2 ≤ k) :
+    ∃ D : ℕ, ∀ n : ℕ,
+      countingDepthCoeff k (countingThresholdBase k (max 1 (numGroups n))) ≤
+        D * (Nat.clog 2 n + 1) ^ (k - 2) := by
+  obtain ⟨A, hA⟩ := exists_countingThresholdBase_numGroups_le_clog hk
+  refine ⟨countingBChoiceCoeff k * A ^ (k - 2), fun n => ?_⟩
+  calc countingDepthCoeff k (countingThresholdBase k (max 1 (numGroups n)))
+      ≤ countingBChoiceCoeff k * countingThresholdBase k (max 1 (numGroups n)) ^ (k - 2) :=
+        countingDepthCoeff_le_mul_pow ((by decide : 1 ≤ 2).trans (two_le_countingThresholdBase _ _))
+    _ ≤ countingBChoiceCoeff k * (A * (Nat.clog 2 n + 1)) ^ (k - 2) :=
+        Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (hA n) _)
+    _ = (countingBChoiceCoeff k * A ^ (k - 2)) * (Nat.clog 2 n + 1) ^ (k - 2) := by
+        rw [Nat.mul_pow, Nat.mul_assoc]
+
+/-- A polynomial charge for the declared size supplies a uniform polynomial bound on the
+numerical depth coefficient. This is a growth statement, not a machine certificate. -/
+theorem polyBounded_countingDepthCoeff_numGroups {α : Type*} {size N : α → ℕ}
+    {k : ℕ} (hk : 2 ≤ k) (hN : PolyBounded size N) :
+    PolyBounded size (fun x =>
+      countingDepthCoeff k (countingThresholdBase k (max 1 (numGroups (N x))))) := by
+  obtain ⟨D, hD⟩ := exists_countingDepthCoeff_numGroups_le_pow_clog hk
+  have h : PolyBounded id (fun n =>
+      countingDepthCoeff k (countingThresholdBase k (max 1 (numGroups n)))) := by
+    refine PolyBounded.of_forall_le D (k - 2) fun n => (hD n).trans ?_
+    have hn : Nat.clog 2 n ≤ n := Nat.clog_le_of_le_pow n.lt_two_pow_self.le
+    exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (Nat.add_le_add_right hn 1) _)
+  exact h.comp hN
+
+/-- A retained context, external unary declared size and encoded input charge the numerical
+depth coefficient uniformly. The context and input encodings are arbitrary; the declared size
+is not replaced by the input's occurring support or its binary bit length. -/
+theorem polyBounded_countingDepthCoeff_numGroups_encPair {α β : Type}
+    (encC : α ↪ List Bool) (encInput : β ↪ List Bool) {k : ℕ} (hk : 2 ≤ k) :
+    PolyBounded (fun x : α × ℕ × β => (encPair encC (encPair encUnary encInput) x).length)
+      (fun x => countingDepthCoeff k (countingThresholdBase k (max 1 (numGroups x.2.1)))) := by
+  apply polyBounded_countingDepthCoeff_numGroups hk
+  apply PolyBounded.self.mono
+  intro x
+  simp only [length_encPair, encUnary_apply, List.length_replicate]
+  omega
+
+end Cslib.Complexity.SubexponentialSAT.SparseCountingScale

Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean

@@ -36,6 +36,8 @@ tree-word counting, or the complete counting sparsification theorem.
 
 ## 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`:
@@ -76,7 +78,9 @@ theorem four_le_countingBChoiceCoeff {k : ℕ} (hk : 2 ≤ k) : 4 ≤ countingBC
   simpa only [countingDepthCoeff, countingBChoiceCoeff, mul_one] using
     (four_le_countingDepthCoeff (M := 1) hk)
 
-private theorem depthCoeff_le {k M : ℕ} (hM : 1 ≤ M) :
+/-- 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. -/
+theorem countingDepthCoeff_le_mul_pow {k M : ℕ} (hM : 1 ≤ M) :
     countingDepthCoeff k M ≤ countingBChoiceCoeff k * M ^ (k - 2) := by
   calc countingDepthCoeff k M
       ≤ 4 * ∑ r ∈ range (k - 1), 3 ^ r * M ^ (k - 2) := by
@@ -108,7 +112,8 @@ private theorem clog_depthCoeff_le {k : ℕ} (hk : 2 ≤ k) (m : ℕ) :
   apply Nat.clog_le_of_le_pow
   calc 4 * countingDepthCoeff k (2 ^ m) * 2 ^ m
       ≤ 4 * (countingBChoiceCoeff k * (2 ^ m) ^ (k - 2)) * 2 ^ m :=
-        Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ (depthCoeff_le Nat.one_le_two_pow))
+        Nat.mul_le_mul_right _
+          (Nat.mul_le_mul_left _ (countingDepthCoeff_le_mul_pow Nat.one_le_two_pow))
     _ = (4 * countingBChoiceCoeff k) * (2 ^ m) ^ (k - 1) := by
       rw [show k - 1 = (k - 2) + 1 by omega, pow_succ]
       ring

ComplexityTests/CountingParameterBounds.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds
+import Complexity.Computability.Complexity.Problems.SAT
+
+/-! Concrete scheduled outputs, zero/low-width controls, a non-monotone schedule boundary,
+and numerical growth charged to the complete context/unary-size/CNF encoding. -/
+
+open Cslib.Complexity Cslib.Logic.PL Cslib.Logic.PL.ClauseSet.Sparsification
+open Cslib.Complexity.SubexponentialSAT.ReplacementParams
+open Cslib.Complexity.SubexponentialSAT.SparseCountingScale Turing.MultiTapeTM
+
+/-- info: [(1, 512, 6148), (1, 512, 6148), (1, 512, 6148), (1, 512, 6148), (1, 512, 6148),
+ (1, 512, 6148), (1, 512, 6148)] -/
+#guard_msgs (whitespace := lax) in
+#eval [0, 1, 2, 3, 4, 5, 20].map fun n =>
+  let b := max 1 (numGroups n)
+  let M := countingThresholdBase 3 b
+  (b, M, countingDepthCoeff 3 M)
+
+private theorem width_three_one : countingThresholdBase 3 1 = 512 :=
+  countingThresholdBase_eq_two_pow (m := 9) (by decide) (by decide) (by decide) (by decide)
+
+private theorem width_three_two : countingThresholdBase 3 2 = 1024 :=
+  countingThresholdBase_eq_two_pow (m := 10) (by decide) (by decide) (by decide) (by decide)
+
+-- The exported geometric estimate has a concrete positive client; positivity of M matters.
+example : countingDepthCoeff 3 512 ≤ 8192 ∧
+    ¬ countingDepthCoeff 3 0 ≤ countingBChoiceCoeff 3 * 0 ^ (3 - 2) := by
+  constructor
+  · exact countingDepthCoeff_le_mul_pow (by decide : 1 ≤ 512)
+  · decide
+
+-- One constant covers every size, including the positive coefficient at N = 0.
+example : ∃ D : ℕ, 6148 ≤ D ∧ ∀ n : ℕ,
+    countingDepthCoeff 3 (countingThresholdBase 3 (max 1 (numGroups n))) ≤
+      D * (Nat.clog 2 n + 1) := by
+  obtain ⟨D, hD⟩ := exists_countingDepthCoeff_numGroups_le_pow_clog (k := 3) (by decide)
+  have hzero := hD 0
+  norm_num [numGroups, width_three_one, countingDepthCoeff, Finset.sum_range_succ] at hzero
+  refine ⟨D, hzero, fun n => ?_⟩
+  simpa only [Nat.reduceSub, pow_one] using hD n
+
+-- Omitting the additive one would make the all-N claim false at zero for every constant.
+example (D : ℕ) : ¬ countingDepthCoeff 3
+    (countingThresholdBase 3 (max 1 (numGroups 0))) ≤ D * Nat.clog 2 0 := by
+  norm_num [numGroups, width_three_one, countingDepthCoeff, Finset.sum_range_succ]
+
+-- Width two really has degree zero; widths zero and one have empty coefficient sums.
+example (n : ℕ) :
+    countingDepthCoeff 2 (countingThresholdBase 2 (max 1 (numGroups n))) = 4 ∧
+    countingDepthCoeff 1 (countingThresholdBase 1 (max 1 (numGroups n))) = 0 ∧
+    countingDepthCoeff 0 (countingThresholdBase 0 (max 1 (numGroups n))) = 0 := by
+  simp [countingDepthCoeff]
+
+-- Reuse the schedule's integer characterization at its downward jump. No monotonicity in N
+-- is required by the uniform bound, and the selected base changes with the positive budget.
+example :
+    countingDepthCoeff 3 (countingThresholdBase 3 (max 1 (numGroups (2 ^ 524288)))) = 12292 ∧
+    countingDepthCoeff 3 (countingThresholdBase 3 (max 1 (numGroups (2 ^ 524289)))) = 6148 := by
+  have hfirst : numGroups (2 ^ 524288) = 2 := by
+    apply (numGroups_eq_iff ?_).mpr <;> (rw [Nat.clog_pow 2 _ one_lt_two]; decide)
+  have hnext : numGroups (2 ^ 524289) = 1 := by
+    apply (numGroups_eq_iff ?_).mpr <;> (rw [Nat.clog_pow 2 _ one_lt_two]; decide)
+  rw [hfirst, hnext]
+  norm_num [width_three_one, width_three_two, countingDepthCoeff,
+    Finset.sum_range_succ]
+
+-- A size function that itself grows quadratically can be composed through the generic API.
+example : ∃ c d : ℕ, 6148 ≤ c ∧ ∀ n : ℕ,
+    countingDepthCoeff 3
+      (countingThresholdBase 3 (max 1 (numGroups ((n + 1) ^ 2)))) ≤ c * (n + 1) ^ d := by
+  have hN : PolyBounded id (fun n : ℕ => (n + 1) ^ 2) :=
+    PolyBounded.of_forall_le 1 2 (fun _ => by simp)
+  obtain ⟨c, d, h⟩ := (polyBounded_countingDepthCoeff_numGroups (k := 3) (by decide) hN).exists_le
+  have hzero := h 0
+  norm_num [numGroups, width_three_one, countingDepthCoeff, Finset.sum_range_succ] at hzero
+  exact ⟨c, d, hzero, h⟩
+
+-- The same polynomial covers all contexts, declared sizes and formulas. Empty formulas at
+-- N = 0 and N = 3 have different full input lengths, despite identical occurring support.
+example : ∃ c d : ℕ,
+    (∀ x : Bool × ℕ × CNF ℕ,
+      countingDepthCoeff 3 (countingThresholdBase 3 (max 1 (numGroups x.2.1))) ≤
+        c * ((encPair encBool (encPair encUnary encCNF) x).length + 1) ^ d) ∧
+    (encPair encBool (encPair encUnary encCNF) (true, 0, [])).length = 4 ∧
+    (encPair encBool (encPair encUnary encCNF) (false, 3, [])).length = 10 := by
+  obtain ⟨c, d, h⟩ :=
+    (polyBounded_countingDepthCoeff_numGroups_encPair encBool encCNF (k := 3) (by decide)).exists_le
+  exact ⟨c, d, h, by decide, by decide⟩