feat(CountingSimulation): unconditional SharpTIME ⊆ FTIME in time 2^O(T/√log T) (#1833)

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)

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))) :=

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