feat(CountingSimulation): counting classes from #TIME and NTIME/BPTIME/PPTIME ⊊ DTIME[2^T]

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,21 @@ 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.Bounds
+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 +1232,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

Complexity/Computability/Complexity/Classes/CeqP/Time.lean

@@ -0,0 +1,72 @@
+/-
+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; the larger clock serves both
+(`Cslib.Complexity.SharpTIME_pow_mono`).
+
+## 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⟩
+
+/-- **`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_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⟩
+
+end Cslib.Complexity

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