diff --git a/Complexity.lean b/Complexity.lean index 7dc496b6c..4858a3031 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1149,6 +1149,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Con 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.DP diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/BlockNetworks.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/BlockNetworks.lean index 719f8f5f8..c1ee6df5d 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/BlockNetworks.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/BlockNetworks.lean @@ -29,8 +29,9 @@ of the counting simulation (milestone H3 of #1833), so the conditional class con `Complexity.Computability.Complexity.Classes.CountingSimulation.Containments` hold assuming only a contraction algorithm. The joint time-and-space forms keep a single deciding machine within time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`, for a time-constructible -`T` with `max n 2 ≤ T n`. The contraction algorithm remains an explicit hypothesis; this -module does not prove the unconditional simulation. +`T` with `max n 2 ≤ T n`. The contraction algorithm remains an explicit hypothesis here; +`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two` and its +siblings discharge it with the contraction algorithm of Theorem D.1. **The family.** At the input `x`, the clock `t` and the schedule number `σ`, the network (`Cslib.Complexity.CountingSimulation.blockNetworkOf`) is the explicit block-counting network diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean index 81ed2bcab..02af1ea07 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean @@ -34,6 +34,9 @@ The network hypothesis is discharged for explicit networks by `Cslib.Complexity.CountingSimulation.networkFamilies_explicitAdmissible`, so the containments hold assuming only a contraction algorithm (`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_of_contractionAlgorithm` and its +siblings). The contraction algorithm of Theorem D.1 discharges that hypothesis too, which gives the +containments unconditionally +(`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two` and its siblings). ## Main definitions diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean index f5b6d411c..805a16171 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean @@ -36,6 +36,8 @@ by `FastContraction.wfChildren_nativeMk` and `FastContraction.packetShape_child` * `Cslib.Complexity.CountingSimulation.fastLeaves`: the leaf bounds. * `Cslib.Complexity.CountingSimulation.fastAnalysis_nativeMk_holds`: the resource analysis of the native recursion. +* `Cslib.Complexity.CountingSimulation.fastContractionAlgorithm`: the contraction algorithm of + Theorem D.1 for admissible explicit networks. ## References @@ -143,4 +145,13 @@ and, from some size on, its nodes fit in the clock. -/ theorem fastAnalysis_nativeMk_holds : FastAnalysis nativeMk := fastAnalysis_nativeMk fastLeaves +/-- **The contraction algorithm of Theorem D.1** for admissible explicit networks: the native +recursion behind a guard, with direct summation for the networks the guard rejects, in time +`poly(n) 2 ^ O(s / √⌊log₂ s⌋)` and polynomial space. -/ +noncomputable def fastContractionAlgorithm : + ContractionAlgorithm (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat + ExplicitTensorNetwork.encExplicitNetwork) + (fun G => G.2.contraction) ExplicitAdmissible := + contractionAlgorithmOfNative fastAnalysis_nativeMk_holds + end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean new file mode 100644 index 000000000..9e5d30b25 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastSimulation.lean @@ -0,0 +1,94 @@ +/- +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.BlockNetworks +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves + +/-! +# 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 +deterministic machine in time `2 ^ (C T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`. + +## Main results + +* `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. +* `exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_NTIME`, + `exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_BPTIME`, + `exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_PPTIME`: joint time and space. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} + +/-- **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) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (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_decidableInTimeAndSpace_of_mem_NTIME_of_contractionAlgorithm fastContractionAlgorithm hT + hTn hL + +/-- **Bounded-error probabilistic 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_BPTIME + (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ BPTIME enc T) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (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_decidableInTimeAndSpace_of_mem_BPTIME_of_contractionAlgorithm fastContractionAlgorithm hT + hTn hL + +/-- **Strict-majority probabilistic 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_PPTIME + (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ PPTIME enc T) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (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_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm fastContractionAlgorithm hT + hTn hL + +/-- **`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) + (hTn : ∀ n, max n 2 ≤ T n) : + NTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + NTIME_subset_iUnion_DTIME_of_contractionAlgorithm fastContractionAlgorithm hT hTn + +/-- **`BPTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for time-constructible `T` with +`max n 2 ≤ T n`. -/ +theorem BPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + BPTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + BPTIME_subset_iUnion_DTIME_of_contractionAlgorithm fastContractionAlgorithm hT hTn + +/-- **`PPTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`** for time-constructible `T` with +`max n 2 ≤ T n`. -/ +theorem PPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + PPTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + PPTIME_subset_iUnion_DTIME_of_contractionAlgorithm fastContractionAlgorithm hT hTn + +end Cslib.Complexity.CountingSimulation diff --git a/ComplexityTests/FastLeaves.lean b/ComplexityTests/FastLeaves.lean index 03914e387..2e205e997 100644 --- a/ComplexityTests/FastLeaves.lean +++ b/ComplexityTests/FastLeaves.lean @@ -36,4 +36,9 @@ example (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call) -- The resource analysis of the native recursion holds, with no remaining hypothesis. example : FastAnalysis nativeMk := fastAnalysis_nativeMk_holds +-- The contraction algorithm of Theorem D.1, with no remaining hypothesis. +noncomputable example : ContractionAlgorithm (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat + ExplicitTensorNetwork.encExplicitNetwork) (fun G => G.2.contraction) ExplicitAdmissible := + fastContractionAlgorithm + end ComplexityTests.FastLeaves diff --git a/ComplexityTests/FastSimulation.lean b/ComplexityTests/FastSimulation.lean new file mode 100644 index 000000000..5f090f964 --- /dev/null +++ b/ComplexityTests/FastSimulation.lean @@ -0,0 +1,52 @@ +/- +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.FastSimulation +import Complexity.Computability.Complexity.Classes.Constructible.Log + +/-! # 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`. -/ + +namespace ComplexityTests.FastSimulation + +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) + +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))) := + NTIME_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} : + BPTIME 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))) := + BPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two timeConstructible_succ_sq_add_one + max_le_succ_sq_add_one + +-- One machine within both bounds, for strict-majority time. +example {α : Type} {enc : α ↪ List Bool} {L : Set α} + (hL : L ∈ PPTIME enc fun n => (n + 1) ^ 2 + 1) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (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_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_PPTIME + timeConstructible_succ_sq_add_one max_le_succ_sq_add_one hL + +end ComplexityTests.FastSimulation