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/5] =?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/5] =?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 f6adee005d064f27c53a4c057253a5d8e20c38a5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:40:14 -0400 Subject: [PATCH 3/5] feat(SharpP): padded coin counts at a linear clock are SharpTIME functions (#2053) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A native counting machine turns the padded accept count of a fair-coin machine at a linear clock into a SharpTIME[T] count. A deterministic phase writes the clock (c₁ + c₂) * 2 ^ Nat.size (T n) in unary within O(T n) steps, by a streaming fold that doubles a unary counter once per binary digit. The counting phase branches once per coin, continuing after the source halts, until the clock is exhausted. Hence NTIME[T], BPTIME[T] and PPTIME[T] are polynomial-time tests of SharpTIME counts, and NTIME/BPTIME/PPTIME_ssubset_DTIME_two_pow become instances of ssubset_DTIME_two_pow_of_forall_mem_SharpTIME. Their statements are unchanged; they move from Separation.lean to CountingClasses.lean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Classes/Constructible/UnaryClock.lean | 200 ++++++++++ .../CountingSimulation/CountingClasses.lean | 63 ++- .../CountingSimulation/Separation.lean | 39 +- .../Classes/SharpP/PaddedCount.lean | 183 +++++++++ .../MultiTape/Counting/PaddedClock.lean | 359 ++++++++++++++++++ ComplexityTests/PaddedCount.lean | 86 +++++ 7 files changed, 899 insertions(+), 34 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean create mode 100644 Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean create mode 100644 ComplexityTests/PaddedCount.lean diff --git a/Complexity.lean b/Complexity.lean index f021d1b23..0e787ef29 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1154,6 +1154,7 @@ 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.Constructible.UnaryClock public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace public import Complexity.Computability.Complexity.Classes.Counting.Space public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate @@ -1302,6 +1303,7 @@ public import Complexity.Computability.Complexity.Classes.SharpP.GapMachine public import Complexity.Computability.Complexity.Classes.SharpP.Lowness public import Complexity.Computability.Complexity.Classes.SharpP.Machine public import Complexity.Computability.Complexity.Classes.SharpP.Oracle +public import Complexity.Computability.Complexity.Classes.SharpP.PaddedCount public import Complexity.Computability.Complexity.Classes.SharpP.PolyTime public import Complexity.Computability.Complexity.Classes.SharpP.Power public import Complexity.Computability.Complexity.Classes.SharpP.Probability @@ -1824,6 +1826,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Guess public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Oracle.Program public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Oracle.Replay public import Complexity.Computability.Machines.Turing.MultiTape.Counting.OutputPrefix +public import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Program public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Sequential public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Verdict diff --git a/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean new file mode 100644 index 000000000..c03599f82 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean @@ -0,0 +1,200 @@ +/- +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 +public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.OutputToTape +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming +import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes +import Complexity.Computability.Machines.Turing.MultiTape.Run + +/-! +# Unary clocks of linear length from time-constructible bounds + +A time-constructible bound `T` is computed in binary within `O(T n)` steps +(`Cslib.Complexity.TimeConstructible`). Some constructions need a clock in unary instead: a run of +true cells on a work tape that a machine consumes one cell per step. Converting `T n` exactly +from binary to unary by counting down takes `O((T n + 1) ^ 2)` steps +(`Turing.MultiTapeTM.ComputableInO.natToUnary`), which is too slow for linear clocks. + +Rounding up to a power of two avoids the conversion. The binary word of `T n` has +`Nat.size (T n)` digits, and doubling a unary counter once per digit writes +`c * 2 ^ Nat.size (T n)` cells. The `i`-th doubling costs `O(c * 2 ^ i)`, so the doublings cost +`O(c * 2 ^ Nat.size (T n)) = O(T n + 1)` together +(`Turing.MultiTapeTM.ComputableTidilyInO.mul_two_pow_length`). The rounded clock lies between +`c * (T n + 1)` and `c * (2 * T n + 1)`. + +`Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock` packages this as one deterministic +machine that writes the clock on its last work tape within `O(T n)` steps, leaving every other +work tape blank, its input head at the start and nothing emitted. This mirrors the polynomial +budget of `MultiTape.Plumbing.PrepareClock`. + +## Main results + +* `Turing.MultiTapeTM.ComputableTidilyInO.mul_two_pow_length`: `c * 2 ^ l.length` in unary within + time `O(c * 2 ^ l.length + l.length)`. +* `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`: a unary clock of + `c * 2 ^ Nat.size (T n)` cells within `O(T n)` steps. +-/ + +public section + +namespace Turing.MultiTapeTM.ComputableTidilyInO + +/-- Doubling a counter once per element of a list multiplies it by `2 ^ length`. -/ +private theorem foldl_double {α : Type} (l : List α) (m : ℕ) : + l.foldl (fun m _ => m + m) m = m * 2 ^ l.length := by + induction l generalizing m with + | nil => simp + | cons a l ih => + rw [List.foldl_cons, ih, List.length_cons, pow_succ] + ring + +/-- The geometric sum of powers of two below `2 ^ n`. -/ +private theorem sum_range_two_pow_lt (n : ℕ) : ∑ i ∈ Finset.range n, 2 ^ i < 2 ^ n := by + induction n with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ, pow_succ] + omega + +/-- **`c * 2 ^ l.length` in unary in linear time.** A streaming fold doubles a unary counter once +per bit of `l`. Round `i` costs `O(c * 2 ^ i)`, so the rounds cost `O(c * 2 ^ l.length)` in total, +plus `O(l.length)` for the scan. -/ +theorem mul_two_pow_length (c : ℕ) : + ComputableTidilyInO (fun l : List Bool => c * 2 ^ l.length) encBits encUnary + (fun l => c * 2 ^ l.length + l.length) fun l => c * 2 ^ l.length + l.length := by + obtain ⟨c₀, hstep, -⟩ := ((ComputableInDegree.unaryAdd (ComputableInDegree.fst encUnary encBool) + (ComputableInDegree.fst encUnary encBool) le_rfl le_rfl).inO_one).tidy + have hstate (l : List Bool) (i : ℕ) (hi : i ≤ l.length) : + (encUnary ((l.take i).foldl (fun m _ => m + m) c)).length = c * 2 ^ i := by + rw [foldl_double, encUnary_apply, List.length_replicate, List.length_take, + Nat.min_eq_left hi] + obtain ⟨K, hK⟩ := ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum (enc := encUnary) + (step := fun m (_ : Bool) => m + m) c hstep + (R := fun _ i => (5 * c₀ + 4) * (c * 2 ^ i + 1)) + (Q := fun l => c₀ * (2 * (c * 2 ^ l.length) + 3)) + (B := fun l => c * 2 ^ l.length) + (fun l i hi => by + have h₁ := hstate l i hi.le + have h₂ := hstate l (i + 1) hi + simp only [length_encPair, encBool_apply, List.length_singleton, h₁, h₂, pow_succ] + nlinarith) + (fun l i hi => by + have h₁ := hstate l i hi.le + have hpow : c * 2 ^ i ≤ c * 2 ^ l.length := + Nat.mul_le_mul_left c (Nat.pow_le_pow_right (by norm_num) hi.le) + simp only [length_encPair, encBool_apply, List.length_singleton, h₁] + nlinarith) + (fun l i hi => by + rw [hstate l i hi] + exact Nat.mul_le_mul_left c (Nat.pow_le_pow_right (by norm_num) hi)) + refine of_bounds (hK.of_enc_eq (g := fun l : List Bool => c * 2 ^ l.length) + fun l => by rw [foldl_double]) (K * (5 * c₀ + 5) + K * (3 * c₀ + 3) + 1) (fun l => ?_) + (fun l => ?_) fun l => ?_ + · have hsum := sum_range_two_pow_lt l.length + have hs : ∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) ≤ + (5 * c₀ + 4) * (c * 2 ^ l.length + l.length) := by + rw [← Finset.mul_sum, Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_const, + Finset.card_range, smul_eq_mul, mul_one] + exact Nat.mul_le_mul_left _ (Nat.add_le_add_right (Nat.mul_le_mul_left c hsum.le) _) + have h₁ : ∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) + c * 2 ^ l.length + 1 + ≤ (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) := by + have e : (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) = + (5 * c₀ + 4) * (c * 2 ^ l.length + l.length) + (c * 2 ^ l.length + l.length) + + (5 * c₀ + 5) := by ring + rw [e] + omega + calc K * (∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) + c * 2 ^ l.length + 1) + ≤ K * ((5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1)) := Nat.mul_le_mul_left K h₁ + _ = K * (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) := by ring + _ ≤ _ := Nat.mul_le_mul_right _ (by omega) + · have h₁ : c₀ * (2 * (c * 2 ^ l.length) + 3) + c * 2 ^ l.length + 1 ≤ + (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) := by + have e : (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) = + c₀ * (2 * (c * 2 ^ l.length) + 3) + c₀ * (c * 2 ^ l.length) + 3 * c₀ * l.length + + 3 * (c * 2 ^ l.length + l.length + 1) := by ring + rw [e] + omega + calc K * (c₀ * (2 * (c * 2 ^ l.length) + 3) + c * 2 ^ l.length + 1) + ≤ K * ((3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1)) := Nat.mul_le_mul_left K h₁ + _ = K * (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) := by ring + _ ≤ _ := Nat.mul_le_mul_right _ (by omega) + · simp only [encUnary_apply, List.length_replicate] + calc c * 2 ^ l.length ≤ 1 * (c * 2 ^ l.length + l.length + 1) := by omega + _ ≤ _ := Nat.mul_le_mul_right _ (by omega) + +end Turing.MultiTapeTM.ComputableTidilyInO + +namespace Cslib.Complexity + +open Turing Turing.MultiTapeTM + +/-- `2 ^ Nat.size m` is the least power of two above `m`, so it is at most `2 * m + 1`. -/ +theorem two_pow_size_le (m : ℕ) : 2 ^ Nat.size m ≤ 2 * m + 1 := by + rcases Nat.eq_zero_or_pos m with rfl | hm + · simp + · have hsize : 0 < Nat.size m := Nat.size_pos.mpr hm + have hle : 2 ^ (Nat.size m - 1) ≤ m := Nat.lt_size.mp (by omega) + have : 2 ^ Nat.size m = 2 * 2 ^ (Nat.size m - 1) := by + rw [← pow_succ'] + congr 1 + omega + omega + +/-- **A unary clock of linear length.** For a time-constructible `T` and a constant `c`, one +deterministic machine with finitely many states writes `c * 2 ^ Nat.size (T n)` true cells on its +last work tape within `C * T n + C` steps, on every input of length `n`. It halts with every other +work tape blank, all heads at their starting cells and nothing emitted. The clock has between +`c * (T n + 1)` and `c * (2 * T n + 1)` cells (`Nat.lt_size_self`, +`Cslib.Complexity.two_pow_size_le`). -/ +theorem TimeConstructible.exists_prepare_unaryClock {T : ℕ → ℕ} (hT : TimeConstructible T) + (c : ℕ) : + ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State) + (C : ℕ), ∀ input, + machine.runFrom (machine.initCfg input) (C * T input.length + C) = + wordsCfg input none (Function.update (fun _ => []) (Fin.last r) + (List.replicate (c * 2 ^ Nat.size (T input.length)) true)) [] := by + have hbits : ComputableTidilyInO (fun x : List Bool => encNat (T x.length)) encBits encBits + (fun x => T x.length) fun x => T x.length := + hT.computableInO.tidy.of_enc_eq fun _ => rfl + have hclock := ((ComputableTidilyInO.mul_two_pow_length c).comp hbits).of_enc_eq + (g := fun x : List Bool => List.replicate (c * 2 ^ Nat.size (T x.length)) true) + (encOut := encBits) fun x => by + simp [encUnary_apply, encNat_apply, Nat.size_eq_bits_len] + have hdigits (m : ℕ) : (encNat m).length = Nat.size m := by + rw [encNat_apply, Nat.size_eq_bits_len] + have hlinear (x : List Bool) : T x.length + (c * 2 ^ (encNat (T x.length)).length + + (encNat (T x.length)).length) ≤ (2 * c + 2) * (T x.length + 1) := by + have h₁ := Nat.mul_le_mul_left c (two_pow_size_le (T x.length)) + have h₂ : Nat.size (T x.length) ≤ T x.length := Nat.size_le.mpr Nat.lt_two_pow_self + rw [hdigits] + have e : (2 * c + 2) * (T x.length + 1) = c * (2 * T x.length + 1) + c + + 2 * (T x.length + 1) := by ring + rw [e] + omega + obtain ⟨c₁, ⟨r, State, hfinite, machine, hmachine⟩, -⟩ := hclock.mono (2 * c + 2) + (T' := fun x => T x.length) (S' := fun x => T x.length) hlinear hlinear + refine ⟨r, State ⊕ RewindWorkState, inferInstance, machine.outputToWord, c₁ + 2 * c + 2, + fun input => ?_⟩ + have hbound : c₁ * (T input.length + 1) + + (List.replicate (c * 2 ^ Nat.size (T input.length)) true).length + 2 ≤ + (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) := by + have h₁ := Nat.mul_le_mul_left c (two_pow_size_le (T input.length)) + rw [List.length_replicate] + have e : (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) = + c₁ * (T input.length + 1) + c * (2 * T input.length + 1) + c + 2 * T input.length + 2 := by + ring + rw [e] + omega + have hwrite := (hmachine input).outputToWord.mono hbound le_rfl + obtain ⟨_, _, hrun, ⟨rfl, rfl⟩, _⟩ := + transformsTapes_iff_runFrom.mp hwrite input (fun _ => []) [] ⟨rfl, rfl⟩ + simpa only [initCfg_eq_wordsCfg, encBits_apply, List.nil_append] using hrun + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean index 8a12ca07a..501c963b1 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean @@ -11,8 +11,10 @@ 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.Complexity.Classes.SharpP.PaddedCount import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision /-! @@ -37,9 +39,14 @@ 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`. +`NTIME`, `BPTIME` and `PPTIME` are such classes too. The library reduces them to padded fair-coin +counts (`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`), and padded counts at a linear clock +are `SharpTIME enc T` functions (`Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`). +So `NTIME[T]` is a positivity test of one count, and `PPTIME[T]` and `BPTIME[T]` compare a count +`f` with the count `g = 2 ^ τ` of all coin strings by `g < 2 * f` +(`Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`, +`Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`). Their strict containments in +`DTIME[2 ^ T]` are instances of the same separation. ## Main results @@ -52,6 +59,8 @@ derived here. Their strict containments in `DTIME[2 ^ T]` are in `CountingSimula `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]`. +* `NTIME_ssubset_DTIME_two_pow`, `BPTIME_ssubset_DTIME_two_pow`, `PPTIME_ssubset_DTIME_two_pow`: + the strict containments of nondeterministic, bounded-error and majority time. ## References @@ -194,4 +203,52 @@ theorem CeqTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, m 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 +/-! ### Nondeterministic, bounded-error and majority time -/ + +private theorem computableInPolyTime_pos : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (0 < p.1)) (encPair encNat encNat) encBool := + ComputableInPolyTime.binary_lt' (ComputableInPolyTime.const 0) + (ComputableInPolyTime.fst encNat encNat) + +private theorem computableInPolyTime_lt_two_mul : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.2 < 2 * p.1)) (encPair encNat encNat) + encBool := + ComputableInPolyTime.binary_lt' (ComputableInPolyTime.snd encNat encNat) + (ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 2) + (ComputableInPolyTime.fst encNat encNat)) + +/-- `NTIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/ +private theorem NTIME_forall_mem_SharpTIME (hT : TimeConstructible T) {A : Set α} + (hA : A ∈ NTIME 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⟩ := exists_mem_SharpTIME_of_mem_NTIME hT hA + exact ⟨f, hf, f, hf, _, computableInPolyTime_pos, fun x => by simp [hA x]⟩ + +/-- `PPTIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/ +private theorem PPTIME_forall_mem_SharpTIME (hT : TimeConstructible T) {A : Set α} + (hA : A ∈ PPTIME 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⟩ := exists_mem_SharpTIME_of_mem_PPTIME hT hA + exact ⟨f, hf, g, hg, _, computableInPolyTime_lt_two_mul, fun x => by simp [hA x]⟩ + +/-- **`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_forall_mem_SharpTIME hT hTn fun _ => NTIME_forall_mem_SharpTIME hT + +/-- **`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_forall_mem_SharpTIME hT hTn fun _ hA => + PPTIME_forall_mem_SharpTIME hT (BPTIME_subset_PPTIME hA) + +/-- **`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_forall_mem_SharpTIME hT hTn fun _ => PPTIME_forall_mem_SharpTIME hT + end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean index 10dc7f685..9815e49cd 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean @@ -15,11 +15,10 @@ 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. +For time-constructible `T` with `max n 2 ≤ T n`, the counting simulation of #1833 places counting +classes such as `NTIME[T]`, `BPTIME[T]` and `PPTIME[T]` in +`⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`. That union lies in `DTIME[2 ^ T]` but does not exhaust it. +Hence every class inside it 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 @@ -36,9 +35,10 @@ is strictly contained in `DTIME[2 ^ T]` on bit strings. 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`). +The separation is applied in +`Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses` to every class +decided by polynomial-time tests of exact counts in `Cslib.Complexity.SharpTIME`: `⊕TIME[T]`, +`Mod_kTIME[T]`, `C₌TIME[T]`, and also `NTIME[T]`, `BPTIME[T]` and `PPTIME[T]`. ## Main results @@ -48,8 +48,6 @@ The same separation applies to every class decided by polynomial-time tests of e `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 @@ -156,25 +154,4 @@ theorem ssubset_DTIME_two_pow_of_subset_iUnion {𝒞 : Set (Set (List Bool))} ⟨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/SharpP/PaddedCount.lean b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean new file mode 100644 index 000000000..08cd722f4 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean @@ -0,0 +1,183 @@ +/- +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 +public import Complexity.Computability.Complexity.Classes.PP.Time +public import Complexity.Computability.Complexity.Classes.SharpP.Time +public import Complexity.Computability.Complexity.Classes.Time.AcceptCount +import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock +import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock +import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock + +/-! +# Padded coin counts in time-bounded counting + +The library reduces nondeterministic, bounded-error and majority time to the padded accepting +count of a fair-coin machine (`Turing.MultiTapePTM.acceptCount`): the number of coin strings of a +length `τ` whose replay outputs `[true]`, where a run that halts early ignores its remaining coins +(`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`, +`Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`, +`Turing.MultiTapePTM.decidesByMajorityInTime_iff`). `Cslib.Complexity.SharpTIME` counts accepting +terminal branches of native counting machines instead, without padding. + +For a time-constructible `T`, padded counts at a linear clock are `SharpTIME enc T` functions +(`Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`). The clock is +`τ n = c * 2 ^ Nat.size (T n)`, which lies between `c * (T n + 1)` and `c * (2 * T n + 1)`. A +deterministic phase writes it in unary within `O(T n)` steps +(`Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`). The counting machine +`Turing.MultiTapeCTM.PaddedClock.machine` then branches once per coin, continuing after the source +halts, until the clock is exhausted. The clock is chosen before the machine, so several counts +can share it. A clock exactly `c₁ * T n + c₂` would need an exact binary-to-unary conversion in +linear time; the rounded clock suffices below, because each characterization holds at every +clock of at least `c₁ * T n + c₂`. + +Hence: + +* `NTIME[T]` problems are positivity tests of one `SharpTIME[T]` count + (`Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`). +* `PPTIME[T]` and `BPTIME[T]` problems are comparisons `g a < 2 * f a` of two `SharpTIME[T]` + counts, where `g a = 2 ^ τ` is the count of a machine accepting every coin string + (`Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`, + `Cslib.Complexity.exists_mem_SharpTIME_of_mem_BPTIME`). + +The converse direction, from terminal counts to padded counts, is +`Turing.MultiTapeCTM.CountingChoice.acceptCount_table_of_halts`. + +## Main definitions + +* `Turing.MultiTapePTM.acceptAll`: the fair-coin table that emits `true` and halts. + +## Main results + +* `Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`: padded counts at a linear clock. +* `Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`, + `Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`, + `Cslib.Complexity.exists_mem_SharpTIME_of_mem_BPTIME`: the class-level count tests. +-/ + +public section + +namespace Turing.MultiTapePTM + +variable {k : ℕ} {State : Type} {input : List Bool} + +/-- A halted configuration ignores every coin. The same fact is public in +`Classes.LogSpace.Randomized`, which this module does not import. -/ +private theorem stepCoins_halted (M : MultiTapePTM k Bool State) {c : Cfg k Bool State input} + (h : c.state = none) (coins : List Bool) : M.stepCoins coins c = c := by + induction coins with + | nil => rfl + | cons bit coins ih => rw [stepCoins_cons, MultiTapeTM.step_of_halt h, ih] + +/-- The fair-coin table that emits `true` and halts at its first step, whatever the coin. -/ +@[expose] def acceptAll : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ _ := .step ⟨0, Fin.elim0, some true, none⟩ Empty.elim Empty.elim + +/-- Every coin string of positive length makes `acceptAll` accept. -/ +theorem acceptCount_acceptAll (input : List Bool) (n : ℕ) : + acceptAll.acceptCount input (n + 1) = 2 ^ (n + 1) := by + rw [acceptCount, Cslib.Complexity.acceptCount, Finset.filter_true_of_mem] + · simp + · intro w _ + have hstep : (acceptAll.withCoin (w 0)).toTM.step (Cfg.init acceptAll.initial input) = + ⟨none, 1, fun _ _ => none, fun _ => 0, [true]⟩ := by + rw [MultiTapeTM.step_of_state rfl, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr] + exact Cfg.ext rfl (by simp [acceptAll, MultiTapeMachine.Action.emptyOracleEquiv, + withCoin]) (funext fun i => i.elim0) (funext fun i => i.elim0) rfl + rw [List.ofFn_succ, runClosedCoins_eq_output_stepCoins, stepCoins_cons, hstep, + stepCoins_halted _ rfl] + simp + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing + +variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} {A : Set α} + +/-- **Padded counts at a linear clock are time-bounded terminal counts.** For a time-constructible +`T` and constants `c₁` and `c₂`, there is a clock `τ` with `c₁ * T n + c₂ ≤ τ n ≤ C * T n + C` +such that, for every fair-coin machine `M` with a binary alphabet and finitely many states, the +padded accepting count of `M` with `τ` coins lies in `SharpTIME enc T`. The clock does not depend +on `M`. -/ +theorem exists_clock_acceptCount_mem_SharpTIME (hT : TimeConstructible T) (c₁ c₂ : ℕ) : + ∃ τ : ℕ → ℕ, (∀ n, c₁ * T n + c₂ ≤ τ n) ∧ (∃ C, ∀ n, τ n ≤ C * T n + C) ∧ + ∀ {k : ℕ} {State : Type} [Finite State] (M : MultiTapePTM k Bool State), + (fun a => M.acceptCount (enc a) (τ (enc a).length)) ∈ SharpTIME enc T := by + obtain ⟨r, P, hP, prepare, C, hprepare⟩ := hT.exists_prepare_unaryClock (c₁ + c₂) + have hupper (n : ℕ) : (c₁ + c₂) * 2 ^ Nat.size (T n) ≤ + 2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) := by + have := Nat.mul_le_mul_left (c₁ + c₂) (two_pow_size_le (T n)) + have e : 2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) = + (c₁ + c₂) * (2 * T n + 1) + (c₁ + c₂) := by ring + omega + refine ⟨fun n => (c₁ + c₂) * 2 ^ Nat.size (T n), fun n => ?_, ⟨2 * (c₁ + c₂), hupper⟩, + fun {k State} _ M => ?_⟩ + · have h : (c₁ + c₂) * (T n + 1) ≤ (c₁ + c₂) * 2 ^ Nat.size (T n) := + Nat.mul_le_mul_left _ (Nat.lt_size_self _) + have e : (c₁ + c₂) * (T n + 1) = c₁ * T n + c₂ + (c₂ * T n + c₁) := by ring + rw [e] at h + change c₁ * T n + c₂ ≤ (c₁ + c₂) * 2 ^ Nat.size (T n) + omega + · let compiled := MultiTapeCTM.PaddedClock.compile M (prepare.extendTapes (Fin.natAddEmb k)) + refine ⟨C + 2 * (c₁ + c₂), C + 2 * (c₁ + c₂) + 1, k + r + 1, P ⊕ Option State, + inferInstance, compiled, MultiTapeCTM.PaddedClock.nonblocking_compile _ _, fun a => ?_⟩ + have hready := MultiTapePTM.PolynomialClock.prepare_runFrom (k := k) prepare (enc a) + (List.replicate ((c₁ + c₂) * 2 ^ Nat.size (T (enc a).length)) true) + (C * T (enc a).length + C) (hprepare (enc a)) + obtain ⟨hhalt, hcount⟩ := MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_compile M + (prepare.extendTapes (Fin.natAddEmb k)) (enc a) _ _ hready + have hle : C * T (enc a).length + C + ((c₁ + c₂) * 2 ^ Nat.size (T (enc a).length) + 1) ≤ + (C + 2 * (c₁ + c₂)) * T (enc a).length + (C + 2 * (c₁ + c₂) + 1) := by + have := hupper (enc a).length + have e : (C + 2 * (c₁ + c₂)) * T (enc a).length + (C + 2 * (c₁ + c₂) + 1) = + C * T (enc a).length + C + (2 * (c₁ + c₂) * T (enc a).length + 2 * (c₁ + c₂)) + 1 := by + ring + omega + refine ⟨hhalt.mono hle, ?_⟩ + change compiled.branchCount (· == [true]) _ _ = _ + rw [hhalt.branchCount_eq hle] + exact hcount + +/-- **`NTIME[T]` as a positive count.** For a time-constructible `T`, every problem in +`NTIME enc T` consists of the instances with a positive count `f a`, for some `f` in +`SharpTIME enc T`. -/ +theorem exists_mem_SharpTIME_of_mem_NTIME (hT : TimeConstructible T) (hA : A ∈ NTIME enc T) : + ∃ f ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ 0 < f a := by + obtain ⟨k, State, _, M, c₁, c₂, hM⟩ := exists_acceptCount_of_mem_NTIME hA + obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc) hT c₁ c₂ + exact ⟨_, hmem M, fun a => hM a _ (hτ _)⟩ + +/-- **`PPTIME[T]` as a comparison of two counts.** For a time-constructible `T`, every problem in +`PPTIME enc T` consists of the instances with `g a < 2 * f a`, for some `f` and `g` in +`SharpTIME enc T`. Here `f` counts accepting coin strings at a common linear clock `τ` and +`g a = 2 ^ τ` counts all of them. -/ +theorem exists_mem_SharpTIME_of_mem_PPTIME (hT : TimeConstructible T) (hA : A ∈ PPTIME enc T) : + ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ g a < 2 * f a := by + obtain ⟨c₁, c₂, k, State, _, M, hM⟩ := hA + obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc) hT c₁ (c₂ + 1) + refine ⟨_, hmem M, _, hmem MultiTapePTM.acceptAll, fun a => ?_⟩ + have hdecide := MultiTapePTM.decidesByMajorityInTime_iff.mp + (hM.mono (t' := fun a => τ (enc a).length) fun a => (Nat.le_succ _).trans (hτ _)) a + obtain ⟨m, hm⟩ : ∃ m, τ (enc a).length = m + 1 := + Nat.exists_eq_add_one.mpr (Nat.lt_of_lt_of_le (Nat.succ_pos _) (hτ _)) + rw [hdecide.2] + change _ ↔ MultiTapePTM.acceptAll.acceptCount (enc a) (τ (enc a).length) < _ + rw [hm, MultiTapePTM.acceptCount_acceptAll] + +/-- **`BPTIME[T]` as a comparison of two counts**, through `Cslib.Complexity.BPTIME_subset_PPTIME`. +-/ +theorem exists_mem_SharpTIME_of_mem_BPTIME (hT : TimeConstructible T) (hA : A ∈ BPTIME enc T) : + ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ g a < 2 * f a := + exists_mem_SharpTIME_of_mem_PPTIME hT (BPTIME_subset_PPTIME hA) + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean new file mode 100644 index 000000000..70c6bb308 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean @@ -0,0 +1,359 @@ +/- +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.Machines.Turing.MultiTape.Counting.Deterministic +public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Sequential +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount +import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic + +/-! +# Padded coin counts as terminal-path counts + +A closed fair-coin table counts the coin strings of a fixed length `τ` on which it outputs +`[true]` (`Turing.MultiTapePTM.acceptCount`). A run that halts early ignores its remaining coins, +so an accepting run of length `ℓ` contributes `2 ^ (τ - ℓ)` strings. A native counting machine +counts each terminal branch once (`Turing.MultiTapeCTM.acceptCount`). + +`Turing.MultiTapeCTM.PaddedClock.machine` turns the first count into the second. It keeps the +source tapes on its first `k` work tapes and a unary clock on its last work tape. While the +clock head reads `true`, it takes one of two transition occurrences, one per coin: it performs +the source action selected by that coin and advances the clock head. After the source halts, the +two occurrences only advance the clock. On the first cell that does not hold `true`, it halts +with a single occurrence and emits nothing. Thus a clock of `τ` cells has exactly one terminal +branch for each coin string of length `τ`, and that branch ends with the output of the coin +replay. + +`Turing.MultiTapeCTM.PaddedClock.compile` precedes this machine by a deterministic phase that +writes `τ` true cells on the clock tape and leaves every other tape blank. The time and +correctness of that phase are hypotheses here; the clock is prepared from a time-constructible +bound in `Complexity.Computability.Complexity.Classes.Constructible.UnaryClock`. + +## Main definitions + +* `Turing.MultiTapeCTM.PaddedClock.machine`: count coin strings under a prepared unary clock. +* `Turing.MultiTapeCTM.PaddedClock.compile`: prepare the clock, then count. + +## Main results + +* `Turing.MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_machine`: a clock of `n` cells halts + every branch within `n + 1` steps and counts the coin strings of length `n`. +* `Turing.MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_compile`: after a preparation of + `time` steps writing `τ` cells, every branch halts within `time + (τ + 1)` steps and the + terminal accepting count is the padded accepting count at `τ`. + +## References + +The unary clock tape follows `MultiTape.Machine.Clock`, whose controller does not pad halted +runs with branching choices. +-/ + +public section + +namespace Turing.MultiTapeCTM.PaddedClock + +open Cslib MultiTapeMachine + +variable {k r : ℕ} {State : Type} {input : List Bool} + +/-- The source action selected by a coin at a running source state. -/ +def coinAction (M : MultiTapePTM k Bool State) (state : State) (symbol : Option Bool) + (work : Fin k → Option Bool) (bit : Bool) : Turing.Action k Bool State := + Action.emptyOracleEquiv (M.tr state symbol work Empty.elim bit) + +/-- A source action on the first `k` work tapes, advancing the clock head on the last one. -/ +def lift (action : Turing.Action k Bool State) : + Turing.Action (k + r + 1) Bool (Option State) where + inputTape := action.inputTape + workTapes := Fin.lastCases (none, 1) (Fin.addCases action.workTapes fun _ => (none, 0)) + output := action.output + state := some action.state + +/-- After the source halts: advance the clock head and change nothing else. -/ +def tick : Turing.Action (k + r + 1) Bool (Option State) where + inputTape := 0 + workTapes := Fin.lastCases (none, 1) fun _ => (none, 0) + output := none + state := some none + +/-- Halt once the clock is exhausted, emitting nothing. -/ +def stop : Turing.Action (k + r + 1) Bool (Option State) where + inputTape := 0 + workTapes := fun _ => (none, 0) + output := none + state := none + +/-- The transition occurrences: one per coin while the clock head reads `true`, and a single halt +afterwards. A halted source keeps two occurrences per clock cell. -/ +def choices (M : MultiTapePTM k Bool State) (r : ℕ) (state : Option State) + (symbol : Option Bool) (work : Fin (k + r + 1) → Option Bool) : + List (Turing.Action (k + r + 1) Bool (Option State)) := + if work (Fin.last (k + r)) = some true then + match state with + | some state => [false, true].map fun bit => + lift (coinAction M state symbol (fun i => work (Fin.castAdd r i).castSucc) bit) + | none => [tick, tick] + else [stop] + +/-- **Padded coin counting.** Run a fair-coin table on the first `k` work tapes under the unary +clock on the last work tape, branching once per coin until the clock is exhausted. The control +state is the source state, `none` once the source has halted. -/ +def machine (M : MultiTapePTM k Bool State) (r : ℕ) : + MultiTapeCTM (k + r + 1) Bool (Option State) where + initial := some M.initial + tr state symbol work _ := (choices M r state symbol work).map Action.emptyOracleEquiv.symm + +/-- A source configuration on the first `k` work tapes, blank middle tapes, and the clock tape +`clock` with its head at `pos`. -/ +def config (r : ℕ) (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ) : + Cfg (k + r + 1) Bool (Option State) input where + state := some c.state + inputPos := c.inputPos + workTapes := Fin.lastCases clock (Fin.addCases c.workTapes fun _ _ => none) + workTapePos := Fin.lastCases pos (Fin.addCases c.workTapePos fun _ => 0) + output := c.output + +/-- No local view is stuck: some occurrence is always available. -/ +theorem nonblocking_machine (M : MultiTapePTM k Bool State) (r : ℕ) : + (machine M r).Nonblocking := by + intro state symbol work + simp only [machine, choices, ne_eq, List.map_eq_nil_iff] + split_ifs + · cases state <;> simp + · simp + +/-- The occurrences at a simulated configuration are the coin choices of its source state. -/ +theorem actions_config (M : MultiTapePTM k Bool State) (c : Cfg k Bool State input) + (clock : ℤ → Option Bool) (pos : ℤ) : + (machine M r).actions (config r c clock pos) = + choices M r c.state c.inputSymbol (config r c clock pos).workTapeSymbols := by + simp only [actions, config, machine, List.map_map] + rw [Equiv.self_comp_symm, List.map_id] + rfl + +@[simp] theorem workTapeSymbols_config_last (c : Cfg k Bool State input) + (clock : ℤ → Option Bool) (pos : ℤ) : + (config r c clock pos).workTapeSymbols (Fin.last (k + r)) = clock pos := by + simp [config, Cfg.workTapeSymbols] + +@[simp] theorem workTapeSymbols_config_source (c : Cfg k Bool State input) + (clock : ℤ → Option Bool) (pos : ℤ) (i : Fin k) : + (config r c clock pos).workTapeSymbols (Fin.castAdd r i).castSucc = c.workTapeSymbols i := by + simp [config, Cfg.workTapeSymbols] + +/-- A lifted source action acts on the source data and advances the clock head. -/ +theorem apply_lift (action : Turing.Action k Bool State) (c : Cfg k Bool State input) + (clock : ℤ → Option Bool) (pos : ℤ) : + (lift (r := r) action).apply (config r c clock pos) = + config r (action.apply c) clock (pos + 1) := by + refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext j <;> induction j using Fin.lastCases with + | last => simp [lift, config, Action.apply] + | cast j => + induction j using Fin.addCases with + | left i => + simp only [lift, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_left] + | right i => + simp only [lift, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_right, + SignType.coe_zero, add_zero] + +/-- After the source halts, a tick only advances the clock head. -/ +theorem apply_tick {c : Cfg k Bool State input} (hc : c.state = none) + (clock : ℤ → Option Bool) (pos : ℤ) : + (tick (k := k) (r := r) (State := State)).apply (config r c clock pos) = + config r c clock (pos + 1) := by + refine Cfg.ext (by simp [tick, config, hc]) (by simp [tick, config]) + ?_ ?_ (by simp [tick, config, Action.apply]) <;> + funext j <;> induction j using Fin.lastCases with + | last => simp [tick, config, Action.apply] + | cast j => + induction j using Fin.addCases with + | left i => + simp only [tick, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_left, + SignType.coe_zero, add_zero] + | right i => + simp only [tick, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_right, + SignType.coe_zero, add_zero] + +/-- The fixed-coin step of the source, in the notation of the coin replay. -/ +private theorem step_withCoin_of_state (M : MultiTapePTM k Bool State) + {c : Cfg k Bool State input} {state : State} (hc : c.state = some state) (bit : Bool) : + (M.withCoin bit).toTM.step c = + (coinAction M state c.inputSymbol c.workTapeSymbols bit).apply c := by + rw [MultiTapeTM.step_of_state hc, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr] + rfl + +/-- While the clock lasts, the occurrences are the two coins, each followed by the simulated +configuration after the corresponding coin step. -/ +private theorem actions_config_of_clock (M : MultiTapePTM k Bool State) + (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ) + (hpos : clock pos = some true) : + ∃ g : Bool → Turing.Action (k + r + 1) Bool (Option State), + (machine M r).actions (config r c clock pos) = [false, true].map g ∧ + ∀ bit, (g bit).apply (config r c clock pos) = + config r ((M.withCoin bit).toTM.step c) clock (pos + 1) := by + rw [actions_config] + cases hc : c.state with + | none => + refine ⟨fun _ => tick, ?_, fun bit => ?_⟩ + · simp [choices, hpos] + · rw [apply_tick hc, MultiTapeTM.step_of_halt hc] + | some state => + refine ⟨fun bit => lift (coinAction M state c.inputSymbol c.workTapeSymbols bit), ?_, + fun bit => ?_⟩ + · simp [choices, hpos] + · rw [apply_lift, step_withCoin_of_state M hc] + +/-- A terminal configuration counts once exactly when its output passes the verdict. -/ +private theorem branchCount_of_halted {State' : Type} (N : MultiTapeCTM (k + r + 1) Bool State') + {cfg : Cfg (k + r + 1) Bool State' input} (h : cfg.Halted) (verdict : List Bool → Bool) + (fuel : ℕ) : N.branchCount verdict fuel cfg = if verdict cfg.output then 1 else 0 := by + rw [← countP_runList, runList_halted _ h] + cases hv : verdict cfg.output <;> simp [h, hv] + +/-- The padded count splits over the first coin. -/ +theorem acceptCount_stepCoins_succ (M : MultiTapePTM k Bool State) (c : Cfg k Bool State input) + (n : ℕ) : + Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool => + decide ((M.stepCoins p.2 p.1).output = [true])) c (n + 1) = + Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool => + decide ((M.stepCoins p.2 p.1).output = [true])) ((M.withCoin false).toTM.step c) n + + Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool => + decide ((M.stepCoins p.2 p.1).output = [true])) ((M.withCoin true).toTM.step c) n := by + rw [show n + 1 = 1 + n from Nat.add_comm n 1, Complexity.acceptCount_add, + Fintype.sum_equiv (Equiv.funUnique (Fin 1) Bool) _ + (fun bit => Complexity.acceptCount (fun x : Cfg k Bool State input × List Bool => + decide ((M.stepCoins (bit :: x.2) x.1).output = [true])) c n) + (fun u => by simp [List.ofFn_succ]), + Fintype.sum_bool] + simp only [Complexity.acceptCount, MultiTapePTM.stepCoins_cons] + exact Nat.add_comm _ _ + +/-- **The counting phase.** With `n` true cells from the clock head on, every branch halts within +`n + 1` steps, and the accepting terminal branches are counted exactly by the coin strings of +length `n` whose replay outputs `[true]`. -/ +theorem haltsWithin_acceptCount_machine (M : MultiTapePTM k Bool State) (r n : ℕ) + (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ) + (hclock : ∀ i : ℕ, i < n → clock (pos + i) = some true) + (hstop : clock (pos + n) ≠ some true) : + (machine M r).HaltsWithin (n + 1) (config r c clock pos) ∧ + (machine M r).acceptCount (n + 1) (config r c clock pos) = + Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool => + decide ((M.stepCoins p.2 p.1).output = [true])) c n := by + induction n generalizing c pos with + | zero => + have hpos : clock pos ≠ some true := by simpa using hstop + have hact : (machine M r).actions (config r c clock pos) = [stop] := by + rw [actions_config] + simp [choices, hpos] + have hhalt : (stop (k := k) (r := r) (State := State)).apply (config r c clock pos) + |>.Halted := rfl + refine ⟨.step (by simp [hact]) fun index => ?_, ?_⟩ + · have hindex : ((machine M r).actions (config r c clock pos))[index] = stop := + List.mem_singleton.mp (hact ▸ List.getElem_mem index.isLt) + exact .halt (by rw [hindex]; exact hhalt) + · rw [acceptCount, ← countP_runList, runList_succ _ _ _ _ rfl, hact, + Complexity.acceptCount_zero] + by_cases hout : c.output = [true] <;> simp [stop, config, Action.apply, hout] + | succ n ih => + have hpos : clock pos = some true := by simpa using hclock 0 (Nat.succ_pos n) + have hnext (bit : Bool) := ih ((M.withCoin bit).toTM.step c) (pos + 1) + (fun i hi => by + have := hclock (i + 1) (by omega) + rwa [Nat.cast_add, Nat.cast_one, add_comm (i : ℤ) 1, ← add_assoc] at this) + (by + have := hstop + rwa [Nat.cast_add, Nat.cast_one, add_comm (n : ℤ) 1, ← add_assoc] at this) + obtain ⟨g, hact, hg⟩ := actions_config_of_clock (r := r) M c clock pos hpos + refine ⟨.step (by simp [hact]) fun index => ?_, ?_⟩ + · have hmem : ((machine M r).actions (config r c clock pos))[index] ∈ + [false, true].map g := by + rw [← hact] + exact List.getElem_mem index.isLt + obtain ⟨bit, -, hbit⟩ := List.mem_map.mp hmem + rw [← hbit, hg] + exact (hnext bit).1 + · rw [acceptCount_stepCoins_succ, acceptCount, ← countP_runList, + runList_succ _ _ _ _ rfl, hact, List.flatMap_map] + simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil, List.countP_append, hg] + rw [← (hnext false).2, ← (hnext true).2, acceptCount, acceptCount, ← countP_runList, + ← countP_runList] + +variable {P : Type} + +/-- **Prepare, then count.** A deterministic phase on all tapes prepares the clock; the counting +phase then runs the source from its initial configuration. -/ +noncomputable def compile (M : MultiTapePTM k Bool State) + (prepare : MultiTapeTM (k + r + 1) Bool P) : MultiTapeCTM (k + r + 1) Bool (P ⊕ Option State) := + (ofDeterministic prepare).seq (machine M r) + +theorem nonblocking_compile (M : MultiTapePTM k Bool State) + (prepare : MultiTapeTM (k + r + 1) Bool P) : (compile M prepare).Nonblocking := + (nonblocking_ofDeterministic prepare).seq (nonblocking_machine M r) + +/-- A prepared clock of `τ` cells is the initial source configuration under that clock. -/ +private theorem start_eq (M : MultiTapePTM k Bool State) (input : List Bool) (τ : ℕ) : + (wordsCfg input (none : Option P) + (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []).withState + (some (machine M r).initial) = + config r (Cfg.init M.initial input) (tapeOfList (List.replicate τ true)) 0 := by + refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext j <;> induction j using Fin.lastCases with + | last => simp [config, wordsCfg, Cfg.withState] + | cast j => + induction j using Fin.addCases with + | left i => + simp only [config, wordsCfg, Cfg.withState, Fin.lastCases_castSucc, Fin.addCases_left, + Cfg.init, Function.update_of_ne (Fin.castSucc_ne_last _), tapeOfList_nil] + | right i => + simp only [config, wordsCfg, Cfg.withState, Fin.lastCases_castSucc, Fin.addCases_right, + Function.update_of_ne (Fin.castSucc_ne_last _), tapeOfList_nil] + +/-- **Padded counts from a prepared clock.** If the preparation halts after `time` steps with +exactly `τ` true cells on the last work tape, every other tape blank and nothing emitted, then +every branch of the compiled machine halts within `time + (τ + 1)` steps, and its accepting +terminal count is the padded accepting count `M.acceptCount input τ`. -/ +theorem haltsWithin_acceptCount_compile (M : MultiTapePTM k Bool State) + (prepare : MultiTapeTM (k + r + 1) Bool P) (input : List Bool) (time τ : ℕ) + (hprepare : prepare.runFrom (prepare.initCfg input) time = + wordsCfg input none + (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []) : + (compile M prepare).HaltsWithin (time + (τ + 1)) (Cfg.init (compile M prepare).initial input) ∧ + (compile M prepare).acceptCount (time + (τ + 1)) + (Cfg.init (compile M prepare).initial input) = M.acceptCount input τ := by + set first := ofDeterministic prepare with hfirst_def + set cfg := first.initialConfig input with hcfg_def + have hready : prepare.runFrom cfg.tapes time = wordsCfg input none + (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) [] := hprepare + have hfirst : first.HaltsWithin time cfg.tapes := by + rw [haltsWithin_ofDeterministic_iff, hready] + rfl + have hrun : first.runList time cfg.tapes = [wordsCfg input none + (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []] := by + rw [runList_ofDeterministic, hready] + have hclock := haltsWithin_acceptCount_machine M r τ (Cfg.init M.initial input) + (tapeOfList (List.replicate τ true)) 0 (fun i hi => by simp [hi]) (by simp) + have hsecond : ∀ result ∈ first.runList time cfg.tapes, + (machine M r).HaltsWithin (τ + 1) (result.withState (some (machine M r).initial)) := by + intro result hresult + rw [hrun, List.mem_singleton] at hresult + rw [hresult, start_eq] + exact hclock.1 + have hstart : Cfg.init (compile M prepare).initial input = + (Sequential.left (machine M r) cfg).tapes := rfl + refine ⟨hstart ▸ HaltsWithin.seq (nonblocking_ofDeterministic prepare) (nonblocking_machine M r) + cfg time (τ + 1) hfirst hsecond, ?_⟩ + rw [hstart, acceptCount, ← countP_runList, + show compile M prepare = first.seq (machine M r) from rfl, + runList_seq first (machine M r) cfg time (τ + 1) hfirst hsecond, hrun, List.flatMap_singleton, + List.countP_map, start_eq] + have hcount := hclock.2 + rw [acceptCount, ← countP_runList] at hcount + simp only [Function.comp_def, Cfg.mapState, Option.isNone_map] + rw [hcount, MultiTapePTM.acceptCount] + simp only [Complexity.acceptCount, MultiTapePTM.runClosedCoins_eq_output_stepCoins] + +end Turing.MultiTapeCTM.PaddedClock diff --git a/ComplexityTests/PaddedCount.lean b/ComplexityTests/PaddedCount.lean new file mode 100644 index 000000000..e5679119c --- /dev/null +++ b/ComplexityTests/PaddedCount.lean @@ -0,0 +1,86 @@ +/- +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.SharpP.PaddedCount +import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock +import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock +import ComplexityTests.CountingSeparation + +/-! # Padded coin counts as `SharpTIME` functions: checked instances + +The unary clock of `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`, the padded +count bridge and the class-level count tests, at the clock `T n = (n + 1) ^ 2 + 1`. The +always-accepting table gives a nonvacuous instance: its padded count is positive. -/ + +namespace ComplexityTests.PaddedCount + +open Cslib.Complexity Turing ComplexityTests.CountingSeparation + +/-! ### The clock -/ + +/-- The rounded clock is between `c * (m + 1)` and `c * (2 * m + 1)`. -/ +example (c m : ℕ) : c * (m + 1) ≤ c * 2 ^ Nat.size m ∧ c * 2 ^ Nat.size m ≤ c * (2 * m + 1) := + ⟨Nat.mul_le_mul_left c (Nat.lt_size_self m), Nat.mul_le_mul_left c (two_pow_size_le m)⟩ + +example : ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State) + (C : ℕ), ∀ input, + machine.runFrom (machine.initCfg input) (C * ((input.length + 1) ^ 2 + 1) + C) = + wordsCfg input none (Function.update (fun _ => []) (Fin.last r) + (List.replicate (3 * 2 ^ Nat.size ((input.length + 1) ^ 2 + 1)) true)) [] := + timeConstructible_succ_sq_add_one.exists_prepare_unaryClock 3 + +/-! ### The always-accepting table -/ + +example : MultiTapePTM.acceptAll.acceptCount [true, false] 3 = 8 := + MultiTapePTM.acceptCount_acceptAll _ 2 + +example : MultiTapePTM.acceptAll.acceptCount [] 0 = 0 := by + rw [MultiTapePTM.acceptCount, acceptCount_zero] + rfl + +/-! ### The bridge -/ + +/-- A padded count at a linear clock is a positive `SharpTIME` function. -/ +example {α : Type} {enc : α ↪ List Bool} : + ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, 0 < f a := by + obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc) + timeConstructible_succ_sq_add_one 0 1 + refine ⟨_, hmem MultiTapePTM.acceptAll, fun a => ?_⟩ + obtain ⟨m, hm⟩ : ∃ m, τ (enc a).length = m + 1 := + Nat.exists_eq_add_one.mpr (Nat.lt_of_lt_of_le (by norm_num) (hτ (enc a).length)) + simp only [hm, MultiTapePTM.acceptCount_acceptAll] + positivity + +/-- The counting phase alone: a clock of `n` cells and the coin strings of length `n`. -/ +example {k : ℕ} {State : Type} (M : MultiTapePTM k Bool State) (input : List Bool) (n : ℕ) : + (MultiTapeCTM.PaddedClock.machine M 0).acceptCount (n + 1) + (MultiTapeCTM.PaddedClock.config 0 (Cfg.init M.initial input) + (tapeOfList (List.replicate n true)) 0) = + M.acceptCount input n := by + rw [(MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_machine M 0 n _ _ 0 + (fun i hi => by simp [hi]) (by simp)).2, MultiTapePTM.acceptCount] + simp only [Cslib.Complexity.acceptCount, MultiTapePTM.runClosedCoins_eq_output_stepCoins] + +/-! ### Count tests for nondeterministic, majority and bounded-error time -/ + +example {α : Type} {enc : α ↪ List Bool} {A : Set α} + (hA : A ∈ NTIME enc fun n => (n + 1) ^ 2 + 1) : + ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ 0 < f a := + exists_mem_SharpTIME_of_mem_NTIME timeConstructible_succ_sq_add_one hA + +example {α : Type} {enc : α ↪ List Bool} {A : Set α} + (hA : A ∈ PPTIME enc fun n => (n + 1) ^ 2 + 1) : + ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), + ∃ g ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ g a < 2 * f a := + exists_mem_SharpTIME_of_mem_PPTIME timeConstructible_succ_sq_add_one hA + +example {α : Type} {enc : α ↪ List Bool} {A : Set α} + (hA : A ∈ BPTIME enc fun n => (n + 1) ^ 2 + 1) : + ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), + ∃ g ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ g a < 2 * f a := + exists_mem_SharpTIME_of_mem_BPTIME timeConstructible_succ_sq_add_one hA + +end ComplexityTests.PaddedCount From 8131f79fd8c456085666186b2fe638f809e4f4d7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:46:53 -0400 Subject: [PATCH 4/5] 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) := From fc10e7f35d68faeb801b0e713fee3003c9f74de8 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 13:05:52 -0400 Subject: [PATCH 5/5] refactor(SharpP): private tidy clock helper; share replay and doubling facts Address review on #2068. - `ComputableTidilyInO.mul_two_pow_length` is private to `UnaryClock.lean`; the public result stays the plain `TimeConstructible.exists_prepare_unaryClock`. - New `Foundations/Data/Nat/Doubling.lean` with `List.foldl_add_self_eq_mul_two_pow` and `Nat.two_pow_size_le`, replacing the copies in `UnaryClock`, `LogSpace/CounterProgram/Unary` and `Complexity/Quantitative`. - New `Probabilistic/HaltedReplay.lean` with `MultiTapePTM.step_withCoin_of_halted` and `MultiTapePTM.stepCoins_of_halted` (moved from `Classes/LogSpace/Randomized.lean` and generalized over the alphabet) and `MultiTapePTM.acceptAll` with `acceptCount_acceptAll` (moved from `SharpP/PaddedCount.lean`). The private copy in `PaddedCount` is gone. - Remove the unused private `branchCount_of_halted` from `Counting/PaddedClock.lean`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Classes/Constructible/UnaryClock.lean | 47 +++--------- .../Classes/LogSpace/Randomized.lean | 13 +--- .../Classes/SharpP/PaddedCount.lean | 42 +---------- .../LogSpace/CounterProgram/Unary.lean | 13 +--- .../MultiTape/Complexity/Quantitative.lean | 7 +- .../MultiTape/Counting/PaddedClock.lean | 7 -- .../MultiTape/Probabilistic/HaltedReplay.lean | 74 +++++++++++++++++++ Complexity/Foundations/Data/Nat/Doubling.lean | 54 ++++++++++++++ ComplexityTests/PaddedCount.lean | 4 +- 10 files changed, 154 insertions(+), 109 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean create mode 100644 Complexity/Foundations/Data/Nat/Doubling.lean diff --git a/Complexity.lean b/Complexity.lean index 7f40dc9c3..951648520 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2018,6 +2018,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.E public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Table public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.TablePolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount.PolyTime @@ -2947,6 +2948,7 @@ public import Complexity.Foundations.Data.Nat.CeilDiv public import Complexity.Foundations.Data.Nat.Choose public import Complexity.Foundations.Data.Nat.Choose.Real public import Complexity.Foundations.Data.Nat.Div +public import Complexity.Foundations.Data.Nat.Doubling public import Complexity.Foundations.Data.Nat.Factorial public import Complexity.Foundations.Data.Nat.IntermediateValue public import Complexity.Foundations.Data.Nat.Log diff --git a/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean index c03599f82..c16cc6a9a 100644 --- a/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean +++ b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Complexity.Classes.Constructible public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.OutputToTape import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming +import Complexity.Foundations.Data.Nat.Doubling import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes import Complexity.Computability.Machines.Turing.MultiTape.Run @@ -25,9 +26,8 @@ from binary to unary by counting down takes `O((T n + 1) ^ 2)` steps Rounding up to a power of two avoids the conversion. The binary word of `T n` has `Nat.size (T n)` digits, and doubling a unary counter once per digit writes `c * 2 ^ Nat.size (T n)` cells. The `i`-th doubling costs `O(c * 2 ^ i)`, so the doublings cost -`O(c * 2 ^ Nat.size (T n)) = O(T n + 1)` together -(`Turing.MultiTapeTM.ComputableTidilyInO.mul_two_pow_length`). The rounded clock lies between -`c * (T n + 1)` and `c * (2 * T n + 1)`. +`O(c * 2 ^ Nat.size (T n)) = O(T n + 1)` together. The rounded clock lies between +`c * (T n + 1)` and `c * (2 * T n + 1)` (`Nat.two_pow_size_le`). `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock` packages this as one deterministic machine that writes the clock on its last work tape within `O(T n)` steps, leaving every other @@ -36,8 +36,6 @@ budget of `MultiTape.Plumbing.PrepareClock`. ## Main results -* `Turing.MultiTapeTM.ComputableTidilyInO.mul_two_pow_length`: `c * 2 ^ l.length` in unary within - time `O(c * 2 ^ l.length + l.length)`. * `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`: a unary clock of `c * 2 ^ Nat.size (T n)` cells within `O(T n)` steps. -/ @@ -46,15 +44,6 @@ public section namespace Turing.MultiTapeTM.ComputableTidilyInO -/-- Doubling a counter once per element of a list multiplies it by `2 ^ length`. -/ -private theorem foldl_double {α : Type} (l : List α) (m : ℕ) : - l.foldl (fun m _ => m + m) m = m * 2 ^ l.length := by - induction l generalizing m with - | nil => simp - | cons a l ih => - rw [List.foldl_cons, ih, List.length_cons, pow_succ] - ring - /-- The geometric sum of powers of two below `2 ^ n`. -/ private theorem sum_range_two_pow_lt (n : ℕ) : ∑ i ∈ Finset.range n, 2 ^ i < 2 ^ n := by induction n with @@ -65,15 +54,16 @@ private theorem sum_range_two_pow_lt (n : ℕ) : ∑ i ∈ Finset.range n, 2 ^ i /-- **`c * 2 ^ l.length` in unary in linear time.** A streaming fold doubles a unary counter once per bit of `l`. Round `i` costs `O(c * 2 ^ i)`, so the rounds cost `O(c * 2 ^ l.length)` in total, -plus `O(l.length)` for the scan. -/ -theorem mul_two_pow_length (c : ℕ) : +plus `O(l.length)` for the scan. The tidy realization is private to this file; the public result +is the plain preparation theorem below. -/ +private theorem mul_two_pow_length (c : ℕ) : ComputableTidilyInO (fun l : List Bool => c * 2 ^ l.length) encBits encUnary (fun l => c * 2 ^ l.length + l.length) fun l => c * 2 ^ l.length + l.length := by obtain ⟨c₀, hstep, -⟩ := ((ComputableInDegree.unaryAdd (ComputableInDegree.fst encUnary encBool) (ComputableInDegree.fst encUnary encBool) le_rfl le_rfl).inO_one).tidy have hstate (l : List Bool) (i : ℕ) (hi : i ≤ l.length) : (encUnary ((l.take i).foldl (fun m _ => m + m) c)).length = c * 2 ^ i := by - rw [foldl_double, encUnary_apply, List.length_replicate, List.length_take, + rw [List.foldl_add_self_eq_mul_two_pow, encUnary_apply, List.length_replicate, List.length_take, Nat.min_eq_left hi] obtain ⟨K, hK⟩ := ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum (enc := encUnary) (step := fun m (_ : Bool) => m + m) c hstep @@ -95,8 +85,8 @@ theorem mul_two_pow_length (c : ℕ) : rw [hstate l i hi] exact Nat.mul_le_mul_left c (Nat.pow_le_pow_right (by norm_num) hi)) refine of_bounds (hK.of_enc_eq (g := fun l : List Bool => c * 2 ^ l.length) - fun l => by rw [foldl_double]) (K * (5 * c₀ + 5) + K * (3 * c₀ + 3) + 1) (fun l => ?_) - (fun l => ?_) fun l => ?_ + fun l => by rw [List.foldl_add_self_eq_mul_two_pow]) + (K * (5 * c₀ + 5) + K * (3 * c₀ + 3) + 1) (fun l => ?_) (fun l => ?_) fun l => ?_ · have hsum := sum_range_two_pow_lt l.length have hs : ∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) ≤ (5 * c₀ + 4) * (c * 2 ^ l.length + l.length) := by @@ -135,24 +125,11 @@ namespace Cslib.Complexity open Turing Turing.MultiTapeTM -/-- `2 ^ Nat.size m` is the least power of two above `m`, so it is at most `2 * m + 1`. -/ -theorem two_pow_size_le (m : ℕ) : 2 ^ Nat.size m ≤ 2 * m + 1 := by - rcases Nat.eq_zero_or_pos m with rfl | hm - · simp - · have hsize : 0 < Nat.size m := Nat.size_pos.mpr hm - have hle : 2 ^ (Nat.size m - 1) ≤ m := Nat.lt_size.mp (by omega) - have : 2 ^ Nat.size m = 2 * 2 ^ (Nat.size m - 1) := by - rw [← pow_succ'] - congr 1 - omega - omega - /-- **A unary clock of linear length.** For a time-constructible `T` and a constant `c`, one deterministic machine with finitely many states writes `c * 2 ^ Nat.size (T n)` true cells on its last work tape within `C * T n + C` steps, on every input of length `n`. It halts with every other work tape blank, all heads at their starting cells and nothing emitted. The clock has between -`c * (T n + 1)` and `c * (2 * T n + 1)` cells (`Nat.lt_size_self`, -`Cslib.Complexity.two_pow_size_le`). -/ +`c * (T n + 1)` and `c * (2 * T n + 1)` cells (`Nat.lt_size_self`, `Nat.two_pow_size_le`). -/ theorem TimeConstructible.exists_prepare_unaryClock {T : ℕ → ℕ} (hT : TimeConstructible T) (c : ℕ) : ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State) @@ -171,7 +148,7 @@ theorem TimeConstructible.exists_prepare_unaryClock {T : ℕ → ℕ} (hT : Time rw [encNat_apply, Nat.size_eq_bits_len] have hlinear (x : List Bool) : T x.length + (c * 2 ^ (encNat (T x.length)).length + (encNat (T x.length)).length) ≤ (2 * c + 2) * (T x.length + 1) := by - have h₁ := Nat.mul_le_mul_left c (two_pow_size_le (T x.length)) + have h₁ := Nat.mul_le_mul_left c (Nat.two_pow_size_le (T x.length)) have h₂ : Nat.size (T x.length) ≤ T x.length := Nat.size_le.mpr Nat.lt_two_pow_self rw [hdigits] have e : (2 * c + 2) * (T x.length + 1) = c * (2 * T x.length + 1) + c + @@ -185,7 +162,7 @@ theorem TimeConstructible.exists_prepare_unaryClock {T : ℕ → ℕ} (hT : Time have hbound : c₁ * (T input.length + 1) + (List.replicate (c * 2 ^ Nat.size (T input.length)) true).length + 2 ≤ (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) := by - have h₁ := Nat.mul_le_mul_left c (two_pow_size_le (T input.length)) + have h₁ := Nat.mul_le_mul_left c (Nat.two_pow_size_le (T input.length)) rw [List.length_replicate] have e : (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) = c₁ * (T input.length + 1) + c * (2 * T input.length + 1) + c + 2 * T input.length + 2 := by diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean index a1f91e687..2a206c82a 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.HaltingTime public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay /-! # Randomized logarithmic space @@ -84,18 +85,6 @@ noncomputable def acceptCoins (input : List Bool) (t : ℕ) : ℕ := theorem acceptCoins_le (input : List Bool) (t : ℕ) : machine.acceptCoins input t ≤ 2 ^ t := (Finset.card_filter_le _ _).trans (by simp) -/-- A halted configuration ignores its coin. -/ -theorem step_withCoin_of_halted {input : List Bool} {c : Cfg k Bool State input} (h : c.Halted) - (bit : Bool) : (machine.withCoin bit).toTM.step c = c := - MultiTapeTM.step_iff.mp ((MultiTapeNTM.step_of_halt h).mpr rfl) - -/-- A halted configuration ignores any further coins. -/ -theorem stepCoins_of_halted {input : List Bool} {c : Cfg k Bool State input} (h : c.Halted) - (coins : List Bool) : machine.stepCoins coins c = c := by - induction coins with - | nil => rfl - | cons bit coins ih => rw [stepCoins_cons, step_withCoin_of_halted machine h, ih] - /-- Under a time bound `t`, every replay of `t` or more coins ends halted. -/ theorem halted_stepCoins {input : List Bool} {t : ℕ} (ht : machine.toNTM.RunsInTime input t) {coins : List Bool} (hlen : t ≤ coins.length) : diff --git a/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean index 08cd722f4..25023433e 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean @@ -14,7 +14,9 @@ public import Complexity.Computability.Complexity.Classes.Time.AcceptCount import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock +import Complexity.Foundations.Data.Nat.Doubling /-! # Padded coin counts in time-bounded counting @@ -50,10 +52,6 @@ Hence: The converse direction, from terminal counts to padded counts, is `Turing.MultiTapeCTM.CountingChoice.acceptCount_table_of_halts`. -## Main definitions - -* `Turing.MultiTapePTM.acceptAll`: the fair-coin table that emits `true` and halts. - ## Main results * `Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`: padded counts at a linear clock. @@ -64,40 +62,6 @@ The converse direction, from terminal counts to padded counts, is public section -namespace Turing.MultiTapePTM - -variable {k : ℕ} {State : Type} {input : List Bool} - -/-- A halted configuration ignores every coin. The same fact is public in -`Classes.LogSpace.Randomized`, which this module does not import. -/ -private theorem stepCoins_halted (M : MultiTapePTM k Bool State) {c : Cfg k Bool State input} - (h : c.state = none) (coins : List Bool) : M.stepCoins coins c = c := by - induction coins with - | nil => rfl - | cons bit coins ih => rw [stepCoins_cons, MultiTapeTM.step_of_halt h, ih] - -/-- The fair-coin table that emits `true` and halts at its first step, whatever the coin. -/ -@[expose] def acceptAll : MultiTapePTM 0 Bool Unit where - initial := () - tr _ _ _ _ _ := .step ⟨0, Fin.elim0, some true, none⟩ Empty.elim Empty.elim - -/-- Every coin string of positive length makes `acceptAll` accept. -/ -theorem acceptCount_acceptAll (input : List Bool) (n : ℕ) : - acceptAll.acceptCount input (n + 1) = 2 ^ (n + 1) := by - rw [acceptCount, Cslib.Complexity.acceptCount, Finset.filter_true_of_mem] - · simp - · intro w _ - have hstep : (acceptAll.withCoin (w 0)).toTM.step (Cfg.init acceptAll.initial input) = - ⟨none, 1, fun _ _ => none, fun _ => 0, [true]⟩ := by - rw [MultiTapeTM.step_of_state rfl, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr] - exact Cfg.ext rfl (by simp [acceptAll, MultiTapeMachine.Action.emptyOracleEquiv, - withCoin]) (funext fun i => i.elim0) (funext fun i => i.elim0) rfl - rw [List.ofFn_succ, runClosedCoins_eq_output_stepCoins, stepCoins_cons, hstep, - stepCoins_halted _ rfl] - simp - -end Turing.MultiTapePTM - namespace Cslib.Complexity open _root_.Turing @@ -116,7 +80,7 @@ theorem exists_clock_acceptCount_mem_SharpTIME (hT : TimeConstructible T) (c₁ obtain ⟨r, P, hP, prepare, C, hprepare⟩ := hT.exists_prepare_unaryClock (c₁ + c₂) have hupper (n : ℕ) : (c₁ + c₂) * 2 ^ Nat.size (T n) ≤ 2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) := by - have := Nat.mul_le_mul_left (c₁ + c₂) (two_pow_size_le (T n)) + have := Nat.mul_le_mul_left (c₁ + c₂) (Nat.two_pow_size_le (T n)) have e : 2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) = (c₁ + c₂) * (2 * T n + 1) + (c₁ + c₂) := by ring omega diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean index e23bd6f32..5ffb28cc6 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame +import Complexity.Foundations.Data.Nat.Doubling import Mathlib.Data.List.GetD import Mathlib.Data.Nat.Bitwise import Mathlib.Data.Nat.Size @@ -155,14 +156,6 @@ private theorem bits_eq_map_testBit (v : ℕ) : v.bits = (List.range v.size).map refine List.ext_getElem (by simp [Nat.size_eq_bits_len]) fun i h _ => ?_ simp [Nat.testBit_eq_inth, List.getI_eq_getElem _ h] -private theorem two_pow_size_le (v : ℕ) : 2 ^ v.size ≤ 2 * v + 1 := by - rcases Nat.eq_zero_or_pos v with rfl | hv - · simp - · obtain ⟨s, hs⟩ : ∃ s, v.size = s + 1 := ⟨v.size - 1, by have := Nat.size_pos.mpr hv; omega⟩ - have : 2 ^ s ≤ v := Nat.lt_size.mp (by omega) - rw [hs, pow_succ] - omega - /-- The loop of `binaryProgram`, from the power `2 ^ i`, emits the bits of `v` from index `i` on below its size. -/ private theorem reachesOut_binaryLoop (e : Expr) {v : ℕ} (hB : 2 * a + 1 + b ≤ B) @@ -170,7 +163,7 @@ private theorem reachesOut_binaryLoop (e : Expr) {v : ℕ} (hB : 2 * a + 1 + b ∀ i ≤ v.size, (binaryProgram e).ReachesOut (encPair encUnary encUnary (a, b)) ((binaryProgram e).Active B) (6, [a, b, 2 ^ i, v]) (11, [a, b, 2 ^ v.size, v]) ((List.range' i (v.size - i)).map v.testBit) := by - have hsize := two_pow_size_le v + have hsize := Nat.two_pow_size_le v intro i hi induction h : v.size - i generalizing i with | zero => @@ -266,7 +259,7 @@ theorem computableInLogSpace_binary (e : Expr) (d : ℕ) (he : ∀ a b, e.eval [ rw [length_input] obtain ⟨h₁, h₂⟩ := le_pow_add_two (n := 2 * a + 1 + b) (by omega) ((hF a b).trans (Nat.pow_le_pow_left (by omega) d)) - have hsize := two_pow_size_le (F a b) + have hsize := Nat.two_pow_size_le (F a b) refine ⟨_, _, [], reachesOut_binaryProgram e (he a b) (by omega) h₂, rfl, by simp [encNat_apply], bounded4 (by omega) (by omega) (by omega) (by omega)⟩ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean index aac57a6a7..c225959c2 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Equali public import Mathlib.Tactic.FunProp import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition +import Complexity.Foundations.Data.Nat.Doubling import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring @@ -688,11 +689,7 @@ theorem lengthUnary : ComputableInO (fun l : List Bool => l.length) encBits encU /-- Doubling `m` once for each element of a list of length `n` multiplies it by `2 ^ n`. -/ private theorem foldl_double (n m : ℕ) : (List.replicate n true).foldl (fun m _ => m + m) m = m * 2 ^ n := by - induction n generalizing m with - | zero => simp - | succ n ih => - rw [List.replicate_succ, List.foldl_cons, ih] - ring + rw [List.foldl_add_self_eq_mul_two_pow, List.length_replicate] /-- **`2 ^ n` in unary**, by doubling `n` times, within time `O((n + 1) * 2 ^ n)` and space `O(2 ^ n)`. -/ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean index 70c6bb308..871b6e552 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean @@ -208,13 +208,6 @@ private theorem actions_config_of_clock (M : MultiTapePTM k Bool State) · simp [choices, hpos] · rw [apply_lift, step_withCoin_of_state M hc] -/-- A terminal configuration counts once exactly when its output passes the verdict. -/ -private theorem branchCount_of_halted {State' : Type} (N : MultiTapeCTM (k + r + 1) Bool State') - {cfg : Cfg (k + r + 1) Bool State' input} (h : cfg.Halted) (verdict : List Bool → Bool) - (fuel : ℕ) : N.branchCount verdict fuel cfg = if verdict cfg.output then 1 else 0 := by - rw [← countP_runList, runList_halted _ h] - cases hv : verdict cfg.output <;> simp [h, hv] - /-- The padded count splits over the first coin. -/ theorem acceptCount_stepCoins_succ (M : MultiTapePTM k Bool State) (c : Cfg k Bool State input) (n : ℕ) : diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean new file mode 100644 index 000000000..927db50ec --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean @@ -0,0 +1,74 @@ +/- +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.Machines.Turing.MultiTape.Probabilistic.AcceptCount + +/-! +# Replays after halting + +A halted configuration of a fair-coin table ignores its coin +(`Turing.MultiTapePTM.step_withCoin_of_halted`) and every further coin +(`Turing.MultiTapePTM.stepCoins_of_halted`). So a table that halts at its first step decides +every coin string at once: the table `Turing.MultiTapePTM.acceptAll`, which emits `true` and +halts, accepts all `2 ^ τ` coin strings of every positive length `τ` +(`Turing.MultiTapePTM.acceptCount_acceptAll`). + +## Main definitions + +* `Turing.MultiTapePTM.acceptAll`: the fair-coin table that emits `true` and halts. + +## Main results + +* `Turing.MultiTapePTM.step_withCoin_of_halted`, `Turing.MultiTapePTM.stepCoins_of_halted`: a + halted configuration ignores its coins. +* `Turing.MultiTapePTM.acceptCount_acceptAll`: `acceptAll` accepts every coin string of positive + length. +-/ + +public section + +namespace Turing.MultiTapePTM + +variable {k : ℕ} {Symbol State : Type} {input : List Symbol} + +/-- A halted configuration ignores its coin. -/ +theorem step_withCoin_of_halted (machine : MultiTapePTM k Symbol State) + {c : Cfg k Symbol State input} (h : c.Halted) (bit : Bool) : + (machine.withCoin bit).toTM.step c = c := + MultiTapeTM.step_of_halt h + +/-- A halted configuration ignores any further coins. -/ +theorem stepCoins_of_halted (machine : MultiTapePTM k Symbol State) + {c : Cfg k Symbol State input} (h : c.Halted) (coins : List Bool) : + machine.stepCoins coins c = c := by + induction coins with + | nil => rfl + | cons bit coins ih => rw [stepCoins_cons, step_withCoin_of_halted machine h, ih] + +/-- The fair-coin table that emits `true` and halts at its first step, whatever the coin. -/ +@[expose] def acceptAll : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ _ := .step ⟨0, Fin.elim0, some true, none⟩ Empty.elim Empty.elim + +/-- Every coin string of positive length makes `acceptAll` accept. -/ +theorem acceptCount_acceptAll (input : List Bool) (n : ℕ) : + acceptAll.acceptCount input (n + 1) = 2 ^ (n + 1) := by + rw [acceptCount, Cslib.Complexity.acceptCount, Finset.filter_true_of_mem] + · simp + · intro w _ + have hstep : (acceptAll.withCoin (w 0)).toTM.step (Cfg.init acceptAll.initial input) = + ⟨none, 1, fun _ _ => none, fun _ => 0, [true]⟩ := by + rw [MultiTapeTM.step_of_state rfl, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr] + exact Cfg.ext rfl (by simp [acceptAll, MultiTapeMachine.Action.emptyOracleEquiv, + withCoin]) (funext fun i => i.elim0) (funext fun i => i.elim0) rfl + rw [List.ofFn_succ, runClosedCoins_eq_output_stepCoins, stepCoins_cons, hstep, + stepCoins_of_halted _ rfl] + simp + +end Turing.MultiTapePTM diff --git a/Complexity/Foundations/Data/Nat/Doubling.lean b/Complexity/Foundations/Data/Nat/Doubling.lean new file mode 100644 index 000000000..1eec7ee01 --- /dev/null +++ b/Complexity/Foundations/Data/Nat/Doubling.lean @@ -0,0 +1,54 @@ +/- +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.Init +public import Mathlib.Data.Nat.Size +import Mathlib.Tactic.Ring + +/-! +# Powers of two by doubling + +Doubling a counter once per element of a list multiplies it by `2 ^ length` +(`List.foldl_add_self_eq_mul_two_pow`), and the least power of two above `n`, `2 ^ Nat.size n`, +is at most `2 * n + 1` (`Nat.two_pow_size_le`). Together they bound unary counters built by +doubling once per binary digit. + +## Main results + +* `List.foldl_add_self_eq_mul_two_pow`: `l.foldl (fun m _ => m + m) m = m * 2 ^ l.length`. +* `Nat.two_pow_size_le`: `2 ^ Nat.size n ≤ 2 * n + 1`. +-/ + +public section + +namespace List + +/-- Doubling a counter once per element of a list multiplies it by `2 ^ length`. -/ +theorem foldl_add_self_eq_mul_two_pow {α : Type*} (l : List α) (m : ℕ) : + l.foldl (fun m _ => m + m) m = m * 2 ^ l.length := by + induction l generalizing m with + | nil => simp + | cons a l ih => + rw [List.foldl_cons, ih, List.length_cons, pow_succ] + ring + +end List + +namespace Nat + +/-- `2 ^ Nat.size n` is the least power of two above `n`, so it is at most `2 * n + 1`. -/ +theorem two_pow_size_le (n : ℕ) : 2 ^ n.size ≤ 2 * n + 1 := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + · obtain ⟨s, hs⟩ : ∃ s, n.size = s + 1 := ⟨n.size - 1, by have := Nat.size_pos.mpr hn; omega⟩ + have : 2 ^ s ≤ n := Nat.lt_size.mp (by omega) + rw [hs, pow_succ] + omega + +end Nat diff --git a/ComplexityTests/PaddedCount.lean b/ComplexityTests/PaddedCount.lean index e5679119c..b94cb5909 100644 --- a/ComplexityTests/PaddedCount.lean +++ b/ComplexityTests/PaddedCount.lean @@ -7,6 +7,8 @@ Authors: Samuel Schlesinger import Complexity.Computability.Complexity.Classes.SharpP.PaddedCount import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay +import Complexity.Foundations.Data.Nat.Doubling import ComplexityTests.CountingSeparation /-! # Padded coin counts as `SharpTIME` functions: checked instances @@ -23,7 +25,7 @@ open Cslib.Complexity Turing ComplexityTests.CountingSeparation /-- The rounded clock is between `c * (m + 1)` and `c * (2 * m + 1)`. -/ example (c m : ℕ) : c * (m + 1) ≤ c * 2 ^ Nat.size m ∧ c * 2 ^ Nat.size m ≤ c * (2 * m + 1) := - ⟨Nat.mul_le_mul_left c (Nat.lt_size_self m), Nat.mul_le_mul_left c (two_pow_size_le m)⟩ + ⟨Nat.mul_le_mul_left c (Nat.lt_size_self m), Nat.mul_le_mul_left c (Nat.two_pow_size_le m)⟩ example : ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State) (C : ℕ), ∀ input,