feat(complexity): add fixed-clock deterministic promise completions

Complexity.lean

@@ -1178,6 +1178,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Fas
 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.Promise
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Separation
 public import Complexity.Computability.Complexity.Classes.DP
 public import Complexity.Computability.Complexity.Classes.EXP
@@ -1306,9 +1307,11 @@ public import Complexity.Computability.Complexity.Classes.ParityP
 public import Complexity.Computability.Complexity.Classes.ParityP.Closure
 public import Complexity.Computability.Complexity.Classes.Promise.Basic
 public import Complexity.Computability.Complexity.Classes.Promise.Circuit
+public import Complexity.Computability.Complexity.Classes.Promise.PP
 public import Complexity.Computability.Complexity.Classes.Promise.Probabilistic
 public import Complexity.Computability.Complexity.Classes.Promise.Randomized
 public import Complexity.Computability.Complexity.Classes.Promise.Reduction
+public import Complexity.Computability.Complexity.Classes.Promise.Time
 public import Complexity.Computability.Complexity.Classes.RP
 public import Complexity.Computability.Complexity.Classes.RP.Closure
 public import Complexity.Computability.Complexity.Classes.RepeatedTrials

Complexity/Computability/Complexity/Classes/Constructible.lean

@@ -41,6 +41,7 @@ length is supplied by the quantitative API (`Turing.MultiTapeTM.ComputableInO.le
 * `Cslib.Complexity.timeConstructible_two_pow`,
   `Cslib.Complexity.timeConstructible_two_pow_two_pow`,
   `Cslib.Complexity.timeConstructible_succ_pow`,
+  `Cslib.Complexity.TimeConstructible.succ`,
   `Cslib.Complexity.TimeConstructible.succ_mul`: time-constructible bounds.
 * `Cslib.Complexity.spaceConstructible_const`, `Cslib.Complexity.spaceConstructible_id`,
   `Cslib.Complexity.spaceConstructible_succ`, `Cslib.Complexity.spaceConstructible_succ_pow`,
@@ -101,6 +102,16 @@ theorem TimeConstructible.of_computableInO {t : ℕ → ℕ} {T S : List Bool 
   · simp only [encBits_apply]
     exact Nat.mul_le_mul_left k (Nat.add_le_add_right (hS x) 1)
 
+/-- Adding one to a time-constructible bound preserves time constructibility. -/
+theorem TimeConstructible.succ {t : ℕ → ℕ} (ht : TimeConstructible t) :
+    TimeConstructible fun n => t n + 1 := by
+  have h := (ComputableInO.of_linear ComputableInLinearTimeAndSpace.natSucc).comp
+    ht.computableInO
+  refine TimeConstructible.of_computableInO (s := fun n => t n + (encNat (t n)).length) 2 h
+    (fun x => ?_) fun _ => le_rfl
+  have hlen := length_encNat_le (t x.length)
+  omega
+
 /-- `2 ^ n` is time-constructible: its binary digits are `n` zeros followed by a one. -/
 theorem timeConstructible_two_pow : TimeConstructible (2 ^ ·) :=
   TimeConstructible.of_computableInO 1

Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastSimulation
+public import Complexity.Computability.Complexity.Classes.Promise.Time
+
+/-!
+# Deterministic promise completions at a prescribed clock
+
+A native bounded-error promise solver running in time `T` has a strict-majority completion in
+`PPTIME T`, at the same clock. The unconditional counting simulation then gives one deterministic
+machine deciding that completion in time `2 ^ (C T / √⌊log₂ T⌋)` and workspace `T ^ d`.
+The caller supplies `T`, its constructibility and `max n 2 ≤ T n`. Only the simulation constants
+are existential: the time scale cannot be weakened by choosing a larger polynomial afterward.
+
+Answers outside the promise are unrestricted. This is not a bounded-error total completion.
+The verifier-defined `PromiseBPP` completion in `PP` is separately proved in `Promise.PP`;
+no clock-preserving equivalence between that verifier definition and `PromiseBPTIME` is asserted.
+
+## Main results
+
+* `exists_completion_of_mem_PromiseBPTIME`: one deterministic completion with the prescribed
+  subexponential time and independent polynomial-workspace bounds.
+-/
+
+public section
+
+namespace Cslib.Complexity.CountingSimulation
+
+open _root_.Turing.MultiTapeTM
+
+/-- A native promise problem at caller-supplied time `T` has a deterministic completion within
+`2 ^ O(T / √log T)` time and polynomial workspace, with one realizing machine. -/
+theorem exists_completion_of_mem_PromiseBPTIME {α : Type} {enc : α ↪ List Bool}
+    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n)
+    {Q : PromiseProblem α} (hQ : Q ∈ PromiseBPTIME enc T) :
+    ∃ (L : Set α) (C d : ℕ), Q.yes ⊆ L ∧ Disjoint L Q.no ∧
+      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) := by
+  obtain ⟨L, hL, hyes, hno⟩ := PromiseBPTIME_subset_promiseClass_PPTIME hQ
+  obtain ⟨C, d, h⟩ :=
+    exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_PPTIME hT hTn hL
+  exact ⟨L, C, d, hyes, hno, h⟩
+
+end Cslib.Complexity.CountingSimulation

Complexity/Computability/Complexity/Classes/PP.lean

@@ -38,6 +38,8 @@ characterisation by fair-coin machines deciding by strict majority within polyno
 
 ## Main results
 
+* `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.solvedBy_majority`: bounded error
+  gives a strict-majority solver on the promise.
 * `Cslib.Complexity.DecidesWithBoundedError.decidesByMajority`: bounded error gives a majority.
 * `Cslib.Complexity.BPP_subset_PP`.
 
@@ -74,24 +76,37 @@ theorem mem_PP {A : Set α} : A ∈ PP enc ↔ ∃ (p : Polynomial ℕ) (V : α
     ComputableInPolyTime V (encPair enc encBits) encBool ∧ DecidesByMajority enc p V A :=
   Iff.rfl
 
+/-- A bounded-error verifier solves its promise problem by strict majority. Ties reject, and
+there is no error-margin requirement outside the promise. -/
+theorem PromiseProblem.SolvesWithBoundedError.solvedBy_majority {p : Polynomial ℕ}
+    {V : α × List Bool → Bool} {Q : PromiseProblem α}
+    (h : Q.SolvesWithBoundedError enc p V) :
+    Q.SolvedBy (fun a => decide
+      (2 ^ p.eval (enc a).length < 2 * acceptCount V a (p.eval (enc a).length))) := by
+  constructor
+  · intro a ha
+    have hyes := (h a).1 ha
+    have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length)
+    unfold BoundedErrorAt at hyes
+    rw [← acceptCount] at hyes
+    simp only [decide_eq_true_eq]
+    omega
+  · intro a ha
+    have hno := (h a).2 ha
+    have hsum := acceptCount_add_card_filter_eq_false
+      (V := V) (a := a) (n := p.eval (enc a).length)
+    unfold BoundedErrorAt at hno
+    simp only [decide_eq_false_iff_not]
+    omega
+
 /-- Bounded error gives a majority: a decider that is right on at least two thirds of the random
 strings accepts the members of its problem, and only them, on more than half. -/
 theorem DecidesWithBoundedError.decidesByMajority {p : Polynomial ℕ} {V : α × List Bool → Bool}
     {A : Set α} (h : DecidesWithBoundedError enc p V A) : DecidesByMajority enc p V A := by
   intro a
-  have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length)
-  have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length)
-  constructor
-  · intro ha
-    have := (h a).1 ha
-    unfold BoundedErrorAt at this
-    rw [← acceptCount] at this
-    omega
-  · intro hlt
-    by_contra ha
-    have := (h a).2 ha
-    unfold BoundedErrorAt at this
-    omega
+  simpa only [decide_eq_true_eq] using
+    (PromiseProblem.solvedBy_ofSet.mp
+      (PromiseProblem.SolvesWithBoundedError.solvedBy_majority h) a)
 
 /-- **`BPP ⊆ PP`.** -/
 theorem BPP_subset_PP : BPP enc ⊆ PP enc :=

Complexity/Computability/Complexity/Classes/Promise/PP.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.PP
+public import Complexity.Computability.Complexity.Classes.Promise.Basic
+
+/-!
+# Strict-majority completions of bounded-error promise problems
+
+A verifier for `PromiseBPP` gives a language in `PP` separating its yes- and no-instances:
+accept exactly when strictly more than half of its random strings are accepted. This is a direct
+consequence of the existing bounded-error and strict-majority definitions. Ties are rejected;
+outside the promise, no bounded-error margin is asserted for the completion.
+
+## Main results
+
+* `Cslib.Complexity.PromiseBPP_subset_promiseClass_PP`: every bounded-error promise problem
+  has a strict-majority completion in `PP`.
+-/
+
+public section
+
+namespace Cslib.Complexity
+
+open Turing.MultiTapeTM
+
+/-- Every problem in `PromiseBPP` has a completion in `PP`, using the same seeded verifier.
+The completion accepts by strict majority, including on inputs outside the promise. -/
+theorem PromiseBPP_subset_promiseClass_PP {α : Type} {enc : α ↪ List Bool} :
+    PromiseBPP enc ⊆ promiseClass (PP enc) := by
+  rintro Q ⟨p, V, hV, hQ⟩
+  let L : Set α := {a | 2 ^ p.eval (enc a).length <
+    2 * acceptCount V a (p.eval (enc a).length)}
+  have hsolve := hQ.solvedBy_majority
+  refine ⟨L, ⟨p, V, hV, fun _ => Iff.rfl⟩, ?_, ?_⟩
+  · intro a ha
+    exact of_decide_eq_true (hsolve.1 a ha)
+  · refine Set.disjoint_right.mpr fun a ha hL => ?_
+    have hno := hsolve.2 a ha
+    simp only [decide_eq_false_iff_not] at hno
+    exact hno hL
+
+end Cslib.Complexity

Complexity/Computability/Complexity/Classes/Promise/Time.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.PP.Time
+public import Complexity.Computability.Complexity.Classes.Promise.Basic
+
+/-!
+# Bounded-error promise computation at a prescribed time
+
+`PromiseBPTIME enc T` fixes a native fair-coin machine and an affine clock `c₁ * T n + c₂`
+before the input. Every run halts within that clock, including off-promise runs. On yes-instances
+the output is `[true]` with probability at least `2/3`, and on no-instances it is `[false]` with
+probability at least `2/3`. No probability gap or answer is required outside the promise.
+
+This is the library's time-indexed native-machine convention, extending `BPTIME` to partial
+promises. It does not define the class through bounded-error total completions. A strict-majority
+completion belongs to `PPTIME` at the same caller-supplied clock, with ties rejecting; this is not
+a bounded-error completion in `BPTIME`.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime`: native clock and error contract.
+* `Cslib.Complexity.PromiseBPTIME`: bounded-error promise computation in affine time.
+
+## Main results
+
+* `PromiseBPTIME_mono`: increasing the time bound preserves membership.
+* `promiseClass_BPTIME_subset_PromiseBPTIME`: total bounded-error completions give witnesses.
+* `PromiseBPTIME_subset_promiseClass_PPTIME`: a strict-majority completion at the same time scale.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+open Cslib.Complexity
+
+variable {α : Type} {k : ℕ} {State : Type}
+
+/-- Every run halts by `t`; bounded error is required only on the two sides of the promise. -/
+@[expose] def SolvesPromiseWithBoundedErrorInTime (machine : MultiTapePTM k Bool State)
+    (enc : α ↪ List Bool) (Q : PromiseProblem α) (t : α → ℕ) : Prop :=
+  ∀ a, (∀ final ∈ (Cslib.ProbComp.eval
+      (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support,
+      final.tapes.state = none) ∧
+    (a ∈ Q.yes → 2 / 3 ≤ Cslib.ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) ∧
+    (a ∈ Q.no → 2 / 3 ≤ Cslib.ProbComp.eval (machine.runClosed (t a) (enc a)) [false])
+
+/-- A sufficiently long clock may be enlarged without changing the output law. -/
+theorem SolvesPromiseWithBoundedErrorInTime.mono
+    {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q : PromiseProblem α}
+    {t t' : α → ℕ} (h : machine.SolvesPromiseWithBoundedErrorInTime enc Q t)
+    (ht : ∀ a, t a ≤ t' a) : machine.SolvesPromiseWithBoundedErrorInTime enc Q t' := by
+  intro a
+  obtain ⟨hhalt, hyes, hno⟩ := h a
+  refine ⟨?_, ?_⟩
+  · rw [machine.eval_runClosedConfigFrom_eq_of_halted _ (ht a) hhalt]
+    exact hhalt
+  · rw [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt]
+    exact ⟨hyes, hno⟩
+
+end Turing.MultiTapePTM
+
+namespace Cslib.Complexity
+
+open _root_.Turing _root_.Turing.MultiTapeTM
+open scoped ENNReal
+
+variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ}
+
+/-- Native bounded-error promise problems with fixed machine parameters and affine time `T`.
+All encoded inputs terminate, but the error conditions only constrain promised inputs. -/
+@[expose] def PromiseBPTIME (enc : α ↪ List Bool) (T : ℕ → ℕ) : Set (PromiseProblem α) :=
+  {Q | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State)
+    (machine : MultiTapePTM k Bool State),
+      machine.SolvesPromiseWithBoundedErrorInTime enc Q fun a => c₁ * T (enc a).length + c₂}
+
+/-- Membership is monotone in the caller's time bound. -/
+theorem PromiseBPTIME_mono {T₁ T₂ : ℕ → ℕ} (h : ∀ n, T₁ n ≤ T₂ n) :
+    PromiseBPTIME enc T₁ ⊆ PromiseBPTIME enc T₂ := by
+  rintro Q ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩
+  exact ⟨c₁, c₂, k, State, hfinite, machine, hQ.mono fun a =>
+    Nat.add_le_add_right (Nat.mul_le_mul_left _ (h _)) _⟩
+
+/-- A bounded-error total completion supplies a native bounded-error promise solver. -/
+theorem promiseClass_BPTIME_subset_PromiseBPTIME :
+    promiseClass (BPTIME enc T) ⊆ PromiseBPTIME enc T := by
+  rintro Q ⟨L, ⟨c₁, c₂, k, State, hfinite, machine, hL⟩, hyes, hno⟩
+  refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hL a).1, ?_, ?_⟩⟩
+  · intro ha
+    simpa only [indicator, hyes ha, ↓reduceIte] using (hL a).2
+  · intro ha
+    have hnot : a ∉ L := fun h => Set.disjoint_right.mp hno ha h
+    simpa only [indicator, hnot, ↓reduceIte] using (hL a).2
+
+/-- Accepting by strict majority completes the promise in `PPTIME` without changing its clock.
+The completion may have an exact tie outside the promise; it need not belong to `BPTIME`. -/
+theorem PromiseBPTIME_subset_promiseClass_PPTIME :
+    PromiseBPTIME enc T ⊆ promiseClass (PPTIME enc T) := by
+  rintro Q ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩
+  let L : Set α := {a | 1 / 2 <
+    ProbComp.eval (machine.runClosed (c₁ * T (enc a).length + c₂) (enc a)) [true]}
+  have hhalf : (1 / 2 : ℝ≥0∞) < 2 / 3 := by
+    refine (ENNReal.toReal_lt_toReal (ENNReal.div_ne_top (by norm_num) (by norm_num))
+      (ENNReal.div_ne_top (by norm_num) (by norm_num))).mp ?_
+    simp only [ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_ofNat]
+    norm_num
+  refine ⟨L, ⟨c₁, c₂, k, State, hfinite, machine,
+    fun a => ⟨(hQ a).1, Iff.rfl⟩⟩, ?_, ?_⟩
+  · intro a ha
+    exact hhalf.trans_le ((hQ a).2.1 ha)
+  · refine Set.disjoint_right.mpr fun a ha hL => ?_
+    let p := ProbComp.eval (machine.runClosed (c₁ * T (enc a).length + c₂) (enc a))
+    have hsum : p [true] + p [false] ≤ 1 := by
+      simpa only [Finset.sum_pair (by decide : ([true] : List Bool) ≠ [false]), PMF.tsum_coe] using
+        (sum_le_tsum ({[true], [false]} : Finset (List Bool)) (f := fun w => p w))
+    have hfalse : (1 / 2 : ℝ≥0∞) ≤ p [false] := hhalf.le.trans ((hQ a).2.2 ha)
+    have hlt := ENNReal.add_lt_add_right (by norm_num : (1 / 2 : ℝ≥0∞) ≠ ⊤) hL
+    rw [ENNReal.add_halves] at hlt
+    exact (hlt.trans_le ((add_le_add le_rfl hfalse).trans hsum)).false
+
+end Cslib.Complexity