From 3740f46f127e9c18bd7b26e7f0309d3cd59d039f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 09:40:37 -0400 Subject: [PATCH 1/3] =?UTF-8?q?feat(CountingSimulation):=20unconditional?= =?UTF-8?q?=20SharpTIME=20=E2=8A=86=20FTIME=20in=20time=202^O(T/=E2=88=9Al?= =?UTF-8?q?og=20T)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Instantiate the count-first containments of #2003 with `fastContractionAlgorithm`, as FastSimulation already does for NTIME, BPTIME and PPTIME: * `SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two` * `exists_computableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_SharpTIME` Check both at the clock `(n + 1) ^ 2 + 1`, and drop the completed ROADMAP item for #1833. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../CountingSimulation/FastSimulation.lean | 28 +++++++++++++++++-- ComplexityTests/FastSimulation.lean | 19 ++++++++++++- ROADMAP.md | 5 ---- 3 files changed, 44 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean index 9e5d30b25..7b121db8c 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean @@ -11,16 +11,21 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Blo public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves /-! -# Nondeterministic and probabilistic time in time `2 ^ O(T / √log T)` and polynomial space +# Counting, nondeterministic and probabilistic time in time `2 ^ O(T / √log T)` and polynomial space The class containments of `Cslib.Complexity.CountingSimulation.BlockNetworks`, with the contraction algorithm of Theorem D.1 of [OpenAI2026ETH] (`CountingSimulation.fastContractionAlgorithm`) in place of their hypothesis. These are the containments of #1833: for time-constructible `T` with -`max n 2 ≤ T n`, every problem in `NTIME[T]`, `BPTIME[T]` or `PPTIME[T]` is decided by one +`max n 2 ≤ T n`, every counting function in `SharpTIME[T]` is computed, with its exact value in +binary, and every problem in `NTIME[T]`, `BPTIME[T]` or `PPTIME[T]` is decided, by one deterministic machine in time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`. ## Main results +* `Cslib.Complexity.CountingSimulation.SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two`: + exact terminal counting with binary output. +* `exists_computableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_SharpTIME`: its joint time and + space bound. * `Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`, `BPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`, `PPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`: the class containments. @@ -42,6 +47,17 @@ open Turing.MultiTapeTM variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} +/-- **Exact terminal counting in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** One deterministic +machine computes each function in `SharpTIME[T]`, writing the exact count in binary. -/ +theorem exists_computableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_SharpTIME + (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {f : α → ℕ} + (hf : f ∈ SharpTIME enc T) : + ∃ C d : ℕ, ComputableInTimeAndSpace f enc encNat + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := + exists_computableInTimeAndSpace_of_mem_SharpTIME_of_contractionAlgorithm fastContractionAlgorithm + hT hTn hf + /-- **Nondeterministic time `T` in time `2 ^ O(T / √log T)` and space `T ^ O(1)`.** -/ theorem exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_NTIME (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ NTIME enc T) : @@ -70,6 +86,14 @@ theorem exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_PPTIME exists_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm fastContractionAlgorithm hT hTn hL +/-- **`SharpTIME[T] ⊆ ⋃ C, FTIME[2 ^ (C T / √⌊log₂ T⌋)]`**, with the exact count in binary, for +time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + SharpTIME enc T ⊆ ⋃ C : ℕ, + FTIME enc encNat (fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))) := + SharpTIME_subset_iUnion_FTIME_of_contractionAlgorithm fastContractionAlgorithm hT hTn + /-- **`NTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ theorem NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) diff --git a/ComplexityTests/FastSimulation.lean b/ComplexityTests/FastSimulation.lean index 5f090f964..2c203d66c 100644 --- a/ComplexityTests/FastSimulation.lean +++ b/ComplexityTests/FastSimulation.lean @@ -7,7 +7,8 @@ Authors: Samuel Schlesinger import Complexity.Computability.Complexity.Classes.CountingSimulation.FastSimulation import Complexity.Computability.Complexity.Classes.Constructible.Log -/-! # Nondeterministic and probabilistic time in time `2 ^ O(T / √log T)`: checked instances +/-! # Counting, nondeterministic and probabilistic time in time `2 ^ O(T / √log T)`: checked +instances The class containments at the clock `T n = (n + 1) ^ 2 + 1`, which is time-constructible and at least `max n 2`. -/ @@ -27,6 +28,22 @@ theorem timeConstructible_succ_sq_add_one : TimeConstructible fun n => (n + 1) ^ theorem max_le_succ_sq_add_one (n : ℕ) : max n 2 ≤ (n + 1) ^ 2 + 1 := max_le (by nlinarith) (by have := Nat.one_le_pow 2 (n + 1) (Nat.succ_pos n); omega) +example {α : Type} {enc : α ↪ List Bool} : + SharpTIME enc (fun n => (n + 1) ^ 2 + 1) ⊆ ⋃ C : ℕ, FTIME enc encNat fun n => + 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := + SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two timeConstructible_succ_sq_add_one + max_le_succ_sq_add_one + +-- One machine within both bounds, writing the exact count in binary. +example {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} + (hf : f ∈ SharpTIME enc fun n => (n + 1) ^ 2 + 1) : + ∃ C d : ℕ, ComputableInTimeAndSpace f enc encNat + (fun a => 2 ^ (C * (((enc a).length + 1) ^ 2 + 1) / + Nat.sqrt (Nat.log 2 (((enc a).length + 1) ^ 2 + 1)))) + (fun a => (((enc a).length + 1) ^ 2 + 1) ^ d) := + exists_computableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_SharpTIME + timeConstructible_succ_sq_add_one max_le_succ_sq_add_one hf + example {α : Type} {enc : α ↪ List Bool} : NTIME enc (fun n => (n + 1) ^ 2 + 1) ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := diff --git a/ROADMAP.md b/ROADMAP.md index e0cdaa32f..70bc1170d 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -235,11 +235,6 @@ index links to canonical definitions rather than keeping a second set. ### Counting and modular classes -- Complete the unconditional `SharpTIME(T)` to binary-output `FTIME(2^{O(T/√log T)})` - endpoint in [#1833](https://github.com/cslib-community/complexitylib/issues/1833). The native - terminal-path class agrees with `SharpP` at polynomial clocks; the count-first simulation - supplies joint time and polynomial workspace conditional on the explicit-network contraction - algorithm. Integration of the concrete contraction removes that remaining premise. - The Another Solution Problem (ASP) framework: certify polynomial-time forward and inverse witness maps. The parsimonious reductions to positive exact-one SAT and its planar three-occurrence variants already preserve counts over occurring variables; the new local From f6d28d6b681e91332164da28283ff5a17cbef960 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:06:17 -0400 Subject: [PATCH 2/3] =?UTF-8?q?feat(CountingSimulation):=20counting=20clas?= =?UTF-8?q?ses=20from=20#TIME=20and=20NTIME/BPTIME/PPTIME=20=E2=8A=8A=20DT?= =?UTF-8?q?IME[2^T]=20(#2050)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add ParityTIME, ModTIME k and CeqTIME as predicates on SharpTIME counts, with polynomial-time unions ParityP, ModP k and CeqP. Derive their containments in ⋃ C, DTIME[2^(C T/√⌊log₂ T⌋)] from SharpTIME ⊆ FTIME (#2041) through a polynomial-time postprocessing lemma for FTIME, and prove one strict containment in DTIME[2^T] for every class decided by tests of two SharpTIME counts. The separating language is the clocked diagonal with the new time-constructible clock 2^(T n / 4). NTIME, BPTIME and PPTIME get the same strict containment through their existing containments. Proposed by coordinator-claude-e6cf7b0d and selected by Samuel. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 6 + .../Complexity/Classes/CeqP/Time.lean | 82 ++++++++ .../Classes/Constructible/TwoPow.lean | 66 ++++++ .../CountingSimulation/CountingClasses.lean | 197 ++++++++++++++++++ .../CountingSimulation/Separation.lean | 180 ++++++++++++++++ .../Classes/FunctionTime/Decide.lean | 91 ++++++++ .../Complexity/Classes/ModP/Time.lean | 98 +++++++++ .../Complexity/Classes/SharpP/Time.lean | 17 ++ ComplexityTests/CountingSeparation.lean | 101 +++++++++ 9 files changed, 838 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/CeqP/Time.lean create mode 100644 Complexity/Computability/Complexity/Classes/Constructible/TwoPow.lean create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean create mode 100644 Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean create mode 100644 Complexity/Computability/Complexity/Classes/ModP/Time.lean create mode 100644 ComplexityTests/CountingSeparation.lean diff --git a/Complexity.lean b/Complexity.lean index 6d336ab1d..f021d1b23 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1150,8 +1150,10 @@ public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Closu public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.Kadin public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.PH public import Complexity.Computability.Complexity.Classes.CeqP +public import Complexity.Computability.Complexity.Classes.CeqP.Time public import Complexity.Computability.Complexity.Classes.Constructible public import Complexity.Computability.Complexity.Classes.Constructible.Log +public import Complexity.Computability.Complexity.Classes.Constructible.TwoPow public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace public import Complexity.Computability.Complexity.Classes.Counting.Space public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate @@ -1160,17 +1162,20 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Ass public import Complexity.Computability.Complexity.Classes.CountingSimulation.BlockNetworks public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments public import Complexity.Computability.Complexity.Classes.CountingSimulation.Count +public import Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAlgorithm public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastAnalysis public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastSimulation public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Separation public import Complexity.Computability.Complexity.Classes.DP public import Complexity.Computability.Complexity.Classes.EXP public import Complexity.Computability.Complexity.Classes.FewP public import Complexity.Computability.Complexity.Classes.FewP.Machine public import Complexity.Computability.Complexity.Classes.FunctionTime +public import Complexity.Computability.Complexity.Classes.FunctionTime.Decide public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.LogClock public import Complexity.Computability.Complexity.Classes.Hierarchy.Nondeterministic @@ -1226,6 +1231,7 @@ public import Complexity.Computability.Complexity.Classes.MIP.NEXP public import Complexity.Computability.Complexity.Classes.MIP.OptimalProver public import Complexity.Computability.Complexity.Classes.ModP public import Complexity.Computability.Complexity.Classes.ModP.GapP +public import Complexity.Computability.Complexity.Classes.ModP.Time public import Complexity.Computability.Complexity.Classes.NP public import Complexity.Computability.Complexity.Classes.NP.Closure public import Complexity.Computability.Complexity.Classes.NP.GuessVerify diff --git a/Complexity/Computability/Complexity/Classes/CeqP/Time.lean b/Complexity/Computability/Complexity/Classes/CeqP/Time.lean new file mode 100644 index 000000000..0f9878cae --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CeqP/Time.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.CeqP +public import Complexity.Computability.Complexity.Classes.SharpP.Time + +/-! +# Time-bounded exact counting + +`Cslib.Complexity.CeqTIME enc t` is a time-parameterized counterpart of `Cslib.Complexity.CeqP`. +Its members are the problems decided by equality of two counts in +`Cslib.Complexity.SharpTIME enc t`. Each count is the number of accepting terminal branches of a +fixed nonblocking native counting machine whose branches all halt within time `O(t n)`. This +follows the two-count characterization of `C=P` +(`Cslib.Complexity.mem_CeqP_iff_exists_SharpP`). + +At polynomial clocks this is `CeqP`: `Cslib.Complexity.mem_CeqP_iff_exists_mem_CeqTIME`, by the +equality of `Cslib.Complexity.SharpP` with the union of the classes `SharpTIME (n ^ d)`. The two +counts may first need different polynomial clocks; constant factors are absorbed, so the larger +clock serves both (`Cslib.Complexity.SharpTIME_mono_of_le_mul_add`). + +## Main definitions + +* `Cslib.Complexity.CeqTIME`: equality of two terminal-path counts within time `O(t n)`. + +## Main results + +* `Cslib.Complexity.CeqTIME_mono`: monotonicity in the clock. +* `Cslib.Complexity.mem_CeqP_iff_exists_mem_CeqTIME`: `C=P` is the union of the classes + `CeqTIME (n ^ d)`. + +## References + +* [S. Fenner, L. Fortnow, S. Kurtz, *Gap-definable counting classes*][FennerFortnowKurtz1994] +* [L. Fortnow, *Counting Complexity*][Fortnow1997] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} + +/-- `C₌TIME[t]`: the problems whose members are the instances where two counts in +`SharpTIME enc t` agree. -/ +def CeqTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := + {A | ∃ f ∈ SharpTIME enc t, ∃ g ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ f a = g a} + +/-- `CeqTIME` is monotone in the clock. -/ +theorem CeqTIME_mono {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : + CeqTIME enc t₁ ⊆ CeqTIME enc t₂ := fun _ ⟨f, hf, g, hg, hA⟩ => + ⟨f, SharpTIME_mono h hf, g, SharpTIME_mono h hg, hA⟩ + +/-- A smaller polynomial degree gives a smaller `SharpTIME` class: `n ^ d ≤ n ^ D + 1`. -/ +private theorem SharpTIME_pow_subset {d D : ℕ} (h : d ≤ D) : + SharpTIME enc (· ^ d) ⊆ SharpTIME enc (· ^ D) := + SharpTIME_mono_of_le_mul_add (C := 1) fun n => by + rcases Nat.eq_zero_or_pos n with rfl | hn + · rcases Nat.eq_zero_or_pos d with rfl | hd + · simp + · simp [Nat.zero_pow hd] + · simpa only [one_mul] using (Nat.pow_le_pow_right hn h).trans (Nat.le_succ _) + +/-- **`C=P` is the union of the classes `CeqTIME (n ^ d)`.** -/ +theorem mem_CeqP_iff_exists_mem_CeqTIME : A ∈ CeqP enc ↔ ∃ d, A ∈ CeqTIME enc (· ^ d) := by + rw [mem_CeqP_iff_exists_SharpP] + constructor + · rintro ⟨f, hf, g, hg, hA⟩ + obtain ⟨d₁, hd₁⟩ := mem_SharpP_iff_exists_mem_SharpTIME.mp hf + obtain ⟨d₂, hd₂⟩ := mem_SharpP_iff_exists_mem_SharpTIME.mp hg + exact ⟨max d₁ d₂, f, SharpTIME_pow_subset (le_max_left _ _) hd₁, + g, SharpTIME_pow_subset (le_max_right _ _) hd₂, hA⟩ + · rintro ⟨d, f, hf, g, hg, hA⟩ + exact ⟨f, SharpTIME.subset_SharpP d hf, g, SharpTIME.subset_SharpP d hg, hA⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Constructible/TwoPow.lean b/Complexity/Computability/Complexity/Classes/Constructible/TwoPow.lean new file mode 100644 index 000000000..9477b7e2f --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Constructible/TwoPow.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.NatPolynomial +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# Exponentials of constructible clocks + +If `T` is time-constructible, so is `n ↦ 2 ^ (T n / k)` for every `k ≥ 1`. The machine computes +`T n` in binary within `O(T n)` steps and divides it by `k`. It then counts the quotient `m` down +to unary within `O((m + 1) ^ 2)` steps (`Turing.MultiTapeTM.ComputableInO.natToUnary`) and writes +`2 ^ m` in binary, as `m` zeros followed by a one. Since `T n < k * (m + 1)`, every stage is +polynomial in `m`, hence `O(2 ^ m)`. + +Such clocks separate time classes at exponential scale. The clocked diagonal with clock +`2 ^ (T n / 4)` is decidable within time `O(2 ^ T n)`, which separates `DTIME[2 ^ T]` from the +classes of the counting simulation in `CountingSimulation.Separation`. + +## Main results + +* `Cslib.Complexity.TimeConstructible.two_pow_div`: `n ↦ 2 ^ (T n / k)` is time-constructible. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +/-- **Exponentials of constructible clocks.** If `T` is time-constructible and `0 < k`, then so +is `n ↦ 2 ^ (T n / k)`. -/ +theorem TimeConstructible.two_pow_div {T : ℕ → ℕ} (hT : TimeConstructible T) {k : ℕ} + (hk : 0 < k) : TimeConstructible fun n => 2 ^ (T n / k) := by + have hdiv : ComputableInPolyTime (fun m : ℕ => m / k) encNat encNat := + ComputableInPolyTime.binary_div.comp + (ComputableInPolyTime.id'.prod (ComputableInPolyTime.const k)) + have h₁ := ComputableInO.natToUnary.comp (hdiv.nat_inO.comp hT.computableInO) + have h₂ := ((ComputableInDegree.two_pow_length encUnary).inO_one.comp h₁).of_enc_eq + (encC := encNat) (g := fun x : List Bool => 2 ^ (T x.length / k)) fun x => by + simp only [Function.comp_apply, encUnary_apply, List.length_replicate] + obtain ⟨C, hC⟩ := PolynomiallyBounded.exists_le_mul_two_pow + (p := fun m => 2 * (k * m + k) + (m + 1) ^ 2 + m) (by fun_prop) + refine TimeConstructible.of_computableInO C h₂ + (s := fun n => T n + T n + T n / k + T n / k) (fun x => ?_) fun x => ?_ + · have hlt : T x.length < k * (T x.length / k + 1) := by + rw [Nat.mul_add_one] + exact Nat.lt_div_mul_add hk |>.trans_eq (by ring) + have := hC (T x.length / k) + simp only [Function.comp_apply, encUnary_apply, List.length_replicate] + nlinarith + · simp only [Function.comp_apply, encUnary_apply, List.length_replicate] + exact le_rfl + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean new file mode 100644 index 000000000..8a12ca07a --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean @@ -0,0 +1,197 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.CeqP.Time +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Separation +public import Complexity.Computability.Complexity.Classes.ModP.Time +import Complexity.Computability.Complexity.Classes.FunctionTime.Decide +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision + +/-! +# Counting classes from exact counting in time `2 ^ O(T / √log T)` + +For time-constructible `T` with `max n 2 ≤ T n`, every count in `Cslib.Complexity.SharpTIME enc T` +is computed exactly, in binary, within time `2 ^ (C T n / √⌊log₂ (T n)⌋)` +(`Cslib.Complexity.CountingSimulation.SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two`). +Decision classes defined by a polynomial-time test of such counts follow from this. The test reads +outputs of at most that many digits, so it runs within time polynomial in +`2 ^ (C T n / √⌊log₂ (T n)⌋)` (`Cslib.Complexity.setOf_mem_DTIME_of_mem_FTIME`), which is +`2 ^ (C' T n / √⌊log₂ (T n)⌋)` for a larger constant `C'`. Hence every problem decided by a +polynomial-time test of two counts in `SharpTIME enc T` lies in +`⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]` +(`Cslib.Complexity.CountingSimulation.setOf_mem_iUnion_DTIME_of_mem_SharpTIME`). On bit strings, +every class of such problems is strictly contained in `DTIME[2 ^ T]` +(`Cslib.Complexity.CountingSimulation.ssubset_DTIME_two_pow_of_forall_mem_SharpTIME`), by the +separation of `Complexity.Computability.Complexity.Classes.CountingSimulation.Separation`. + +Parity, a nonzero residue modulo a fixed `k` and equality of two counts are such tests. This gives +the containments and strict containments of `Cslib.Complexity.ParityTIME`, +`Cslib.Complexity.ModTIME` (for every fixed `k`) and `Cslib.Complexity.CeqTIME`. The bounds are on +time only; no polynomial workspace bound is claimed for these classes. + +`NTIME`, `BPTIME` and `PPTIME` reduce in this library to counts of padded fair-coin strings +(`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`), not to terminal-path counts, so they are not +derived here. Their strict containments in `DTIME[2 ^ T]` are in `CountingSimulation.Separation`. + +## Main results + +* `Cslib.Complexity.CountingSimulation.setOf_mem_iUnion_DTIME_of_mem_SharpTIME`: a polynomial-time + test of two terminal-path counts. +* `Cslib.Complexity.CountingSimulation.ssubset_DTIME_two_pow_of_forall_mem_SharpTIME`: the strict + containment of every class of such tests in `DTIME[2 ^ T]`. +* `ParityTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`, + `ModTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`, + `CeqTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`: the containments. +* `ParityTIME_ssubset_DTIME_two_pow`, `ModTIME_ssubset_DTIME_two_pow`, + `CeqTIME_ssubset_DTIME_two_pow`: the strict containments in `DTIME[2 ^ T]`. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} + +/-- The scale `2 ^ (C T n / √⌊log₂ (T n)⌋)` is monotone in the constant. -/ +private theorem two_pow_div_sqrt_log_two_mono {C C' : ℕ} (h : C ≤ C') (n : ℕ) : + 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) ≤ 2 ^ (C' * T n / Nat.sqrt (Nat.log 2 (T n))) := + Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ h)) + +/-- **A polynomial-time test of two terminal-path counts in time `2 ^ O(T / √log T)`.** For +time-constructible `T` with `max n 2 ≤ T n`, counts `f` and `g` in `SharpTIME enc T` and a +polynomial-time test `rule` of binary pairs, the instances where `rule (f a, g a)` holds form a +problem in `⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`. -/ +theorem setOf_mem_iUnion_DTIME_of_mem_SharpTIME (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) {f g : α → ℕ} (hf : f ∈ SharpTIME enc T) + (hg : g ∈ SharpTIME enc T) {rule : ℕ × ℕ → Bool} + (hrule : ComputableInPolyTime rule (encPair encNat encNat) encBool) : + {a | rule (f a, g a) = true} ∈ + ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by + obtain ⟨C₁, hf'⟩ := + Set.mem_iUnion.mp (SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two hT hTn hf) + obtain ⟨C₂, hg'⟩ := + Set.mem_iUnion.mp (SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two hT hTn hg) + set C := max C₁ C₂ + obtain ⟨e, he⟩ := setOf_mem_DTIME_of_mem_FTIME + (FTIME_mono (two_pow_div_sqrt_log_two_mono (le_max_left C₁ C₂)) hf') + (FTIME_mono (two_pow_div_sqrt_log_two_mono (le_max_right C₁ C₂)) hg') hrule + -- `(2 ^ x + 1) ^ e ≤ 2 ^ e * 2 ^ (e * x)` + refine Set.mem_iUnion.mpr ⟨e * C, DTIME_mono_of_le_mul_add (C := 2 ^ e) (fun n => ?_) he⟩ + have h1 : 1 ≤ 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := Nat.one_le_two_pow + calc (2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) + 1) ^ e + ≤ (2 * 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))) ^ e := Nat.pow_le_pow_left (by omega) e + _ = 2 ^ e * 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)) * e) := by rw [mul_pow, ← pow_mul] + _ ≤ 2 ^ e * 2 ^ (e * C * T n / Nat.sqrt (Nat.log 2 (T n))) := by + refine Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) ?_) + rw [mul_comm _ e, mul_assoc] + exact Nat.mul_div_le_mul_div_assoc _ _ _ + _ ≤ _ := Nat.le_add_right _ _ + +/-- **Strict containment in `DTIME[2 ^ T]` of every class decided by tests of counts.** For +time-constructible `T` with `max n 2 ≤ T n`, every class of problems on bit strings, each decided +by a polynomial-time test of two counts in `SharpTIME encBits T`, is strictly contained in +`DTIME[2 ^ T]`. -/ +theorem ssubset_DTIME_two_pow_of_forall_mem_SharpTIME {𝒞 : Set (Set (List Bool))} + (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) + (h : ∀ A ∈ 𝒞, ∃ f ∈ SharpTIME encBits T, ∃ g ∈ SharpTIME encBits T, ∃ rule : ℕ × ℕ → Bool, + ComputableInPolyTime rule (encPair encNat encNat) encBool ∧ + ∀ x, x ∈ A ↔ rule (f x, g x) = true) : + 𝒞 ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_subset_iUnion hT (fun n => (le_max_left _ _).trans (hTn n)) + fun A hA => by + obtain ⟨f, hf, g, hg, rule, hrule, hA⟩ := h A hA + rw [show A = {x | rule (f x, g x) = true} from Set.ext hA] + exact setOf_mem_iUnion_DTIME_of_mem_SharpTIME hT hTn hf hg hrule + +/-! ### Parity, modular and exact counting -/ + +private theorem computableInPolyTime_mod_ne_zero (k : ℕ) : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.1 % k ≠ 0)) + (encPair encNat encNat) encBool := + ComputableInPolyTime.decide_not (p := fun p : ℕ × ℕ => p.1 % k = 0) + (ComputableInPolyTime.decide_eq' (ComputableInPolyTime.binary_mod.comp + ((ComputableInPolyTime.fst encNat encNat).prod (ComputableInPolyTime.const k))) + (ComputableInPolyTime.const 0)) + +private theorem computableInPolyTime_eq : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.1 = p.2)) (encPair encNat encNat) encBool := + ComputableInPolyTime.decide_eq' (ComputableInPolyTime.fst encNat encNat) + (ComputableInPolyTime.snd encNat encNat) + +/-- `Mod_kTIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/ +private theorem ModTIME_forall_mem_SharpTIME {k : ℕ} {A : Set α} (hA : A ∈ ModTIME k enc T) : + ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∃ rule : ℕ × ℕ → Bool, + ComputableInPolyTime rule (encPair encNat encNat) encBool ∧ + ∀ x, x ∈ A ↔ rule (f x, g x) = true := by + obtain ⟨f, hf, hA⟩ := hA + exact ⟨f, hf, f, hf, _, computableInPolyTime_mod_ne_zero k, fun x => by simp [hA x]⟩ + +/-- `C₌TIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/ +private theorem CeqTIME_forall_mem_SharpTIME {A : Set α} (hA : A ∈ CeqTIME enc T) : + ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∃ rule : ℕ × ℕ → Bool, + ComputableInPolyTime rule (encPair encNat encNat) encBool ∧ + ∀ x, x ∈ A ↔ rule (f x, g x) = true := by + obtain ⟨f, hf, g, hg, hA⟩ := hA + exact ⟨f, hf, g, hg, _, computableInPolyTime_eq, fun x => by simp [hA x]⟩ + +/-- **`Mod_kTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for every fixed `k` and +time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem ModTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (k : ℕ) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + ModTIME k enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + fun A hA => by + obtain ⟨f, hf, g, hg, rule, hrule, hA⟩ := ModTIME_forall_mem_SharpTIME hA + rw [show A = {x | rule (f x, g x) = true} from Set.ext hA] + exact setOf_mem_iUnion_DTIME_of_mem_SharpTIME hT hTn hf hg hrule + +/-- **`⊕TIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for time-constructible `T` with +`max n 2 ≤ T n`. -/ +theorem ParityTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + ParityTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by + rw [← ModTIME_two] + exact ModTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two 2 hT hTn + +/-- **`C₌TIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for time-constructible `T` with +`max n 2 ≤ T n`. -/ +theorem CeqTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + CeqTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + fun A hA => by + obtain ⟨f, hf, g, hg, rule, hrule, hA⟩ := CeqTIME_forall_mem_SharpTIME hA + rw [show A = {x | rule (f x, g x) = true} from Set.ext hA] + exact setOf_mem_iUnion_DTIME_of_mem_SharpTIME hT hTn hf hg hrule + +/-- **`Mod_kTIME[T] ⊊ DTIME[2 ^ T]`** for every fixed `k` and time-constructible `T` with +`max n 2 ≤ T n`. -/ +theorem ModTIME_ssubset_DTIME_two_pow (k : ℕ) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : ModTIME k encBits T ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ => ModTIME_forall_mem_SharpTIME + +/-- **`⊕TIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem ParityTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) : + ParityTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n := by + rw [← ModTIME_two] + exact ModTIME_ssubset_DTIME_two_pow 2 hT hTn + +/-- **`C₌TIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem CeqTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) : + CeqTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ => CeqTIME_forall_mem_SharpTIME + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean new file mode 100644 index 000000000..10dc7f685 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastSimulation +public import Complexity.Computability.Complexity.Classes.Hierarchy.Time +import Complexity.Computability.Complexity.Classes.Constructible.TwoPow +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential + +/-! +# Strict containments in `DTIME[2 ^ T]` from the counting simulation + +For time-constructible `T` with `max n 2 ≤ T n`, the counting simulation of #1833 places +`NTIME[T]`, `BPTIME[T]` and `PPTIME[T]` in `⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]` +(`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two` and its +siblings). That union lies in `DTIME[2 ^ T]` but does not exhaust it. Hence each of these classes +is strictly contained in `DTIME[2 ^ T]` on bit strings. + +**The separating language** is the clocked diagonal `Cslib.Complexity.timeDiagonal J` of +`Complexity.Computability.Complexity.Classes.Hierarchy.Time`, with the clock +`J n = 2 ^ (T n / 4)`. This clock is time-constructible +(`Cslib.Complexity.TimeConstructible.two_pow_div`). One language serves every constant `C`: + +* it is decidable within time `O((n + 1) ^ 5 * (J n + 1) ^ 3)`, which is `O(2 ^ T n)` because + `(n + 1) ^ 5 ≤ (T n + 1) ^ 5 = O(2 ^ (T n / 4))`; +* for each `C` and `c`, eventually `c * 2 ^ (C T n / √⌊log₂ T n⌋) + c ≤ J n`, since + `√⌊log₂ T n⌋ ≥ 8 C` and `2 c ≤ 2 ^ (T n / 8)` from some length on, so the diagonal argument + (`Cslib.Complexity.setOf_timeDiagonal_notMem_DTIME`) excludes it from each + `DTIME[2 ^ (C T / √⌊log₂ T⌋)]`. + +The polynomial overhead of the native universal machine is absorbed by the gap between +`2 ^ (T / 4)` and `2 ^ T`. No faster universal simulation is assumed. + +The same separation applies to every class decided by polynomial-time tests of exact counts in +`Cslib.Complexity.SharpTIME`, such as `⊕TIME[T]`, `Mod_kTIME[T]` and `C₌TIME[T]` +(`Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses`). + +## Main results + +* `Cslib.Complexity.CountingSimulation.iUnion_DTIME_two_pow_div_sqrt_log_two_subset`: the union + lies in `DTIME[2 ^ T]`. +* `DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`: one language of + `DTIME[2 ^ T]` lies outside every `DTIME[2 ^ (C T / √⌊log₂ T⌋)]`. +* `Cslib.Complexity.CountingSimulation.ssubset_DTIME_two_pow_of_subset_iUnion`: every class inside + the union is strictly contained in `DTIME[2 ^ T]`. +* `Cslib.Complexity.CountingSimulation.NTIME_ssubset_DTIME_two_pow`, + `BPTIME_ssubset_DTIME_two_pow`, `PPTIME_ssubset_DTIME_two_pow`: the strict containments. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Filter Turing.MultiTapeTM + +variable {T : ℕ → ℕ} + +/-- From some length on, `√⌊log₂ (T n)⌋` is at least any given constant. -/ +private theorem eventually_le_sqrt_log_two (hTn : ∀ n, n ≤ T n) (C : ℕ) : + ∀ᶠ n in atTop, C ≤ Nat.sqrt (Nat.log 2 (T n)) := by + filter_upwards [eventually_ge_atTop (2 ^ (C * C))] with n hn + exact Nat.le_sqrt.mpr (Nat.le_log_of_pow_le one_lt_two (hn.trans (hTn n))) + +/-- **The union lies in `DTIME[2 ^ T]`**: each exponent `C T / √⌊log₂ T⌋` is eventually at +most `T`. -/ +theorem iUnion_DTIME_two_pow_div_sqrt_log_two_subset {α : Type} {enc : α ↪ List Bool} + (hTn : ∀ n, n ≤ T n) : + (⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))) ⊆ + DTIME enc fun n => 2 ^ T n := by + refine Set.iUnion_subset fun C => DTIME_mono_of_eventually_le ?_ + filter_upwards [eventually_le_sqrt_log_two hTn C] with n hn + exact Nat.pow_le_pow_right (by norm_num) (Nat.div_le_of_le_mul (Nat.mul_le_mul_right _ hn)) + +/-- The upper resource bound of the clocked diagonal with clock `2 ^ (T n / 4)` is +`O(2 ^ T n)`. -/ +private theorem exists_diagonal_bound_le (hTn : ∀ n, n ≤ T n) : + ∃ K, ∀ n, (n + 1) ^ 5 * (2 ^ (T n / 4) + 1) ^ 3 ≤ K * 2 ^ T n + K := by + obtain ⟨C₀, hC₀⟩ := PolynomiallyBounded.exists_le_mul_two_pow + (p := fun m => (4 * m + 4) ^ 5) (by fun_prop) + refine ⟨8 * C₀, fun n => ?_⟩ + set m := T n / 4 with hm + have h₁ : n + 1 ≤ 4 * m + 4 := by + have := hTn n + omega + have h₂ : (n + 1) ^ 5 ≤ C₀ * 2 ^ m := (Nat.pow_le_pow_left h₁ 5).trans (hC₀ m) + have h₃ : (2 ^ m + 1) ^ 3 ≤ 8 * 2 ^ (3 * m) := by + have : 1 ≤ 2 ^ m := Nat.one_le_two_pow + calc (2 ^ m + 1) ^ 3 ≤ (2 * 2 ^ m) ^ 3 := Nat.pow_le_pow_left (by omega) 3 + _ = 8 * 2 ^ (3 * m) := by ring + have h₄ : 2 ^ (m + 3 * m) ≤ 2 ^ T n := Nat.pow_le_pow_right (by norm_num) (by omega) + calc (n + 1) ^ 5 * (2 ^ m + 1) ^ 3 ≤ C₀ * 2 ^ m * (8 * 2 ^ (3 * m)) := Nat.mul_le_mul h₂ h₃ + _ = 8 * C₀ * 2 ^ (m + 3 * m) := by ring + _ ≤ 8 * C₀ * 2 ^ T n + 8 * C₀ := (Nat.mul_le_mul_left _ h₄).trans (Nat.le_add_right _ _) + +/-- The clock `2 ^ (T n / 4)` eventually exceeds every `c * 2 ^ (C T n / √⌊log₂ T n⌋) + c`. -/ +private theorem eventually_le_two_pow_div_four (hTn : ∀ n, n ≤ T n) (C c : ℕ) : + ∀ᶠ n in atTop, c * 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) + c ≤ 2 ^ (T n / 4) := by + filter_upwards [eventually_le_sqrt_log_two hTn (8 * C), + eventually_ge_atTop (16 * c + 16)] with n hs hn + set s := Nat.sqrt (Nat.log 2 (T n)) + set u := T n / 8 with hu + -- the exponent is at most `T n / 8` + have hexp : C * T n / s ≤ u := by + rcases Nat.eq_zero_or_pos C with rfl | hC + · simp + · refine (Nat.le_div_iff_mul_le (by norm_num)).mpr ?_ + have hdiv := Nat.div_mul_le_self (C * T n) s + have : C * T n / s * (8 * C) ≤ C * T n := (Nat.mul_le_mul_left _ hs).trans hdiv + nlinarith + -- `2 c` is below `2 ^ u` + have hcu : 2 * c ≤ 2 ^ u := by + have : 2 * c + 1 ≤ u := by + have := hTn n + omega + exact (Nat.le_succ _).trans (this.trans Nat.lt_two_pow_self.le) + have hu2 : 2 ^ u * 2 ^ u ≤ 2 ^ (T n / 4) := by + rw [← pow_add] + exact Nat.pow_le_pow_right (by norm_num) (by omega) + calc c * 2 ^ (C * T n / s) + c ≤ c * 2 ^ u + c * 2 ^ u := + Nat.add_le_add (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by norm_num) hexp)) + (Nat.le_mul_of_pos_right _ Nat.one_le_two_pow) + _ = 2 * c * 2 ^ u := by ring + _ ≤ 2 ^ u * 2 ^ u := Nat.mul_le_mul_right _ hcu + _ ≤ 2 ^ (T n / 4) := hu2 + +/-- **One language of `DTIME[2 ^ T]` outside every `DTIME[2 ^ (C T / √⌊log₂ T⌋)]`**, for a +time-constructible `T` with `n ≤ T n`: the clocked diagonal with clock `2 ^ (T n / 4)`. -/ +theorem DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two + (hT : TimeConstructible T) (hTn : ∀ n, n ≤ T n) : + ¬DTIME encBits (fun n => 2 ^ T n) ⊆ + ⋃ C, DTIME encBits fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by + intro h + obtain ⟨K, hK⟩ := exists_diagonal_bound_le hTn + have hmem := DTIME_mono_of_le_mul_add hK + (setOf_timeDiagonal_mem_DTIME (hT.two_pow_div (by norm_num : 0 < 4))) + obtain ⟨C, hC⟩ := Set.mem_iUnion.mp (h hmem) + exact setOf_timeDiagonal_notMem_DTIME (eventually_le_two_pow_div_four hTn C) hC + +/-- **Strict containment in `DTIME[2 ^ T]`** of every class of problems on bit strings inside +`⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`, for a time-constructible `T` with `n ≤ T n`. -/ +theorem ssubset_DTIME_two_pow_of_subset_iUnion {𝒞 : Set (Set (List Bool))} + (hT : TimeConstructible T) (hTn : ∀ n, n ≤ T n) + (h : 𝒞 ⊆ ⋃ C, DTIME encBits fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))) : + 𝒞 ⊂ DTIME encBits fun n => 2 ^ T n := + ⟨h.trans (iUnion_DTIME_two_pow_div_sqrt_log_two_subset hTn), fun hsub => + DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn (hsub.trans h)⟩ + +private theorem le_of_max_le (hTn : ∀ n, max n 2 ≤ T n) (n : ℕ) : n ≤ T n := + (le_max_left _ _).trans (hTn n) + +/-- **`NTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem NTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) : + NTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn) + (NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn) + +/-- **`BPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem BPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) : + BPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn) + (BPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn) + +/-- **`PPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem PPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) : + PPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n := + ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn) + (PPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn) + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean b/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean new file mode 100644 index 000000000..e051095a9 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.FunctionTime +public import Complexity.Computability.Complexity.Classes.Time +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts + +/-! +# Deciding by a polynomial-time test of function-time outputs + +A function in `Cslib.Complexity.FTIME enc encOut t` writes its encoded output within time +`O(t n)`, so the output has length `O(t n)`. A polynomial-time test of the outputs of two such +functions therefore runs within time polynomial in `t n`: the problem it decides lies in +`DTIME[(t + 1) ^ e]` for some `e`. This is how decision classes defined by counts, such as +parity or equality of counts, follow from computing the counts. + +## Main results + +* `Cslib.Complexity.setOf_mem_DTIME_of_mem_FTIME`: a polynomial-time test of two function-time + outputs decides a problem in `DTIME[(t + 1) ^ e]`. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α β β₁ β₂ : Type} {enc : α ↪ List Bool} {t : ℕ → ℕ} + +/-- A function in `FTIME[t]` is computable within time `O(t n)`, and its encoded output has length +`O(t n)`. -/ +private theorem FTIME.exists_computableInO {encOut : β ↪ List Bool} {f : α → β} + (hf : f ∈ FTIME enc encOut t) : + ∃ (c : ℕ) (s : ℕ → ℕ), ComputableInO f enc encOut (fun a => t (enc a).length) + (fun a => t (enc a).length + s (enc a).length) ∧ + ∀ a, (encOut (f a)).length ≤ c * (t (enc a).length + 1) := by + obtain ⟨c₁, c₂, s, h⟩ := hf + have hl (a : α) : (encOut (f a)).length ≤ (c₁ + c₂ + 1) * (t (enc a).length + 1) := + (h.length_le a).trans (by nlinarith) + exact ⟨c₁ + c₂ + 1, s, ⟨c₁ + c₂ + 1, h.mono (fun _ => by dsimp only; nlinarith) + (fun _ => by dsimp only; nlinarith), fun a => (hl a).trans (by nlinarith)⟩, hl⟩ + +/-- **A polynomial-time test of two function-time outputs.** If `f` and `g` are in `FTIME[t]` +and `rule` is a polynomial-time test of their encoded pair, then the instances where +`rule (f a, g a)` holds form a problem in `DTIME[(t + 1) ^ e]` for some `e`. -/ +theorem setOf_mem_DTIME_of_mem_FTIME {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} + {f : α → β₁} {g : α → β₂} (hf : f ∈ FTIME enc enc₁ t) (hg : g ∈ FTIME enc enc₂ t) + {rule : β₁ × β₂ → Bool} (hrule : ComputableInPolyTime rule (encPair enc₁ enc₂) encBool) : + ∃ e, {a | rule (f a, g a) = true} ∈ DTIME enc fun n => (t n + 1) ^ e := by + obtain ⟨c₁, s₁, h₁, hl₁⟩ := FTIME.exists_computableInO hf + obtain ⟨c₂, s₂, h₂, hl₂⟩ := FTIME.exists_computableInO hg + obtain ⟨e, e', hr⟩ := hrule.tidy.exists_degree + have h := (ComputableInO.of_tidy hr.inO).comp (h₁.prod h₂) + set c := c₁ + c₂ + 1 with hc + have hmem := setOf_mem_DTIME_of_computableInO h + (t := fun n => (2 + (3 * c) ^ e) * (t n + 1) ^ (e + 1)) fun a => by + have hlen : (encPair enc₁ enc₂ (f a, g a)).length + 1 ≤ + 3 * c * (t (enc a).length + 1) := by + rw [length_encPair] + have := hl₁ a + have := hl₂ a + dsimp only + rw [hc] + nlinarith + have hpow : ((encPair enc₁ enc₂ (f a, g a)).length + 1) ^ e ≤ + (3 * c) ^ e * (t (enc a).length + 1) ^ (e + 1) := + calc _ ≤ (3 * c * (t (enc a).length + 1)) ^ e := Nat.pow_le_pow_left hlen e + _ = (3 * c) ^ e * (t (enc a).length + 1) ^ e := mul_pow _ _ _ + _ ≤ _ := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_succ e)) + have ht : t (enc a).length + 1 ≤ (t (enc a).length + 1) ^ (e + 1) := + Nat.le_self_pow (Nat.succ_ne_zero e) _ + calc _ ≤ t (enc a).length + t (enc a).length + + (3 * c) ^ e * (t (enc a).length + 1) ^ (e + 1) := by omega + _ ≤ _ := by nlinarith + exact ⟨e + 1, DTIME_mono_of_le_mul_add (C := 2 + (3 * c) ^ e) (fun _ => Nat.le_add_right _ _) + (by simpa only [Function.comp_apply] using hmem)⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/ModP/Time.lean b/Complexity/Computability/Complexity/Classes/ModP/Time.lean new file mode 100644 index 000000000..c6a3bbc60 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/ModP/Time.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.ModP +public import Complexity.Computability.Complexity.Classes.SharpP.Time + +/-! +# Time-bounded parity and modular counting + +`Cslib.Complexity.ParityTIME enc t` and `Cslib.Complexity.ModTIME k enc t` are time-parameterized +counterparts of `Cslib.Complexity.ParityP` and `Cslib.Complexity.ModP k`. Membership is the +oddness, respectively a nonzero residue modulo `k`, of a count in +`Cslib.Complexity.SharpTIME enc t`. Such a count is the number of accepting terminal branches of +one fixed nonblocking native counting machine whose branches all halt within time `O(t n)`. + +**Why terminal paths.** A terminal path is counted once, so enlarging a sufficient clock does not +change the count (`Cslib.Complexity.SharpTIME_mono`). Padded fair-coin strings, as counted for +`Cslib.Complexity.PPTIME`, behave differently: after a run halts, each further coin doubles its +contribution. That leaves the acceptance probability unchanged but changes residues, so padded +counts suit threshold classes and not modular ones. + +As for `Cslib.Complexity.ModP`, the definition is total in `k`. The standard modular counting +classes take `k ≥ 2`, and `ModTIME 2 = ParityTIME` (`Cslib.Complexity.ModTIME_two`). At +polynomial clocks these are the verifier-based classes: +`Cslib.Complexity.mem_ModP_iff_exists_mem_ModTIME` and +`Cslib.Complexity.mem_ParityP_iff_exists_mem_ParityTIME`. Both follow from the equality of +`Cslib.Complexity.SharpP` with the union of the classes `SharpTIME (n ^ d)` +(`Cslib.Complexity.mem_SharpP_iff_exists_mem_SharpTIME`). + +## Main definitions + +* `Cslib.Complexity.ParityTIME`: odd terminal-path counts within time `O(t n)`. +* `Cslib.Complexity.ModTIME`: terminal-path counts nonzero modulo `k` within time `O(t n)`. + +## Main results + +* `Cslib.Complexity.ParityTIME_mono`, `Cslib.Complexity.ModTIME_mono`: monotonicity in the clock. +* `Cslib.Complexity.ModTIME_two`: modulo two, a nonzero residue is oddness. +* `Cslib.Complexity.mem_ParityP_iff_exists_mem_ParityTIME`, + `Cslib.Complexity.mem_ModP_iff_exists_mem_ModTIME`: the polynomial-time unions. + +## References + +* [C. H. Papadimitriou, S. Zachos, *Two remarks on the power of counting*][PapadimitriouZachos1983] +* [L. Fortnow, *Counting Complexity*][Fortnow1997] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} {k : ℕ} {t : ℕ → ℕ} + +/-- `⊕TIME[t]`: the problems whose members are the instances where some count in +`SharpTIME enc t` is odd. -/ +def ParityTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := + {A | ∃ f ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ Odd (f a)} + +/-- `Mod_kTIME[t]`: the problems whose members are the instances where some count in +`SharpTIME enc t` is nonzero modulo `k`. The standard classes take `k ≥ 2`. -/ +def ModTIME (k : ℕ) (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := + {A | ∃ f ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ f a % k ≠ 0} + +/-- `ParityTIME` is monotone in the clock. -/ +theorem ParityTIME_mono {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : + ParityTIME enc t₁ ⊆ ParityTIME enc t₂ := fun _ ⟨f, hf, hA⟩ => ⟨f, SharpTIME_mono h hf, hA⟩ + +/-- `ModTIME k` is monotone in the clock. -/ +theorem ModTIME_mono {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : + ModTIME k enc t₁ ⊆ ModTIME k enc t₂ := fun _ ⟨f, hf, hA⟩ => ⟨f, SharpTIME_mono h hf, hA⟩ + +/-- Modulo two, a nonzero residue is oddness. -/ +theorem ModTIME_two : ModTIME 2 enc t = ParityTIME enc t := by + ext A + simp only [ModTIME, ParityTIME, Set.mem_ofPred_eq, ← Nat.not_even_iff_odd, + Nat.even_iff, ne_eq] + +/-- **`ModP k` is the union of the classes `ModTIME k (n ^ d)`.** -/ +theorem mem_ModP_iff_exists_mem_ModTIME : A ∈ ModP k enc ↔ ∃ d, A ∈ ModTIME k enc (· ^ d) := by + constructor + · rintro ⟨f, hf, hA⟩ + obtain ⟨d, hd⟩ := mem_SharpP_iff_exists_mem_SharpTIME.mp hf + exact ⟨d, f, hd, hA⟩ + · rintro ⟨d, f, hf, hA⟩ + exact ⟨f, SharpTIME.subset_SharpP d hf, hA⟩ + +/-- **`⊕P` is the union of the classes `ParityTIME (n ^ d)`.** -/ +theorem mem_ParityP_iff_exists_mem_ParityTIME : + A ∈ ParityP enc ↔ ∃ d, A ∈ ParityTIME enc (· ^ d) := by + simp only [← ModP_two, ← ModTIME_two, mem_ModP_iff_exists_mem_ModTIME] + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Time.lean b/Complexity/Computability/Complexity/Classes/SharpP/Time.lean index f53e73ab4..26bb3d744 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/Time.lean @@ -34,6 +34,7 @@ is distinct from a count of freely padded fair-coin strings. * `Cslib.Complexity.mem_SharpTIME`: the fixed-machine and exact terminal-count contract. * `Cslib.Complexity.SharpTIME_mono`: larger sufficient clocks preserve membership and counts. +* `Cslib.Complexity.SharpTIME_mono_of_le_mul_add`: constant factors of the clock are absorbed. * `Cslib.Complexity.SharpTIME.subset_SharpP`: every polynomial-time slice belongs to `SharpP`. * `Cslib.Complexity.mem_SharpP_iff_exists_mem_SharpTIME`: their union is exactly `SharpP`. @@ -87,6 +88,22 @@ theorem SharpTIME_mono {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) rw [hhalt.branchCount_eq hle] exact hcount +/-- Constant factors and additive constants of the time bound are absorbed by the constants of +`SharpTIME`. -/ +theorem SharpTIME_mono_of_le_mul_add {t₁ t₂ : ℕ → ℕ} {C : ℕ} (h : ∀ n, t₁ n ≤ C * t₂ n + C) : + SharpTIME enc t₁ ⊆ SharpTIME enc t₂ := by + rintro f ⟨c₁, c₂, k, State, hfinite, machine, hnon, hm⟩ + refine ⟨c₁ * C, c₁ * C + c₂, k, State, hfinite, machine, hnon, fun a => ?_⟩ + obtain ⟨hhalt, hcount⟩ := hm a + have hle : c₁ * t₁ (enc a).length + c₂ ≤ c₁ * C * t₂ (enc a).length + (c₁ * C + c₂) := by + have := Nat.mul_le_mul_left c₁ (h (enc a).length) + rw [Nat.mul_add, ← Nat.mul_assoc] at this + omega + refine ⟨hhalt.mono hle, ?_⟩ + change machine.branchCount (· == [true]) _ _ = f a + rw [hhalt.branchCount_eq hle] + exact hcount + /-- A polynomial-time accepting-path counter belongs to the existing verifier-defined `#P`. This is the forward native-machine correspondence, with its affine polynomial clock. -/ theorem SharpTIME.subset_SharpP (d : ℕ) : SharpTIME enc (· ^ d) ⊆ SharpP enc := by diff --git a/ComplexityTests/CountingSeparation.lean b/ComplexityTests/CountingSeparation.lean new file mode 100644 index 000000000..33b552ba5 --- /dev/null +++ b/ComplexityTests/CountingSeparation.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses +import Complexity.Computability.Complexity.Classes.Constructible.Log + +/-! # Counting classes and strict containments in `DTIME[2 ^ T]`: checked instances + +The containments and strict containments at the clock `T n = (n + 1) ^ 2 + 1`, which is +time-constructible and at least `max n 2`, and nonvacuity of the new time-bounded counting +classes through their polynomial-time unions. -/ + +namespace ComplexityTests.CountingSeparation + +open Cslib.Complexity Cslib.Complexity.CountingSimulation Turing.MultiTapeTM + +/-- The clock `(n + 1) ^ 2 + 1` is time-constructible. -/ +theorem timeConstructible_succ_sq_add_one : TimeConstructible fun n => (n + 1) ^ 2 + 1 := + timeConstructible_succ_sq.comp_of_computableInPolyTime (g := fun m => m + 1) + (ComputableInPolyTime.binary_add.comp + (ComputableInPolyTime.id'.prod (ComputableInPolyTime.const 1))) + fun _ => Nat.le_succ _ + +/-- The clock `(n + 1) ^ 2 + 1` is at least `max n 2`. -/ +theorem max_le_succ_sq_add_one (n : ℕ) : max n 2 ≤ (n + 1) ^ 2 + 1 := + max_le (by nlinarith) (by have := Nat.one_le_pow 2 (n + 1) (Nat.succ_pos n); omega) + +/-! ### The separating clock -/ + +example : TimeConstructible fun n => 2 ^ (((n + 1) ^ 2 + 1) / 4) := + timeConstructible_succ_sq_add_one.two_pow_div (by norm_num) + +example : ¬DTIME encBits (fun n => 2 ^ ((n + 1) ^ 2 + 1)) ⊆ ⋃ C, DTIME encBits fun n => + 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := + DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two + timeConstructible_succ_sq_add_one fun n => (le_max_left _ _).trans (max_le_succ_sq_add_one n) + +/-! ### Nondeterministic and probabilistic time -/ + +example : NTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + NTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +example : BPTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + BPTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +example : PPTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + PPTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +/-! ### Parity, modular and exact counting -/ + +example {α : Type} {enc : α ↪ List Bool} : + ParityTIME enc (fun n => (n + 1) ^ 2 + 1) ⊆ ⋃ C, DTIME enc fun n => + 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := + ParityTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two timeConstructible_succ_sq_add_one + max_le_succ_sq_add_one + +example {α : Type} {enc : α ↪ List Bool} : + ModTIME 3 enc (fun n => (n + 1) ^ 2 + 1) ⊆ ⋃ C, DTIME enc fun n => + 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := + ModTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two 3 timeConstructible_succ_sq_add_one + max_le_succ_sq_add_one + +example {α : Type} {enc : α ↪ List Bool} : + CeqTIME enc (fun n => (n + 1) ^ 2 + 1) ⊆ ⋃ C, DTIME enc fun n => + 2 ^ (C * ((n + 1) ^ 2 + 1) / Nat.sqrt (Nat.log 2 ((n + 1) ^ 2 + 1))) := + CeqTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two timeConstructible_succ_sq_add_one + max_le_succ_sq_add_one + +example : ParityTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + ParityTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +example : ModTIME 3 encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + ModTIME_ssubset_DTIME_two_pow 3 timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +example : CeqTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ + DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := + CeqTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one + +/-! ### Nonvacuity through the polynomial-time unions -/ + +example {α : Type} {enc : α ↪ List Bool} : ∃ d, (∅ : Set α) ∈ ModTIME 3 enc (· ^ d) := + mem_ModP_iff_exists_mem_ModTIME.mp (P_subset_ModP (by norm_num) empty_mem_P) + +example {α : Type} {enc : α ↪ List Bool} : ∃ d, (∅ : Set α) ∈ ParityTIME enc (· ^ d) := by + rw [← mem_ParityP_iff_exists_mem_ParityTIME, ← ModP_two] + exact P_subset_ModP le_rfl empty_mem_P + +example {α : Type} {enc : α ↪ List Bool} : ∃ d, (Set.univ : Set α) ∈ CeqTIME enc (· ^ d) := by + refine mem_CeqP_iff_exists_mem_CeqTIME.mp (coNP_subset_CeqP ?_) + rw [mem_coNP, Set.compl_univ] + exact P_subset_NP empty_mem_P + +end ComplexityTests.CountingSeparation From 8131f79fd8c456085666186b2fe638f809e4f4d7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:46:53 -0400 Subject: [PATCH 3/3] refactor(Classes): expose FTIME bounds and SharpTIME degree monotonicity Address the #2054 review by reviewer-codex-edemaine: - FTIME.exists_computableInO, the bridge from the FTIME contract to charged native bounds with an output-length bound, moves to the public FunctionTime/Bounds.lean and is reused by FunctionTime/Decide.lean. - SharpTIME_pow_mono, monotonicity of polynomial SharpTIME slices in the degree (including input length 0), moves from a private lemma in CeqP/Time.lean to SharpP/Time.lean beside SharpTIME_mono_of_le_mul_add. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Complexity/Classes/CeqP/Time.lean | 18 ++----- .../Classes/FunctionTime/Bounds.lean | 49 +++++++++++++++++++ .../Classes/FunctionTime/Decide.lean | 22 ++------- .../Complexity/Classes/SharpP/Time.lean | 12 +++++ ComplexityTests/CountingSeparation.lean | 12 +++++ 6 files changed, 83 insertions(+), 31 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/FunctionTime/Bounds.lean diff --git a/Complexity.lean b/Complexity.lean index f021d1b23..e6a780b13 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1175,6 +1175,7 @@ public import Complexity.Computability.Complexity.Classes.EXP public import Complexity.Computability.Complexity.Classes.FewP public import Complexity.Computability.Complexity.Classes.FewP.Machine public import Complexity.Computability.Complexity.Classes.FunctionTime +public import Complexity.Computability.Complexity.Classes.FunctionTime.Bounds public import Complexity.Computability.Complexity.Classes.FunctionTime.Decide public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.LogClock diff --git a/Complexity/Computability/Complexity/Classes/CeqP/Time.lean b/Complexity/Computability/Complexity/Classes/CeqP/Time.lean index 0f9878cae..3dba01118 100644 --- a/Complexity/Computability/Complexity/Classes/CeqP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/CeqP/Time.lean @@ -22,8 +22,8 @@ follows the two-count characterization of `C=P` At polynomial clocks this is `CeqP`: `Cslib.Complexity.mem_CeqP_iff_exists_mem_CeqTIME`, by the equality of `Cslib.Complexity.SharpP` with the union of the classes `SharpTIME (n ^ d)`. The two -counts may first need different polynomial clocks; constant factors are absorbed, so the larger -clock serves both (`Cslib.Complexity.SharpTIME_mono_of_le_mul_add`). +counts may first need different polynomial clocks; the larger clock serves both +(`Cslib.Complexity.SharpTIME_pow_mono`). ## Main definitions @@ -57,16 +57,6 @@ theorem CeqTIME_mono {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : CeqTIME enc t₁ ⊆ CeqTIME enc t₂ := fun _ ⟨f, hf, g, hg, hA⟩ => ⟨f, SharpTIME_mono h hf, g, SharpTIME_mono h hg, hA⟩ -/-- A smaller polynomial degree gives a smaller `SharpTIME` class: `n ^ d ≤ n ^ D + 1`. -/ -private theorem SharpTIME_pow_subset {d D : ℕ} (h : d ≤ D) : - SharpTIME enc (· ^ d) ⊆ SharpTIME enc (· ^ D) := - SharpTIME_mono_of_le_mul_add (C := 1) fun n => by - rcases Nat.eq_zero_or_pos n with rfl | hn - · rcases Nat.eq_zero_or_pos d with rfl | hd - · simp - · simp [Nat.zero_pow hd] - · simpa only [one_mul] using (Nat.pow_le_pow_right hn h).trans (Nat.le_succ _) - /-- **`C=P` is the union of the classes `CeqTIME (n ^ d)`.** -/ theorem mem_CeqP_iff_exists_mem_CeqTIME : A ∈ CeqP enc ↔ ∃ d, A ∈ CeqTIME enc (· ^ d) := by rw [mem_CeqP_iff_exists_SharpP] @@ -74,8 +64,8 @@ theorem mem_CeqP_iff_exists_mem_CeqTIME : A ∈ CeqP enc ↔ ∃ d, A ∈ CeqTIM · rintro ⟨f, hf, g, hg, hA⟩ obtain ⟨d₁, hd₁⟩ := mem_SharpP_iff_exists_mem_SharpTIME.mp hf obtain ⟨d₂, hd₂⟩ := mem_SharpP_iff_exists_mem_SharpTIME.mp hg - exact ⟨max d₁ d₂, f, SharpTIME_pow_subset (le_max_left _ _) hd₁, - g, SharpTIME_pow_subset (le_max_right _ _) hd₂, hA⟩ + exact ⟨max d₁ d₂, f, SharpTIME_pow_mono (le_max_left _ _) hd₁, + g, SharpTIME_pow_mono (le_max_right _ _) hd₂, hA⟩ · rintro ⟨d, f, hf, g, hg, hA⟩ exact ⟨f, SharpTIME.subset_SharpP d hf, g, SharpTIME.subset_SharpP d hg, hA⟩ diff --git a/Complexity/Computability/Complexity/Classes/FunctionTime/Bounds.lean b/Complexity/Computability/Complexity/Classes/FunctionTime/Bounds.lean new file mode 100644 index 000000000..a5fa7139a --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/FunctionTime/Bounds.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.FunctionTime +import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts + +/-! +# Charged bounds of function-time computations + +A function in `Cslib.Complexity.FTIME enc encOut t` is computed within time `c₁ * t n + c₂`. As +a computation within time `O(t n)` (`Turing.MultiTapeTM.ComputableInO`), it carries the +workspace of its certificate, and its encoded output, written within the time bound, has length +`O(t n)`. Clients that compose function-time outputs with further computations, such as a +polynomial-time test of two counts, start from this form. + +## Main results + +* `Cslib.Complexity.FTIME.exists_computableInO`: a function in `FTIME[t]` is computable within + time `O(t n)`, with encoded output length `O(t n)`. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {t : ℕ → ℕ} {f : α → β} + +/-- **Function time as charged native bounds.** A function in `FTIME[t]` is computable within +time `O(t n)` and the workspace `t n + s n` of its certificate, and its encoded output has length +`O(t n)`, with the constant `c` fixed before the input. -/ +theorem FTIME.exists_computableInO (hf : f ∈ FTIME enc encOut t) : + ∃ (c : ℕ) (s : ℕ → ℕ), ComputableInO f enc encOut (fun a => t (enc a).length) + (fun a => t (enc a).length + s (enc a).length) ∧ + ∀ a, (encOut (f a)).length ≤ c * (t (enc a).length + 1) := by + obtain ⟨c₁, c₂, s, h⟩ := hf + have hl (a : α) : (encOut (f a)).length ≤ (c₁ + c₂ + 1) * (t (enc a).length + 1) := + (h.length_le a).trans (by nlinarith) + exact ⟨c₁ + c₂ + 1, s, ⟨c₁ + c₂ + 1, h.mono (fun _ => by dsimp only; nlinarith) + (fun _ => by dsimp only; nlinarith), fun a => (hl a).trans (by nlinarith)⟩, hl⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean b/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean index e051095a9..43ab1df7a 100644 --- a/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean +++ b/Complexity/Computability/Complexity/Classes/FunctionTime/Decide.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Complexity.Classes.FunctionTime public import Complexity.Computability.Complexity.Classes.Time +import Complexity.Computability.Complexity.Classes.FunctionTime.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic @@ -21,10 +22,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts # Deciding by a polynomial-time test of function-time outputs A function in `Cslib.Complexity.FTIME enc encOut t` writes its encoded output within time -`O(t n)`, so the output has length `O(t n)`. A polynomial-time test of the outputs of two such -functions therefore runs within time polynomial in `t n`: the problem it decides lies in -`DTIME[(t + 1) ^ e]` for some `e`. This is how decision classes defined by counts, such as -parity or equality of counts, follow from computing the counts. +`O(t n)`, so the output has length `O(t n)` (`Cslib.Complexity.FTIME.exists_computableInO`). +A polynomial-time test of the outputs of two such functions therefore runs within time polynomial +in `t n`: the problem it decides lies in `DTIME[(t + 1) ^ e]` for some `e`. This is how decision +classes defined by counts, such as parity or equality of counts, follow from computing the counts. ## Main results @@ -40,19 +41,6 @@ open Turing.MultiTapeTM variable {α β β₁ β₂ : Type} {enc : α ↪ List Bool} {t : ℕ → ℕ} -/-- A function in `FTIME[t]` is computable within time `O(t n)`, and its encoded output has length -`O(t n)`. -/ -private theorem FTIME.exists_computableInO {encOut : β ↪ List Bool} {f : α → β} - (hf : f ∈ FTIME enc encOut t) : - ∃ (c : ℕ) (s : ℕ → ℕ), ComputableInO f enc encOut (fun a => t (enc a).length) - (fun a => t (enc a).length + s (enc a).length) ∧ - ∀ a, (encOut (f a)).length ≤ c * (t (enc a).length + 1) := by - obtain ⟨c₁, c₂, s, h⟩ := hf - have hl (a : α) : (encOut (f a)).length ≤ (c₁ + c₂ + 1) * (t (enc a).length + 1) := - (h.length_le a).trans (by nlinarith) - exact ⟨c₁ + c₂ + 1, s, ⟨c₁ + c₂ + 1, h.mono (fun _ => by dsimp only; nlinarith) - (fun _ => by dsimp only; nlinarith), fun a => (hl a).trans (by nlinarith)⟩, hl⟩ - /-- **A polynomial-time test of two function-time outputs.** If `f` and `g` are in `FTIME[t]` and `rule` is a polynomial-time test of their encoded pair, then the instances where `rule (f a, g a)` holds form a problem in `DTIME[(t + 1) ^ e]` for some `e`. -/ diff --git a/Complexity/Computability/Complexity/Classes/SharpP/Time.lean b/Complexity/Computability/Complexity/Classes/SharpP/Time.lean index 26bb3d744..df398def4 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/Time.lean @@ -35,6 +35,7 @@ is distinct from a count of freely padded fair-coin strings. * `Cslib.Complexity.mem_SharpTIME`: the fixed-machine and exact terminal-count contract. * `Cslib.Complexity.SharpTIME_mono`: larger sufficient clocks preserve membership and counts. * `Cslib.Complexity.SharpTIME_mono_of_le_mul_add`: constant factors of the clock are absorbed. +* `Cslib.Complexity.SharpTIME_pow_mono`: polynomial slices are monotone in the degree. * `Cslib.Complexity.SharpTIME.subset_SharpP`: every polynomial-time slice belongs to `SharpP`. * `Cslib.Complexity.mem_SharpP_iff_exists_mem_SharpTIME`: their union is exactly `SharpP`. @@ -104,6 +105,17 @@ theorem SharpTIME_mono_of_le_mul_add {t₁ t₂ : ℕ → ℕ} {C : ℕ} (h : rw [hhalt.branchCount_eq hle] exact hcount +/-- Polynomial slices are monotone in the degree: a smaller degree gives a smaller class. At +input length `0` the clocks are `0 ^ d ≤ 0 ^ D + 1`, which the additive constant absorbs. -/ +theorem SharpTIME_pow_mono {d D : ℕ} (h : d ≤ D) : + SharpTIME enc (· ^ d) ⊆ SharpTIME enc (· ^ D) := + SharpTIME_mono_of_le_mul_add (C := 1) fun n => by + rcases Nat.eq_zero_or_pos n with rfl | hn + · rcases Nat.eq_zero_or_pos d with rfl | hd + · simp + · simp [Nat.zero_pow hd] + · simpa only [one_mul] using (Nat.pow_le_pow_right hn h).trans (Nat.le_succ _) + /-- A polynomial-time accepting-path counter belongs to the existing verifier-defined `#P`. This is the forward native-machine correspondence, with its affine polynomial clock. -/ theorem SharpTIME.subset_SharpP (d : ℕ) : SharpTIME enc (· ^ d) ⊆ SharpP enc := by diff --git a/ComplexityTests/CountingSeparation.lean b/ComplexityTests/CountingSeparation.lean index 33b552ba5..88cde4d41 100644 --- a/ComplexityTests/CountingSeparation.lean +++ b/ComplexityTests/CountingSeparation.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses import Complexity.Computability.Complexity.Classes.Constructible.Log +import Complexity.Computability.Complexity.Classes.FunctionTime.Bounds /-! # Counting classes and strict containments in `DTIME[2 ^ T]`: checked instances @@ -84,6 +85,17 @@ example : CeqTIME encBits (fun n => (n + 1) ^ 2 + 1) ⊂ DTIME encBits fun n => 2 ^ ((n + 1) ^ 2 + 1) := CeqTIME_ssubset_DTIME_two_pow timeConstructible_succ_sq_add_one max_le_succ_sq_add_one +/-! ### Supporting API -/ + +example {α : Type} {enc : α ↪ List Bool} : SharpTIME enc (· ^ 1) ⊆ SharpTIME enc (· ^ 2) := + SharpTIME_pow_mono (by norm_num) + +example {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} + (hf : f ∈ FTIME enc encOut fun n => (n + 1) ^ 2 + 1) : + ∃ c, ∀ a, (encOut (f a)).length ≤ c * (((enc a).length + 1) ^ 2 + 1 + 1) := by + obtain ⟨c, -, -, hl⟩ := FTIME.exists_computableInO hf + exact ⟨c, hl⟩ + /-! ### Nonvacuity through the polynomial-time unions -/ example {α : Type} {enc : α ↪ List Bool} : ∃ d, (∅ : Set α) ∈ ModTIME 3 enc (· ^ d) :=