feat(Sparsification): certify binary first-success parameter cost

Complexity.lean

@@ -1044,6 +1044,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Factorial
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Fin
@@ -2227,6 +2228,7 @@ public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingI
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingList
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPathBounds
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPolyTime
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryLog.lean

@@ -0,0 +1,63 @@
+/-
+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.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+public import Mathlib.Data.Nat.Log
+
+/-!
+# Polynomial-time binary ceiling logarithms
+
+The base-two ceiling logarithm of a binary natural is computed from its bit length and a
+comparison with the preceding power of two. The result is in unary, with length at most the
+binary input length. Zero and one both return zero. The ordinary polynomial-time certificate
+uses the existing binary size, power and comparison providers; it never expands the input
+natural into a unary word.
+
+## Main results
+
+* `Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two`: ceiling logarithm from binary
+  input to unary output.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM.ComputableInPolyTime
+
+private theorem clog_two_eq (n : ℕ) : Nat.clog 2 n =
+    if n ≤ 2 ^ (n.size - 1) then n.size - 1 else n.size := by
+  have hlo : n.size - 1 ≤ Nat.clog 2 n := by
+    have hs : n.size ≤ Nat.clog 2 n + 1 := Nat.size_le.mpr
+      ((Nat.le_pow_clog (by decide : 1 < 2) n).trans_lt (by
+        rw [pow_succ]
+        have := Nat.two_pow_pos (Nat.clog 2 n)
+        omega))
+    omega
+  have hhi : Nat.clog 2 n ≤ n.size := Nat.clog_le_of_le_pow (Nat.lt_size_self n).le
+  split
+  · rename_i h
+    exact Nat.le_antisymm (Nat.clog_le_of_le_pow h) hlo
+  · rename_i h
+    have := (Nat.lt_clog_iff_pow_lt (by decide : 1 < 2)).mpr (Nat.lt_of_not_ge h)
+    omega
+
+/-- Compute the base-two ceiling logarithm of a binary natural, returning a unary counter.
+The full input, intermediate power of two and output have polynomial bit cost. -/
+@[fun_prop]
+theorem binary_clog_two : ComputableInPolyTime (Nat.clog 2) encNat encUnary := by
+  have hp : ComputableInPolyTime (fun n : ℕ => n.size - 1) encNat encUnary :=
+    unary_sub.comp (binary_size.prod (const 1))
+  have htest := binary_le' (id' (encIn := encNat)) (binary_two_pow.comp hp)
+  convert htest.ite_decide hp binary_size using 1
+  exact funext clog_two_eq
+
+end Turing.MultiTapeTM.ComputableInPolyTime

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

