feat(Classes/CountingSimulation): NTIME, BPTIME and PPTIME in time 2^O(T/√log T) and polynomial space, unconditionally

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

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

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

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

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

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

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