From b8f5317554f1a272d0e9663eec4f644ed2e957cc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 01:48:41 -0400 Subject: [PATCH] feat(fine-grained): bound scheduled counting depth uniformly --- Complexity.lean | 1 + .../FineGrained/CountingParameterBounds.lean | 128 ++++++++++++++++++ .../Sparsification/CountingParameters.lean | 9 +- ComplexityTests/CountingParameterBounds.lean | 94 +++++++++++++ 4 files changed, 230 insertions(+), 2 deletions(-) create mode 100644 Complexity/Computability/Complexity/FineGrained/CountingParameterBounds.lean create mode 100644 ComplexityTests/CountingParameterBounds.lean diff --git a/Complexity.lean b/Complexity.lean index 3b054d8c95..b84a0150f6 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/FineGrained/CountingParameterBounds.lean b/Complexity/Computability/Complexity/FineGrained/CountingParameterBounds.lean new file mode 100644 index 0000000000..67213f1461 --- /dev/null +++ b/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 diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean index 7a3ea6a09d..f52d9c4d64 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean +++ b/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 diff --git a/ComplexityTests/CountingParameterBounds.lean b/ComplexityTests/CountingParameterBounds.lean new file mode 100644 index 0000000000..2ccd121f95 --- /dev/null +++ b/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⟩