@@ -0,0 +1,159 @@
+/-
+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.Logics.Propositional.ClauseSet.Sparsification.CountingParameters
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Mathlib.Algebra.Ring.GeomSum
+
+/-!
+# Binary bit cost of the first-success counting parameter
+
+For each fixed width `k`, the existing `countingThresholdBase k` has an ordinary polynomial-time
+native machine from binary inverse budget `B` to binary threshold base. The same machine works
+for every `B`, including zero. The width is fixed before the input, and is not a runtime unary
+parameter.
+
+The proof refines the selector to a bounded first-match scan through its proven logarithmic
+exponent bound. Only the exponent indices and logarithms are unary; the retained budget, powers
+of two, coefficient sums and integer-test operands remain binary. Existing plain providers charge
+the entire candidate-index list, captured input, arithmetic intermediates and final output. The
+scan may materialize the candidate list; no sharper polynomial degree or workspace claim is made.
+
+## Main results
+
+* `Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_countingThresholdBase`:
+  a uniform binary-input/output certificate for each fixed width.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.exists_length_countingThresholdBase_le`:
+  the full binary output length is linear in the binary input length, for width-dependent constants.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.3, pp. 46–47][OpenAI2026ETH]
+
+This is an implementation of the parameter-search bit-cost claim for `σ = 1/B`; it does not
+certify tree construction, a counting algorithm, general rational encodings or runtime width.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.ClauseSet.Sparsification
+
+open Finset Turing.MultiTapeTM Turing.MultiTapeTM.ComputableInPolyTime
+
+private abbrev Accepts (k B m : ℕ) : Prop :=
+  countingBChoiceCoeff k ≤ 2 ^ m ∧
+    B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤
+      2 ^ m
+
+private def firstExponent (k D B : ℕ) : ℕ :=
+  ((List.range (D + 2 * Nat.clog 2 B + 1)).filter (fun m => decide (Accepts k B m))).headD 0
+
+private def boundedBase (k D B : ℕ) : ℕ :=
+  if B = 0 then 2 else 2 ^ firstExponent k D B
+
+private theorem depthCoeff_polyTime (k : ℕ) :
+    ComputableInPolyTime (countingDepthCoeff k) encNat encNat := by
+  have hsum (n : ℕ) :
+      ComputableInPolyTime (fun M : ℕ => ∑ r ∈ range n, (3 * M) ^ r) encNat encNat := by
+    induction n with
+    | zero => simpa only [range_zero, sum_empty] using (const (encIn := encNat) 0)
+    | succ n ih =>
+      simpa only [geom_sum_succ, Function.comp_def] using
+        binary_add.comp ((binary_mul' (binary_mul' (const 3) id') ih).prod (const 1))
+  exact binary_mul' (const 4) (hsum (k - 1))
+
+private theorem accepts_polyTime (k : ℕ) :
+    ComputableInPolyTime (fun p : ℕ × ℕ => decide (Accepts k p.1 p.2))
+      (encPair encNat encUnary) encBool := by
+  have hB := fst encNat encUnary
+  have hM := binary_two_pow.comp (snd encNat encUnary)
+  have hC := (depthCoeff_polyTime k).comp hM
+  have hh := unary_to_binary.comp
+    (binary_clog_two.comp (binary_mul' (binary_mul' (const 4) hC) hM))
+  have hbudget := binary_le' (binary_mul' (binary_mul' hB (const (countingBChoiceCoeff k))) hh) hM
+  have hlarge := binary_le' (const (countingBChoiceCoeff k)) hM
+  simpa only [Accepts, Bool.decide_and, Function.comp_def] using
+    bool_and.comp (hlarge.prod hbudget)
+
+private theorem firstExponent_polyTime (k D : ℕ) :
+    ComputableInPolyTime (firstExponent k D) encNat encUnary := by
+  have hcount : ComputableInPolyTime (fun B : ℕ => D + 2 * Nat.clog 2 B + 1)
+      encNat encUnary :=
+    unary_add' (unary_add' (const D) (unary_mul' (const 2) binary_clog_two)) (const 1)
+  exact (headD (encA := encUnary) 0).comp
+    (filterWithInput (range.comp hcount) (accepts_polyTime k))
+
+private theorem boundedBase_polyTime (k D : ℕ) :
+    ComputableInPolyTime (boundedBase k D) encNat encNat := by
+  exact ((id' (encIn := encNat)).decide_eq' (const 0)).ite_decide (const 2)
+    (binary_two_pow.comp (firstExponent_polyTime k D))
+
+private theorem boundedBase_eq {k D : ℕ} (hk : 2 ≤ k)
+    (hD : ∀ B, 1 ≤ B → Nat.clog 2 (countingThresholdBase k B) ≤ D + 2 * Nat.clog 2 B)
+    (B : ℕ) : boundedBase k D B = countingThresholdBase k B := by
+  by_cases hB : B = 0
+  · simp [boundedBase, hB, countingThresholdBase_zero]
+  have hB' : 1 ≤ B := by omega
+  obtain ⟨m, hm, hfirst⟩ := countingThresholdBase_first hk hB'
+  have hmBound : m ≤ D + 2 * Nat.clog 2 B := by
+    have h := hD B hB'
+    simpa only [hm, Nat.clog_pow 2 m (by decide)] using h
+  have hpass : Accepts k B m := by
+    simpa only [Accepts, hm] using countingThresholdBase_spec hk hB'
+  have hfound : (List.range (D + 2 * Nat.clog 2 B + 1)).find?
+      (fun j => decide (Accepts k B j)) = some m := by
+    apply List.find?_range_eq_some.mpr
+    refine ⟨by simpa only [decide_eq_true_eq] using hpass, ?_, ?_⟩
+    · simpa only [List.mem_range] using Nat.lt_succ_of_le hmBound
+    · intro j hj
+      simpa only [Bool.not_eq_true', decide_eq_false_iff_not] using hfirst j hj
+  have hfirstEq : firstExponent k D B = m := by
+    simp only [firstExponent, List.headD_eq_head?_getD, List.head?_filter, hfound, Option.getD_some]
+  simp only [boundedBase, hB, ↓reduceIte, hfirstEq, hm]
+
+/-- For each fixed width, one native polynomial-time machine computes the unchanged first-success
+threshold from a binary inverse budget, returning the complete binary output. Widths zero and one
+and inverse budget zero use the existing total default. -/
+theorem computableInPolyTime_countingThresholdBase (k : ℕ) :
+    ComputableInPolyTime (countingThresholdBase k) encNat encNat := by
+  by_cases hk : 2 ≤ k
+  · obtain ⟨D, hD⟩ := exists_clog_countingThresholdBase_le hk
+    exact (boundedBase_polyTime k D).of_enc_eq fun B =>
+      congrArg encNat (boundedBase_eq hk hD B).symm
+  · convert (const (encIn := encNat) (encOut := encNat) 2) using 1
+    exact funext fun B => countingThresholdBase_of_lt_two (by omega) B
+
+/-- The complete binary output has a linear bit-length bound in the complete binary input.
+The additive constant depends only on the fixed width; all inverse budgets, including zero,
+are covered. -/
+theorem exists_length_countingThresholdBase_le (k : ℕ) :
+    ∃ D : ℕ, ∀ B : ℕ, (encNat (countingThresholdBase k B)).length ≤
+      D + 2 * (encNat B).length := by
+  by_cases hk : 2 ≤ k
+  · obtain ⟨D, hD⟩ := exists_clog_countingThresholdBase_le hk
+    refine ⟨D + 2, fun B => ?_⟩
+    by_cases hB : B = 0
+    · subst B
+      rw [countingThresholdBase_zero]
+      change 2 ≤ D + 2 + 2 * 0
+      omega
+    have hB' : 1 ≤ B := by omega
+    obtain ⟨m, hm, _⟩ := countingThresholdBase_first hk hB'
+    have hmBound := hD B hB'
+    have hclog : Nat.clog 2 B ≤ B.size := Nat.clog_le_of_le_pow (Nat.lt_size_self B).le
+    simp only [hm, Nat.clog_pow 2 m (by decide)] at hmBound
+    simp only [hm, encNat_apply, Nat.size_eq_bits_len, Nat.size_pow]
+    omega
+  · refine ⟨2, fun B => ?_⟩
+    rw [countingThresholdBase_of_lt_two (by omega)]
+    change 2 ≤ 2 + 2 * (encNat B).length
+    omega
+
+end Cslib.Logic.PL.ClauseSet.Sparsification

ComplexityTests/BinaryClog.lean

@@ -0,0 +1,21 @@
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog
+
+open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableInPolyTime
+
+-- Ceiling logarithms distinguish exact powers from their next integers and handle zero/one.
+/-- info: [0, 0, 1, 2, 2, 3, 3, 3, 3, 4] -/
+#guard_msgs in
+#eval (List.range 10).map (Nat.clog 2)
+
+example : Nat.clog 2 1024 = 10 ∧ Nat.clog 2 1025 = 11 ∧
+    (encNat 1024).length = 11 ∧ (encUnary (Nat.clog 2 1024)).length = 10 := by decide
+
+-- A caller can construct the next dyadic bound with a binary input and full binary output.
+example : ComputableInPolyTime (fun B : ℕ => 2 ^ Nat.clog 2 B) encNat encNat :=
+  binary_two_pow.comp binary_clog_two
+
+example : 2 ^ Nat.clog 2 3 = 4 ∧ 2 ^ Nat.clog 2 4 = 4 ∧
+    2 ^ Nat.clog 2 0 = 1 ∧ 2 ^ Nat.clog 2 1 = 1 := by decide
+
+-- Replacing the ceiling by the floor misses the first sufficient power at a non-power input.
+example : ¬ 3 ≤ 2 ^ Nat.log 2 3 ∧ 3 ≤ 2 ^ Nat.clog 2 3 := by decide

ComplexityTests/CountingParametersPolyTime.lean

@@ -0,0 +1,40 @@
+import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime
+
+open Cslib.Logic.PL.ClauseSet.Sparsification
+open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableInPolyTime
+
+-- An eleven-bit inverse budget produces the actual first successful parameter, whose entire
+-- output is encoded in binary. Width is fixed separately in each certificate.
+/-- info: [(131072, 18), (1048576, 21), (2, 2), (2, 2)] -/
+#guard_msgs in
+#eval [(2, 1024), (3, 1024), (1, 1024), (3, 0)].map fun (k, B) =>
+  let M := countingThresholdBase k B
+  (M, (encNat M).length)
+
+private theorem width_two_budget_1024 : countingThresholdBase 2 1024 = 131072 :=
+  countingThresholdBase_eq_two_pow (m := 17) (by decide) (by decide) (by decide) (by decide)
+
+example : (encNat 1024).length = 11 ∧
+    (encNat (countingThresholdBase 2 1024)).length = 18 := by
+  rw [width_two_budget_1024]
+  decide
+
+-- The preceding dyadic value satisfies M≥Γ but fails the exact integer stopping test.
+example : countingBChoiceCoeff 2 ≤ 65536 ∧
+    ¬ (1024 * countingBChoiceCoeff 2 *
+      Nat.clog 2 (4 * countingDepthCoeff 2 65536 * 65536) ≤ 65536) := by decide
+
+-- A binary-input caller computes its budget by multiplication and then invokes the selector.
+-- Both the original input and the computed budget retain binary encodings throughout.
+example : ComputableInPolyTime (fun B : ℕ => countingThresholdBase 3 (B * B))
+    encNat encNat :=
+  (computableInPolyTime_countingThresholdBase 3).comp (binary_mul' id' id')
+
+/-- info: 1048576 -/
+#guard_msgs in
+#eval countingThresholdBase 3 (32 * 32)
+
+-- Output is charged as a complete binary word, not as a constant-size numeric register.
+example : ¬ (encNat (countingThresholdBase 2 1024)).length ≤ 11 := by
+  rw [width_two_budget_1024]
+  decide