From c3f01dce91baade960d152ed72976e0fb7826dcc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 00:16:56 -0400 Subject: [PATCH 1/2] feat(PolyTime): certify binary ceiling logarithms --- Complexity.lean | 1 + .../Complexity/PolyTime/Nat/BinaryLog.lean | 63 +++++++++++++++++++ ComplexityTests/BinaryClog.lean | 21 +++++++ 3 files changed, 85 insertions(+) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryLog.lean create mode 100644 ComplexityTests/BinaryClog.lean diff --git a/Complexity.lean b/Complexity.lean index d43d4cf127..a91cdc6e61 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1041,6 +1041,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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryLog.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryLog.lean new file mode 100644 index 0000000000..ec74d94176 --- /dev/null +++ b/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 diff --git a/ComplexityTests/BinaryClog.lean b/ComplexityTests/BinaryClog.lean new file mode 100644 index 0000000000..3f889c82aa --- /dev/null +++ b/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 From ffbc9bfbfb44b80b4138c157247d442ee03c0b96 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 00:21:52 -0400 Subject: [PATCH 2/2] feat(Sparsification): certify binary parameter selection cost --- Complexity.lean | 1 + .../CountingParametersPolyTime.lean | 159 ++++++++++++++++++ .../CountingParametersPolyTime.lean | 40 +++++ 3 files changed, 200 insertions(+) create mode 100644 Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParametersPolyTime.lean create mode 100644 ComplexityTests/CountingParametersPolyTime.lean diff --git a/Complexity.lean b/Complexity.lean index a91cdc6e61..b735125dfc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2220,6 +2220,7 @@ public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingD public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingInsertions 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.CountingSurvival public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTree public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingUnits diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParametersPolyTime.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParametersPolyTime.lean new file mode 100644 index 0000000000..e16e7b41b5 --- /dev/null +++ b/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 diff --git a/ComplexityTests/CountingParametersPolyTime.lean b/ComplexityTests/CountingParametersPolyTime.lean new file mode 100644 index 0000000000..ec426111e1 --- /dev/null +++ b/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