From 415d328669b3160ba61fec83eb334ada48a05af9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 07:56:51 -0400 Subject: [PATCH 1/5] feat(Classes/Time): explicit-time verifier characterization of NTIME (#1572) Guess and verify within explicit time (`setOf_exists_mem_NTIME`), through a closed fair-coin composition with the new framed sampler `pairSampler`, and a linear-time verifier for every problem in `NTIME` (`exists_verifier_of_mem_NTIME`). Infrastructure toward the nondeterministic time hierarchy. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Time/Verifier.lean | 266 +++++++++++++++++ .../MultiTape/Probabilistic/PairSampler.lean | 268 ++++++++++++++++++ .../NondeterministicTimeVerifiers.lean | 85 ++++++ 4 files changed, 621 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/Time/Verifier.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean create mode 100644 ComplexityTests/NondeterministicTimeVerifiers.lean diff --git a/Complexity.lean b/Complexity.lean index d8146fc83f..7eddad2ea2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1327,6 +1327,7 @@ public import Complexity.Computability.Complexity.Classes.Tally public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial +public import Complexity.Computability.Complexity.Classes.Time.Verifier public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting public import Complexity.Computability.Complexity.Classes.Toda.Hierarchy @@ -1990,6 +1991,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.O public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Oracle public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputPrefix public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputToTape +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryBounds public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryTake diff --git a/Complexity/Computability/Complexity/Classes/Time/Verifier.lean b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean new file mode 100644 index 0000000000..89b4f594ab --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean @@ -0,0 +1,266 @@ +/- +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.Time +import Complexity.Computability.Complexity.Classes.NP.Nondeterministic +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput +import Complexity.Computability.Machines.Turing.MultiTape.Run +import Complexity.Probability.BitString +import Complexity.Probability.PMF.Bind + +/-! +# Nondeterministic time through verifiers, with explicit bounds + +This module characterizes `Cslib.Complexity.NTIME enc t` by deterministic verifiers, keeping the +time bound up to constant factors. The polynomial characterization of `NP` +(`Cslib.Complexity.mem_NP_iff_decidableInPolyTime`) loses the degree in both directions. The +two directions here keep it. + +* **Guess and verify** (`Cslib.Complexity.setOf_exists_mem_NTIME`). Suppose a verifier `V` is + computable within time `T (a, w)` on encoded pairs, and a certificate length `ℓ a` is + computable in unary within time `Tℓ a`. Then the problem + `{a | ∃ w, w.length = ℓ a ∧ V (a, w) = true}` lies in `NTIME enc t` whenever + `(enc a).length + Tℓ a + T (a, w)` is within `O(t (enc a).length)` on certificates of that + length. The certificate length may depend on the instance, not only on its encoded length. + The machine is the nondeterministic reading of a closed fair-coin composition: + - a deterministic machine writes `frame (enc a)` followed by `ℓ` ones; + - the fixed sampler `Turing.MultiTapePTM.pairSampler` copies the framed instance and replaces + the ones by fair coins; + - a deterministic machine runs the verifier. + + Its computation paths are exactly the coin replays, so it accepts exactly when some + certificate is accepted, and every branch halts within the composed clock. +* **Verifiers from nondeterministic time** (`Cslib.Complexity.exists_verifier_of_mem_NTIME`). + A problem in `NTIME enc t` has a verifier that is computable in linear time on encoded pairs: + check that the certificate, read as coins of the choice table + (`Turing.MultiTapeNTM.checkChoices`), replays an accepting computation. Every certificate + length of at least `c * t (enc a).length + c` works, for a constant `c`. + +These are explicit-time forms of the guess-and-verify characterization of nondeterministic +polynomial time [Arora and Barak][AroraBarak09]: the choices of an accepting computation are a +certificate, and a certificate can be guessed and then checked. + +## Main results + +* `Cslib.Complexity.setOf_exists_mem_NTIME`: guess and verify within explicit time. +* `Cslib.Complexity.exists_verifier_of_mem_NTIME`: a linear-time verifier for a problem in + `NTIME`, with certificates of every sufficient length. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- **Guess and verify, within explicit time.** If a verifier `V` is computable within time +`T (a, w)` on encoded pairs, and the certificate length `ℓ a` is computable in unary within time +`Tℓ a`, then the problem of instances with an accepted certificate of that length is in +`NTIME enc t`, provided `(enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C` for every +certificate `w` of that length. -/ +theorem setOf_exists_mem_NTIME {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} + {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} + (hℓ : ComputableInO ℓ enc encUnary Tℓ Sℓ) + (hV : ComputableInO V (encPair enc encBits) encBool T S) + (ht : ∀ a w, w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : + {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} ∈ NTIME enc t := by + -- the deterministic preparation and the verifier, as machines + obtain ⟨c₁, ⟨k₁, Q₁, _, tm₁, h₁⟩, -⟩ := + (ComputableInO.of_eq (f := fun a : α => a) (encIn := enc) (encMid := enc) fun _ => rfl).prod hℓ + obtain ⟨c₃, ⟨k₃, Q₃, _, tm₃, h₃⟩, -⟩ := hV + let L (a : α) : ℕ := ℓ a + let u (a : α) : List Bool := frame (enc a) ++ List.replicate (L a) true + let t₁ (a : α) : ℕ := c₁ * ((enc a).length + Tℓ a + 1) + let t₂ (a : α) : ℕ := (u a).length + 1 + let t₃ (a : α) : ℕ := c₃ * (C * t (enc a).length + C + 1) + have hrun₁ (a : α) := (h₁ a).runFrom_of_le (le_refl (t₁ a)) + have hlen₁ (a : α) : (u a).length ≤ t₁ a := (h₁ a).length_output_le + -- the first phase writes the framed instance and the unary certificate length + let M₁ : MultiTapePTM k₁ Bool Q₁ := MultiTapePTM.ofDeterministic tm₁ + have hfirst₁ (a : α) : ∀ final ∈ (ProbComp.eval + (M₁.runClosedConfigFrom (t₁ a) (M₁.initialConfig (enc a)))).support, + final.tapes.state = none := by + intro final hfinal + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₁ a).1 + have hout₁ (a : α) : ProbComp.eval (M₁.runClosed (t₁ a) (enc a)) = PMF.pure (u a) := by + rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₁ a).2] + rfl + -- the sampler copies the framed instance and guesses the certificate + have hsecond₁ (a : α) : ∀ word ∈ (ProbComp.eval (M₁.runClosed (t₁ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (MultiTapePTM.pairSampler.runClosedConfigFrom (t₂ a) + (MultiTapePTM.pairSampler.initialConfig word))).support, final.tapes.state = none := by + intro word hword + rw [hout₁ a, PMF.mem_support_pure_iff] at hword + subst hword + exact MultiTapePTM.pairSampler_halted (enc a) (List.replicate (L a) true) + let P₁₂ := MultiTapePTM.pairSampler.comp M₁ false + let t₁₂ (a : α) : ℕ := t₁ a + (t₁ a + 4 + t₂ a) + have heval₁₂ (a : α) : ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a)) = + (BitString.uniformList (L a)).map (frame (enc a) ++ ·) := by + rw [MultiTapePTM.eval_comp M₁ MultiTapePTM.pairSampler false (enc a) (t₁ a) (t₂ a) + (hfirst₁ a) (hsecond₁ a), hout₁ a, Probability.PMF.monad_bind_eq_bind, PMF.pure_bind] + simpa only [List.length_replicate, u] using + MultiTapePTM.eval_pairSampler (enc a) (List.replicate (L a) true) + have hhalt₁₂ (a : α) := MultiTapePTM.comp_halted M₁ MultiTapePTM.pairSampler false (enc a) + (t₁ a) (t₂ a) (hfirst₁ a) (hsecond₁ a) + -- the verifier runs on every guessed pair within the uniform clock `t₃` + let M₃ : MultiTapePTM k₃ Bool Q₃ := MultiTapePTM.ofDeterministic tm₃ + have hrun₃ (a : α) (w : List Bool) (hw : w.length = L a) := + (h₃ (a, w)).runFrom_of_le (J := t₃ a) (Nat.mul_le_mul_left c₃ (by + have := ht a w hw + omega)) + have hword (a : α) {word : List Bool} + (hword : word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support) : + ∃ w : List Bool, w.length = L a ∧ word = encPair enc encBits (a, w) := by + rw [heval₁₂ a] at hword + obtain ⟨w, hw, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hword + exact ⟨w, BitString.mem_support_uniformList_iff.mp hw, rfl⟩ + have hsecond₂ (a : α) : ∀ word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (M₃.runClosedConfigFrom (t₃ a) (M₃.initialConfig word))).support, + final.tapes.state = none := by + intro word hw final hfinal + obtain ⟨w, hwlen, rfl⟩ := hword a hw + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₃ a w hwlen).1 + let P := M₃.comp P₁₂ false + let total (a : α) : ℕ := t₁₂ a + (t₁₂ a + 4 + t₃ a) + -- the nondeterministic reading decides the problem + have hdec : P.toNTM.DecidesInTime enc + {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} total := by + intro a + have htime : P.toNTM.RunsInTime (enc a) (total a) := P.runsInTime_toNTM + (MultiTapePTM.comp_halted P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) (hsecond₂ a)) + refine ⟨htime, ?_⟩ + rw [MultiTapeNTM.accepts_iff_exists_time_eq htime, + P.exists_computationPath_toNTM_iff (P := fun cfg => cfg.output = [true])] + have hiff : (∃ final ∈ (ProbComp.eval (P.runClosedConfigFrom (total a) + (P.initialConfig (enc a)))).support, final.tapes.output = [true]) ↔ + [true] ∈ (ProbComp.eval (P.runClosed (total a) (enc a))).support := by + rw [MultiTapePTM.runClosed_eq_map, ProbComp.eval_map, PMF.mem_support_map_iff] + rw [hiff, MultiTapePTM.eval_comp P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) + (hsecond₂ a), Probability.PMF.monad_bind_eq_bind, PMF.mem_support_bind_iff] + constructor + · rintro ⟨w, hw, hV⟩ + refine ⟨encPair enc encBits (a, w), ?_, ?_⟩ + · rw [heval₁₂ a] + exact (PMF.mem_support_map_iff _ _ _).mpr + ⟨w, BitString.mem_support_uniformList_iff.mpr hw, rfl⟩ + · rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hw).2, PMF.mem_support_pure_iff] + simp [hV] + · rintro ⟨word, hw, hacc⟩ + obtain ⟨w, hwlen, rfl⟩ := hword a hw + rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hwlen).2, + PMF.mem_support_pure_iff] at hacc + exact ⟨w, hwlen, by simpa using hacc⟩ + -- the composed clock is within `O(t)` + refine ⟨(6 * c₁ + c₃) * C, (6 * c₁ + c₃) * (C + 1) + 14, _, _, inferInstance, P.toNTM, + hdec.mono fun a => ?_⟩ + set X := C * t (enc a).length + C + 1 + have hX₁ : t₁ a ≤ c₁ * X := Nat.mul_le_mul_left c₁ (by + have := ht a (List.replicate (L a) false) (List.length_replicate ..) + omega) + have htotal : total a ≤ 6 * t₁ a + 14 + t₃ a := by + have := hlen₁ a + simp only [total, t₁₂, t₂] + omega + have hX₃ : t₃ a = c₃ * X := rfl + calc total a ≤ 6 * (c₁ * X) + 14 + c₃ * X := by + have := Nat.mul_le_mul_left 6 hX₁ + rw [hX₃] at htotal + omega + _ = (6 * c₁ + c₃) * C * t (enc a).length + ((6 * c₁ + c₃) * (C + 1) + 14) := by + simp only [X] + ring + +/-- **A linear-time verifier for nondeterministic time.** A problem in `NTIME enc t` has a +verifier computable in linear time on encoded pairs. For a constant `c`, every certificate length +`L ≥ c * t (enc a).length + c` works: `a ∈ A` exactly when some certificate of length `L` is +accepted. The verifier checks that the certificate, read as coins of the choice table, replays an +accepting computation. -/ +theorem exists_verifier_of_mem_NTIME {A : Set α} {t : ℕ → ℕ} (hA : A ∈ NTIME enc t) : + ∃ (V : α × List Bool → Bool) (c : ℕ), + ComputableInO V (encPair enc encBits) encBool (fun p => (encPair enc encBits p).length) + (fun p => (encPair enc encBits p).length) ∧ + ∀ a L, c * t (enc a).length + c ≤ L → + (a ∈ A ↔ ∃ w : List Bool, w.length = L ∧ V (a, w) = true) := by + obtain ⟨c₁, c₂, k, State, hfinite, ntm, hdec⟩ := hA + set M := Nat.card (Turing.Action k Bool State) + refine ⟨ntm.checkChoices enc, M * (c₁ + c₂), ?_, fun a L hL => + hdec.mem_iff_exists_checkChoices ?_⟩ + · -- replay the certificate with the choice table, then compare the output with `[true]` + have hswap : ComputableInO (fun p : α × List Bool => (p.2, enc p.1)) (encPair enc encBits) + (encPair encBits encBits) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) := + (ComputableInO.snd enc encBits).prod + ((ComputableInO.of_eq (f := fun x : α => enc x) (encIn := enc) (encMid := encBits) + fun _ => rfl).comp (ComputableInO.fst enc encBits)) + have hrun := (ComputableInO.of_linear + (MultiTapePTM.computableInLinearTimeAndSpace_runClosedCoins ntm.choiceTable)).comp hswap + obtain ⟨cr, hcr⟩ := hrun.length_le_time + have heq := ComputableInO.eqWords.comp ((ComputableInO.const (encIn := encPair enc encBits) + (encMid := encBits) [true]).prod hrun) + have hfun : ((fun p : List Bool × List Bool => decide (p.1 = p.2)) ∘ + fun p : α × List Bool => ([true], ((fun q : List Bool × List Bool => + ntm.choiceTable.runClosedCoins q.1 q.2) ∘ fun p : α × List Bool => (p.2, enc p.1)) p)) = + ntm.checkChoices enc := by + funext p + simp [MultiTapeNTM.checkChoices, eq_comm] + rw [hfun] at heq + -- every part is linear in the encoded pair, including the replayed output + have hbound (p : α × List Bool) : + (encPair enc encBits p).length + ((encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length) + + (encPair encBits encBits (p.2, enc p.1)).length) + + 2 * ((ntm.choiceTable.runClosedCoins p.2 (enc p.1)).length + 2) ≤ + (9 + 10 * cr) * ((encPair enc encBits p).length + 1) := by + have hc := hcr p + simp only [Function.comp_apply, encBits_apply] at hc + have hle : (enc p.1).length ≤ (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + have hsw : (encPair encBits encBits (p.2, enc p.1)).length ≤ + 2 * (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + generalize (encPair enc encBits p).length = N at * + generalize (ntm.choiceTable.runClosedCoins p.2 (enc p.1)).length = R at * + generalize (encPair encBits encBits (p.2, enc p.1)).length = W at * + have hR : R ≤ cr * (5 * N + 1) := hc.trans (Nat.mul_le_mul_left cr (by omega)) + nlinarith + refine heq.mono (9 + 10 * cr) (fun p => ?_) fun p => ?_ + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + nlinarith + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + omega + · have hmul : M * (c₁ * t (enc a).length + c₂) ≤ + M * (c₁ + c₂) * t (enc a).length + M * (c₁ + c₂) := by + rw [Nat.mul_assoc, ← Nat.mul_add] + exact Nat.mul_le_mul_left M (by nlinarith) + exact hmul.trans hL + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean new file mode 100644 index 0000000000..7b6a8192b7 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean @@ -0,0 +1,268 @@ +/- +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.Machines.Turing.MultiTape.Probabilistic.Sampling +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic + +/-! +# Sampling a certificate beside a framed word + +`Turing.MultiTapePTM.pairSampler` is one fixed fair-coin machine with three control states and no +work tapes. On an input `frame y ++ r` it copies `frame y` to the output, then emits one fresh +fair bit for each symbol of `r`, and halts at the right boundary. So it outputs `frame y ++ w`, +the pair encoding of `(y, w)`, for a uniform word `w` of length `r.length`. It takes exactly +`(frame y ++ r).length + 1` transitions. Each copying transition also draws a coin, and ignores +it. Read nondeterministically, the machine guesses a certificate for the framed instance. + +## Main definitions + +* `Turing.MultiTapePTM.pairSampler`: the framed copier and certificate sampler. + +## Main results + +* `Turing.MultiTapePTM.eval_pairSampler`: the output is a uniform certificate after the framed + word. +* `Turing.MultiTapePTM.pairSampler_halted`: every run has halted at the linear clock. +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib MultiTapeMachine MultiTapeTM + +namespace PairSampler + +/-- The control phases: before a frame tag, before a framed data bit, and in the sampled tail. -/ +inductive Phase + | tag + | data + | tail + deriving DecidableEq + +instance : Fintype Phase := + ⟨{.tag, .data, .tail}, fun q => by cases q <;> simp⟩ + +/-- The control state after reading a symbol. The right boundary halts. -/ +def next : Phase → Option Bool → Option Phase + | _, none => none + | .tag, some true => some .data + | .tag, some false => some .tail + | .data, some _ => some .tag + | .tail, some _ => some .tail + +/-- The emitted symbol. Framed symbols are copied, and tail symbols are replaced by the coin. -/ +def emit : Phase → Option Bool → Bool → Option Bool + | _, none, _ => none + | .tail, some _, bit => some bit + | .tag, some b, _ => some b + | .data, some b, _ => some b + +end PairSampler + +open PairSampler in +/-- Copy a framed word, then emit one fair bit per remaining input symbol, and halt at the right +boundary, without work tapes. -/ +def pairSampler : MultiTapePTM 0 Bool Phase where + initial := .tag + tr q symbol _ _ bit := .step + { inputTape := if symbol.isSome then 1 else 0 + workTapes := Fin.elim0 + output := emit q symbol bit + state := next q symbol } + Empty.elim Empty.elim + +namespace PairSampler + +/-- The sampler at an input position, with the output written so far. -/ +def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) + (h : index ≤ input.length) : Config 0 Bool Phase Empty input where + tapes := + { state := state + inputPos := ⟨index + 1, by lia⟩ + workTapes := Fin.elim0 + workTapePos := Fin.elim0 + output := output } + +/-- Reading a remaining symbol writes the emitted symbol and advances once. -/ +theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) + (q : Phase) (o : Option Bool) (s : Option Phase) : + (config input (some q) index output (by lia)).step + { inputTape := 1, workTapes := Fin.elim0, output := o, state := s } + Empty.elim Empty.elim = + config input s (index + 1) (output ++ o.toList) h := by + refine Config.ext ?_ (funext fun oracle => oracle.elim) + refine Cfg.ext_zero_tapes rfl ?_ rfl + apply Fin.ext + change (moveInputPos _ .pos).val = index + 1 + 1 + rw [moveInputPos_pos_of_ne_right _ (by simp only [config]; lia)] + rfl + +/-- One live transition at a remaining symbol: draw a coin and take the selected step. -/ +theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) + (q : Phase) (fuel : ℕ) : + ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) + (config input (some q) index output (by lia))) = + ProbComp.eval (ProbComp.uniform Bool >>= fun bit => + pairSampler.runClosedConfigFrom fuel + (config input (next q (some input[index])) (index + 1) + (output ++ (emit q (some input[index]) bit).toList) h)) := by + have hsym := inputSymbolInner (cfg := + (config input (some q) index output (by lia)).tapes) index (by simp [config]; lia) h + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp only [show (config input (some q) index output (by lia)).tapes.state = some q from rfl, + hsym, pairSampler, Option.isSome_some, ↓reduceIte, bind_map_left, step h] + rfl + +/-- At the right boundary the sampler halts, drawing and discarding one coin. -/ +theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : + ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) + (config input (some q) input.length output le_rfl)) = + PMF.pure (config input none input.length output le_rfl) := by + have hsym := inputSymbol_eq_none_of_boundary (cfg := + (config input (some q) input.length output le_rfl).tapes) + (Or.inr (by simp [config])) + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp only [show (config input (some q) input.length output le_rfl).tapes.state = some q from rfl, + pairSampler, hsym, Option.isSome_none, Bool.false_eq_true, ↓reduceIte, bind_map_left] + have hcfg : ∀ bit : Bool, (config input (some q) input.length output le_rfl).step + { inputTape := 0, workTapes := Fin.elim0, output := emit q none bit, + state := next q none } Empty.elim Empty.elim = + config input none input.length output le_rfl := by + intro bit + refine Config.ext ?_ (funext fun oracle => oracle.elim) + refine Cfg.ext_zero_tapes ?_ (by simp [Config.step, config, Turing.Action.apply]) ?_ + · cases q <;> rfl + · cases q <;> simp [Config.step, config, Turing.Action.apply, emit] + simp only [hcfg] + rcases fuel with _ | fuel + · simp only [MultiTapeMachine.runConfigFrom, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.bind_const] + · have hhalt : ∀ n, ProbComp.eval (pairSampler.runClosedConfigFrom n + (config input none input.length output le_rfl)) = + PMF.pure (config input none input.length output le_rfl) := by + intro n + cases n with + | zero => simp [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + | succ n => + rw [runClosedConfigFrom, runConfigFrom, MultiTapeMachine.runConfigFrom] + simp [config] + simp only [ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => ProbComp.eval + (pairSampler.runClosedConfigFrom (fuel + 1) + (config input none input.length output le_rfl))) = _ + rw [hhalt, PMF.bind_const] + +/-- The tail phase: one fresh fair bit per remaining symbol, then halting at the boundary. -/ +theorem eval_run_tail (input : List Bool) (remaining : ℕ) : + ∀ (index : ℕ) (output : List Bool) (h : index + remaining = input.length), + ProbComp.eval (pairSampler.runClosedConfigFrom (remaining + 1) + (config input (some .tail) index output (by lia))) = + (BitString.uniformList remaining).map + (fun tail => config input none input.length (output ++ tail) le_rfl) := by + induction remaining with + | zero => + intro index output h + have hi : index = input.length := by lia + subst index + rw [eval_run_boundary] + simp [BitString.uniformList_zero, PMF.pure_map] + | succ remaining ih => + intro index output h + have hi : index < input.length := by lia + rw [eval_run_succ hi] + simp only [next, emit, Option.toList_some] + simp only [ProbComp.eval_bind, ProbComp.eval_uniform, ih (index + 1) _ (by lia), + BitString.uniformList_succ, PMF.map_bind, PMF.map_comp, Function.comp_def, + List.append_assoc, List.singleton_append] + +/-- The copying phase: a framed word is copied verbatim, ignoring the coins drawn meanwhile. -/ +theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : + ∀ (pre output : List Bool) (hin : input = pre ++ frame y ++ rest), + ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y).length + fuel) + (config input (some .tag) pre.length output (by subst hin; simp))) = + ProbComp.eval (pairSampler.runClosedConfigFrom fuel + (config input (some .tail) (pre.length + (frame y).length) (output ++ frame y) + (by subst hin; simp))) := by + induction y with + | nil => + intro pre output hin + have hlt : pre.length < input.length := by subst hin; simp [frame] + have hget : input[pre.length] = false := by subst hin; simp [frame] + rw [show (frame []).length + fuel = fuel + 1 by simp [frame]; lia, eval_run_succ hlt] + simp only [hget, next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const] + rfl + | cons b y ih => + intro pre output hin + have hlt : pre.length < input.length := by subst hin; simp [frame] + have hlt' : pre.length + 1 < input.length := by subst hin; simp [frame] + have hget : input[pre.length] = true := by subst hin; simp [frame] + have hget' : input[pre.length + 1] = b := by + subst hin + simp only [frame, List.flatMap_cons, List.append_assoc] + rw [List.getElem_append_right (by simp)] + simp + have hlen : (frame (b :: y)).length + fuel = ((frame y).length + fuel + 1) + 1 := by + simp [frame]; lia + rw [hlen, eval_run_succ hlt] + simp only [hget, next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const, eval_run_succ hlt'] + simp only [hget', next, emit, Option.toList_some, ProbComp.eval_bind] + change (ProbComp.eval (ProbComp.uniform Bool)).bind (fun _ => _) = _ + rw [PMF.bind_const] + have hpre : input = (pre ++ [true, b]) ++ frame y ++ rest := by + subst hin; simp [frame] + have := ih (pre ++ [true, b]) (output ++ [true] ++ [b]) hpre + simp only [List.length_append, List.length_cons, List.length_nil] at this + convert this using 3 + · congr 1 + · simp [frame]; lia + · simp + +end PairSampler + +open PairSampler + +/-- The final configuration retains the framed word and a uniform certificate, and has halted at +the right boundary. -/ +theorem eval_runClosedConfig_pairSampler (y r : List Bool) : + ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) + (pairSampler.initialConfig (frame y ++ r))) = + (BitString.uniformList r.length).map (fun w => + PairSampler.config (frame y ++ r) none (frame y ++ r).length (frame y ++ w) le_rfl) := by + have hcfg : pairSampler.initialConfig (frame y ++ r) = + PairSampler.config (frame y ++ r) (some .tag) ([] : List Bool).length [] (by simp) := by + refine Config.ext ?_ rfl + exact Cfg.ext_zero_tapes rfl rfl rfl + rw [hcfg, show (frame y ++ r).length + 1 = (frame y).length + (r.length + 1) by simp; lia, + eval_run_frame (frame y ++ r) r (r.length + 1) y [] [] (by simp)] + simpa only [List.length_nil, zero_add, List.nil_append] using + eval_run_tail (frame y ++ r) r.length (frame y).length (frame y) (by simp) + +/-- The sampler outputs a uniform certificate after the framed word, in a linear number of +transitions. -/ +theorem eval_pairSampler (y r : List Bool) : + ProbComp.eval (pairSampler.runClosed ((frame y ++ r).length + 1) (frame y ++ r)) = + (BitString.uniformList r.length).map (frame y ++ ·) := by + rw [runClosed_eq_map, ProbComp.eval_map, eval_runClosedConfig_pairSampler, PMF.map_comp] + rfl + +/-- Every supported configuration has actually halted by the linear clock. -/ +theorem pairSampler_halted (y r : List Bool) : + ∀ final ∈ (ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) + (pairSampler.initialConfig (frame y ++ r)))).support, final.tapes.state = none := by + intro final hfinal + rw [eval_runClosedConfig_pairSampler] at hfinal + obtain ⟨output, _, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hfinal + rfl + +end Turing.MultiTapePTM diff --git a/ComplexityTests/NondeterministicTimeVerifiers.lean b/ComplexityTests/NondeterministicTimeVerifiers.lean new file mode 100644 index 0000000000..995a36357f --- /dev/null +++ b/ComplexityTests/NondeterministicTimeVerifiers.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Complexity.Computability.Complexity.Classes.Time.Verifier +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler + +/-! The explicit-time verifier characterization of `NTIME` on concrete bounds. A deterministic +linear-time decider is a verifier with empty certificates, and a linear-time nondeterministic +problem survives the round trip through its linear-time verifier and guess and verify, at the +same linear bound. The sampler's output distribution is checked on a small input. -/ + +public section + +namespace ComplexityTests.NondeterministicTimeVerifiers + +open Cslib Cslib.Complexity Turing Turing.MultiTapeTM + +/-- `c * n + c` in unary, within linear time and space. -/ +private theorem computableInO_linear_unary (c : ℕ) : + ComputableInO (fun x : List Bool => c * x.length + c) encBits encUnary + (fun x => x.length) (fun x => x.length) := by + induction c with + | zero => + simpa using ComputableInO.const (encIn := encBits) (encMid := encUnary) 0 + | succ c ih => + have hstep := ComputableInO.lengthUnary.append + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 1) + (g := fun x : List Bool => x.length + 1) (encOut := encUnary) + fun x => by simp [encUnary_apply, List.replicate_add] + have h := ih.append hstep (g := fun x : List Bool => (c + 1) * x.length + (c + 1)) + (encOut := encUnary) fun x => by + simp only [encUnary_apply, ← List.replicate_add] + congr 1 + ring + exact h.mono 3 (fun x => by simp only [encBits_apply]; omega) + (fun x => by simp only [encBits_apply]; omega) + +/-- Guess and verify with empty certificates recovers deterministic linear time inside +nondeterministic linear time. -/ +example {A : Set (List Bool)} (hA : A ∈ DTIME encBits fun n => n) : + A ∈ NTIME encBits fun n => n := by + have hV := (computableInO_indicator_of_mem_DTIME hA).comp (ComputableInO.fst encBits encBits) + have h := setOf_exists_mem_NTIME (ℓ := fun _ => 0) (t := fun n => n) (C := 6) + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 0) hV fun x w hw => by + simp only [List.length_eq_zero_iff] at hw + subst hw + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, + List.length_nil] + omega + have hset : {x : List Bool | ∃ w : List Bool, w.length = 0 ∧ + (indicator A ∘ Prod.fst) (x, w) = true} = A := by + ext x + simp [indicator] + rwa [hset] at h + +/-- **Round trip at linear time.** A problem in nondeterministic linear time has a linear-time +verifier, and guessing certificates of length `c * n + c` for it decides the problem in +nondeterministic linear time again. Both explicit-time hypotheses are satisfiable together. -/ +theorem mem_NTIME_linear_of_verifier_roundTrip {A : Set (List Bool)} + (hA : A ∈ NTIME encBits fun n => n) : A ∈ NTIME encBits fun n => n := by + obtain ⟨V, c, hV, hmem⟩ := exists_verifier_of_mem_NTIME hA + have h := setOf_exists_mem_NTIME (ℓ := fun x : List Bool => c * x.length + c) + (t := fun n => n) (C := c + 4) + (computableInO_linear_unary c) hV fun x w hw => by + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, hw] + nlinarith + have hset : {x : List Bool | ∃ w : List Bool, w.length = c * x.length + c ∧ + V (x, w) = true} = A := by + ext x + exact (hmem x _ le_rfl).symm + rwa [hset] at h + +/-- The sampler copies the framed word `[true]` and guesses a two-bit certificate. -/ +example : ProbComp.eval (MultiTapePTM.pairSampler.runClosed 6 (frame [true] ++ [false, false])) = + (BitString.uniformList 2).map (frame [true] ++ ·) := by + simpa using MultiTapePTM.eval_pairSampler [true] [false, false] + +end ComplexityTests.NondeterministicTimeVerifiers From 48a6545c6091b21f6b1d19854e8be746217cbef9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:07:01 -0400 Subject: [PATCH 2/5] refactor(Machines/PTM): make the pair sampler's proof configurations private The induction configurations `PairSampler.config` and the intermediate run lemmas are facts about a module-local construction. Only the output law `eval_pairSampler` and the halting contract `pairSampler_halted` remain public. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../MultiTape/Probabilistic/PairSampler.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean index 7b6a8192b7..bce12d8550 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/PairSampler.lean @@ -81,7 +81,7 @@ def pairSampler : MultiTapePTM 0 Bool Phase where namespace PairSampler /-- The sampler at an input position, with the output written so far. -/ -def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) +private def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : List Bool) (h : index ≤ input.length) : Config 0 Bool Phase Empty input where tapes := { state := state @@ -91,7 +91,7 @@ def config (input : List Bool) (state : Option Phase) (index : ℕ) (output : Li output := output } /-- Reading a remaining symbol writes the emitted symbol and advances once. -/ -theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) +private theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) (q : Phase) (o : Option Bool) (s : Option Phase) : (config input (some q) index output (by lia)).step { inputTape := 1, workTapes := Fin.elim0, output := o, state := s } @@ -105,7 +105,7 @@ theorem step {input output : List Bool} {index : ℕ} (h : index < input.length) rfl /-- One live transition at a remaining symbol: draw a coin and take the selected step. -/ -theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) +private theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < input.length) (q : Phase) (fuel : ℕ) : ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) (config input (some q) index output (by lia))) = @@ -121,7 +121,7 @@ theorem eval_run_succ {input output : List Bool} {index : ℕ} (h : index < inpu rfl /-- At the right boundary the sampler halts, drawing and discarding one coin. -/ -theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : +private theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : ProbComp.eval (pairSampler.runClosedConfigFrom (fuel + 1) (config input (some q) input.length output le_rfl)) = PMF.pure (config input none input.length output le_rfl) := by @@ -160,7 +160,7 @@ theorem eval_run_boundary (input output : List Bool) (q : Phase) (fuel : ℕ) : rw [hhalt, PMF.bind_const] /-- The tail phase: one fresh fair bit per remaining symbol, then halting at the boundary. -/ -theorem eval_run_tail (input : List Bool) (remaining : ℕ) : +private theorem eval_run_tail (input : List Bool) (remaining : ℕ) : ∀ (index : ℕ) (output : List Bool) (h : index + remaining = input.length), ProbComp.eval (pairSampler.runClosedConfigFrom (remaining + 1) (config input (some .tail) index output (by lia))) = @@ -183,7 +183,7 @@ theorem eval_run_tail (input : List Bool) (remaining : ℕ) : List.append_assoc, List.singleton_append] /-- The copying phase: a framed word is copied verbatim, ignoring the coins drawn meanwhile. -/ -theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : +private theorem eval_run_frame (input rest : List Bool) (fuel : ℕ) (y : List Bool) : ∀ (pre output : List Bool) (hin : input = pre ++ frame y ++ rest), ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y).length + fuel) (config input (some .tag) pre.length output (by subst hin; simp))) = @@ -234,7 +234,7 @@ open PairSampler /-- The final configuration retains the framed word and a uniform certificate, and has halted at the right boundary. -/ -theorem eval_runClosedConfig_pairSampler (y r : List Bool) : +private theorem eval_runClosedConfig_pairSampler (y r : List Bool) : ProbComp.eval (pairSampler.runClosedConfigFrom ((frame y ++ r).length + 1) (pairSampler.initialConfig (frame y ++ r))) = (BitString.uniformList r.length).map (fun w => From 3cab153017a4f421363ced3886358d03838daf62 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:45:48 -0400 Subject: [PATCH 3/5] feat(Classes/Promise): PromiseBPTIME with explicit-time sample-and-verify (#2084 M1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define bounded-error probabilistic time for promise problems (Turing.MultiTapePTM.SolvesWithBoundedErrorInTime, Cslib.Complexity.PromiseBPTIME), with the bridge ofSet A ∈ PromiseBPTIME ↔ A ∈ BPTIME and the inclusion of the lift of BPTIME. Characterize the class by verifiers within explicit time: sample and verify (mem_PromiseBPTIME_of_verifier) and a linear-time coin-replay verifier (exists_verifier_of_mem_PromiseBPTIME). The sample-and-verify machine is extracted from the guess-and-verify proof of #2025 into Classes/Time/SampleVerify (exists_machine_sampleVerify), and setOf_exists_mem_NTIME now uses it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Promise/Time.lean | 321 ++++++++++++++++++ .../Complexity/Classes/Time/SampleVerify.lean | 171 ++++++++++ .../Complexity/Classes/Time/Verifier.lean | 148 ++------ ComplexityTests/PromiseBPTIME.lean | 85 +++++ ROADMAP.md | 6 + references.bib | 9 + 7 files changed, 620 insertions(+), 122 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Promise/Time.lean create mode 100644 Complexity/Computability/Complexity/Classes/Time/SampleVerify.lean create mode 100644 ComplexityTests/PromiseBPTIME.lean diff --git a/Complexity.lean b/Complexity.lean index df95bf446e..fbae575e27 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1290,6 +1290,7 @@ public import Complexity.Computability.Complexity.Classes.Promise.Circuit 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 @@ -1348,6 +1349,7 @@ public import Complexity.Computability.Complexity.Classes.Tally public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial +public import Complexity.Computability.Complexity.Classes.Time.SampleVerify public import Complexity.Computability.Complexity.Classes.Time.Verifier public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting diff --git a/Complexity/Computability/Complexity/Classes/Promise/Time.lean b/Complexity/Computability/Complexity/Classes/Promise/Time.lean new file mode 100644 index 0000000000..1e4460fa80 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Promise/Time.lean @@ -0,0 +1,321 @@ +/- +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.AcceptCount +public import Complexity.Computability.Complexity.Classes.Promise.Basic +public import Complexity.Computability.Complexity.Classes.Time +import Complexity.Computability.Complexity.Classes.Time.SampleVerify +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput + +/-! +# Bounded-error probabilistic time for promise problems + +`Cslib.Complexity.PromiseBPTIME enc t` consists of the promise problems solved with bounded error +within time `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, on instances whose +encoding under `enc` has length `n`, by a fair-coin machine with a binary alphabet and finitely +many states (`Turing.MultiTapePTM.SolvesWithBoundedErrorInTime`). As for `BPTIME`, every run of +that many steps halts, on every instance. The output must be `[true]` with probability at least +`2 / 3` on the yes-instances and `[false]` with probability at least `2 / 3` on the no-instances; +nothing is required on instances outside the promise [Goldreich, Definition 1.2][Goldreich2006]. +A decision problem is in the class exactly when it is in `BPTIME` +(`Cslib.Complexity.ofSet_mem_PromiseBPTIME_iff`). + +The class is characterized by deterministic verifiers reading random strings, keeping the time +bound up to constant factors: + +* **Sample and verify** (`Cslib.Complexity.mem_PromiseBPTIME_of_verifier`). If a verifier `V` is + computable within time `T (a, w)` on encoded pairs, the length `ℓ a` of the random string is + computable in unary within `Tℓ a`, and `(enc a).length + Tℓ a + T (a, w)` is within + `O(t (enc a).length)`, then a promise problem is in `PromiseBPTIME enc t` when at least two + thirds of the strings of length `ℓ a` are accepted on its yes-instances and rejected on its + no-instances. The machine is `Cslib.Complexity.exists_machine_sampleVerify`. +* **Coin replay** (`Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME`). A promise problem in + `PromiseBPTIME enc t` has a verifier computable in linear time on encoded pairs: replay the + coins on the machine and test whether the output is `[true]`. Every random-string length of at + least `c * t (enc a).length + c` works, since a halted run ignores further coins. + +The polynomial characterization of `PromiseBPP` +(`Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn`) loses the polynomial degree; these +explicit-time forms are what a time hierarchy for promise problems needs. Such a hierarchy is +known without advice, by delayed diagonalization [He][He2025], while the hierarchy for `BPTIME` +itself is open. + +## Main definitions + +* `Turing.MultiTapePTM.SolvesWithBoundedErrorInTime`: bounded error on a promise problem within a + clock. +* `Cslib.Complexity.PromiseBPTIME`: bounded-error probabilistic time for promise problems. + +## Main results + +* `Turing.MultiTapePTM.solvesWithBoundedErrorInTime_ofSet_iff`, + `Cslib.Complexity.ofSet_mem_PromiseBPTIME_iff`: on decision problems, the notions are + `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime` and `Cslib.Complexity.BPTIME`. +* `Cslib.Complexity.promiseClass_BPTIME_subset_PromiseBPTIME`: the lift of `BPTIME` is contained. +* `Cslib.Complexity.PromiseBPTIME_mono`, `Cslib.Complexity.mem_PromiseBPTIME_of_subset`: + monotonicity in the time bound and in the promise. +* `Cslib.Complexity.mem_PromiseBPTIME_of_verifier`: sample and verify within explicit time. +* `Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME`: a linear-time coin-replay verifier. + +## References + +* [O. Goldreich, *On promise problems: a survey*][Goldreich2006] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +* [S. He, *A note on a hierarchy theorem for promise-BPTIME*][He2025] +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib Cslib.Complexity + +variable {k : ℕ} {State : Type} {α : Type*} + +/-- `machine` solves the promise problem `Q` with bounded error within `t`, relative to the +encoding `enc`: on every encoded instance `enc a`, every run of `t a` steps with fair coins has +halted; on a yes-instance the run outputs `[true]`, and on a no-instance `[false]`, with +probability at least `2 / 3`. -/ +@[expose] def SolvesWithBoundedErrorInTime (machine : MultiTapePTM k Bool State) + (enc : α ↪ List Bool) (Q : PromiseProblem α) (t : α → ℕ) : Prop := + ∀ a, (∀ final ∈ (ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ Q.yes → 2 / 3 ≤ ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) ∧ + (a ∈ Q.no → 2 / 3 ≤ ProbComp.eval (machine.runClosed (t a) (enc a)) [false]) + +variable {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q : PromiseProblem α} + +/-- Time bounds can be increased: a halted run ignores further coins. -/ +theorem SolvesWithBoundedErrorInTime.mono {t t' : α → ℕ} + (h : machine.SolvesWithBoundedErrorInTime enc Q t) (ht : ∀ a, t a ≤ t' a) : + machine.SolvesWithBoundedErrorInTime enc Q t' := fun a => by + obtain ⟨hhalt, hyes, hno⟩ := h a + refine ⟨?_, ?_, ?_⟩ + · rw [machine.eval_runClosedConfigFrom_eq_of_halted _ (ht a) hhalt] + exact hhalt + · rwa [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] + · rwa [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] + +/-- A machine solving a promise problem solves every promise problem with fewer yes-instances and +fewer no-instances. -/ +theorem SolvesWithBoundedErrorInTime.of_subset {Q' : PromiseProblem α} {t : α → ℕ} + (h : machine.SolvesWithBoundedErrorInTime enc Q t) (hyes : Q'.yes ⊆ Q.yes) + (hno : Q'.no ⊆ Q.no) : machine.SolvesWithBoundedErrorInTime enc Q' t := fun a => + ⟨(h a).1, fun ha => (h a).2.1 (hyes ha), fun ha => (h a).2.2 (hno ha)⟩ + +/-- On a decision problem, solving with bounded error is deciding with bounded error. -/ +theorem solvesWithBoundedErrorInTime_ofSet_iff {A : Set α} {t : α → ℕ} : + machine.SolvesWithBoundedErrorInTime enc (PromiseProblem.ofSet A) t ↔ + machine.DecidesWithBoundedErrorInTime enc A t := by + refine forall_congr' fun a => and_congr_right fun _ => ?_ + by_cases ha : a ∈ A + · have hno : a ∉ (PromiseProblem.ofSet A).no := fun h => h ha + simp only [MultiTapeTM.indicator, ha, ite_true] + exact ⟨fun h => h.1 ha, fun h => ⟨fun _ => h, fun h' => absurd h' hno⟩⟩ + · simp only [MultiTapeTM.indicator, ha, ite_false] + exact ⟨fun h => h.2 ha, fun h => ⟨fun h' => absurd h' ha, fun _ => h⟩⟩ + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM +open scoped ENNReal + +section Definition + +variable {α : Type*} + +/-- The promise problems solved with bounded error within time `O(t n)`, that is `c₁ * t n + c₂` +for constants `c₁` and `c₂`, on instances whose encoding under `enc` has length `n`, by a fair-coin +machine with a binary alphabet and finitely many states: every run of that many steps has halted, +on every instance, and the output is `[true]` on the yes-instances and `[false]` on the +no-instances with probability at least `2 / 3` [Goldreich, Definition 1.2][Goldreich2006]. -/ +@[expose] def PromiseBPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (PromiseProblem α) := + {Q | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) + (machine : MultiTapePTM k Bool State), + machine.SolvesWithBoundedErrorInTime enc Q fun a => c₁ * t (enc a).length + c₂} + +variable {enc : α ↪ List Bool} {Q : PromiseProblem α} + +/-- `PromiseBPTIME` is monotone in the 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 promise problem with fewer yes-instances and fewer no-instances than one in `PromiseBPTIME` +is in `PromiseBPTIME`. -/ +theorem mem_PromiseBPTIME_of_subset {t : ℕ → ℕ} {Q' : PromiseProblem α} + (hQ : Q ∈ PromiseBPTIME enc t) (hyes : Q'.yes ⊆ Q.yes) (hno : Q'.no ⊆ Q.no) : + Q' ∈ PromiseBPTIME enc t := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩ := hQ + exact ⟨c₁, c₂, k, State, hfinite, machine, hQ.of_subset hyes hno⟩ + +/-- **`PromiseBPTIME` agrees with `BPTIME` on decision problems.** -/ +theorem ofSet_mem_PromiseBPTIME_iff {t : ℕ → ℕ} {A : Set α} : + PromiseProblem.ofSet A ∈ PromiseBPTIME enc t ↔ A ∈ BPTIME enc t := by + simp only [PromiseBPTIME, BPTIME, Set.mem_ofPred_eq, + MultiTapePTM.solvesWithBoundedErrorInTime_ofSet_iff] + +/-- **The lift of `BPTIME` is in `PromiseBPTIME`.** A bounded-error decider of a problem separating +the yes-instances from the no-instances solves the promise problem. -/ +theorem promiseClass_BPTIME_subset_PromiseBPTIME {t : ℕ → ℕ} : + promiseClass (BPTIME enc t) ⊆ PromiseBPTIME enc t := by + rintro Q ⟨A, hA, hyes, hno⟩ + exact mem_PromiseBPTIME_of_subset (ofSet_mem_PromiseBPTIME_iff.mpr hA) hyes + fun a ha haA => hno.notMem_of_mem_left haA ha + +end Definition + +/-! ### Sample and verify -/ + +section Verifier + +variable {α : Type} {enc : α ↪ List Bool} + +/-- A probability of at least `2 / 3` is a fraction of at least two thirds. -/ +private theorem two_thirds_le_div_iff {c n : ℕ} : + (2 / 3 : ℝ≥0∞) ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c := by + rw [ENNReal.le_div_iff_mul_le (Or.inl (pow_ne_zero _ two_ne_zero)) + (Or.inl (ENNReal.pow_ne_top ENNReal.ofNat_ne_top)), div_eq_mul_inv, mul_right_comm, + ← div_eq_mul_inv, ENNReal.div_le_iff (by norm_num) (by norm_num)] + constructor + · intro h + have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by + push_cast + rw [mul_comm (3 : ℝ≥0∞)] + exact h + exact_mod_cast this + · intro h + have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by exact_mod_cast h + push_cast at this + rw [mul_comm (c : ℝ≥0∞)] + exact this + +/-- The probability that the verdict on a uniformly random string of length `n` is `b` is the +fraction of the strings with that verdict. -/ +private theorem uniformList_map_verdict_apply (V : α × List Bool → Bool) (a : α) (n : ℕ) + (b : Bool) : ((BitString.uniformList n).map fun w => [V (a, w)]) [b] = + (acceptCount (fun p => V p == b) a n : ℝ≥0∞) / 2 ^ n := by + rw [BitString.uniformList_map_apply] + simp only [acceptCount, List.cons.injEq, and_true, beq_iff_eq] + +/-- **Sample and verify, within explicit time.** If a verifier `V` is computable within time +`T (a, w)` on encoded pairs, and the length `ℓ a` of the random string is computable in unary +within time `Tℓ a`, with `(enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C` for every +string `w` of length `ℓ a`, then a promise problem is in `PromiseBPTIME enc t` when `V` accepts at +least two thirds of the strings of length `ℓ a` together with each yes-instance `a`, and rejects at +least two thirds of them together with each no-instance. -/ +theorem mem_PromiseBPTIME_of_verifier {Q : PromiseProblem α} {V : α × List Bool → Bool} + {ℓ : α → ℕ} {t : ℕ → ℕ} {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} + (hℓ : ComputableInO ℓ enc encUnary Tℓ Sℓ) + (hV : ComputableInO V (encPair enc encBits) encBool T S) + (ht : ∀ a w, w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) + (hyes : ∀ a ∈ Q.yes, 2 * 2 ^ ℓ a ≤ 3 * acceptCount V a (ℓ a)) + (hno : ∀ a ∈ Q.no, 2 * 2 ^ ℓ a ≤ 3 * acceptCount (fun p => !V p) a (ℓ a)) : + Q ∈ PromiseBPTIME enc t := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := exists_machine_sampleVerify hℓ hV ht + refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hmachine a).1, fun ha => ?_, fun ha => ?_⟩⟩ + · rw [(hmachine a).2, uniformList_map_verdict_apply, two_thirds_le_div_iff] + simpa only [beq_true] using hyes a ha + · rw [(hmachine a).2, uniformList_map_verdict_apply, two_thirds_le_div_iff] + simpa only [beq_false] using hno a ha + +/-- **A linear-time verifier for promise-problem probabilistic time.** A promise problem in +`PromiseBPTIME enc t` has a verifier computable in linear time on encoded pairs. For a constant +`c`, every random-string length `L ≥ c * t (enc a).length + c` works: the verifier accepts at least +two thirds of the strings of length `L` together with each yes-instance, and rejects at least two +thirds of them together with each no-instance. The verifier replays the coins on the machine and +tests whether the output is `[true]`. -/ +theorem exists_verifier_of_mem_PromiseBPTIME {Q : PromiseProblem α} {t : ℕ → ℕ} + (hQ : Q ∈ PromiseBPTIME enc t) : + ∃ (V : α × List Bool → Bool) (c : ℕ), + ComputableInO V (encPair enc encBits) encBool (fun p => (encPair enc encBits p).length) + (fun p => (encPair enc encBits p).length) ∧ + ∀ a L, c * t (enc a).length + c ≤ L → + (a ∈ Q.yes → 2 * 2 ^ L ≤ 3 * acceptCount V a L) ∧ + (a ∈ Q.no → 2 * 2 ^ L ≤ 3 * acceptCount (fun p => !V p) a L) := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩ := hQ + let V : α × List Bool → Bool := fun p => decide (machine.runClosedCoins p.2 (enc p.1) = [true]) + refine ⟨V, c₁ + c₂, ?_, fun a L hL => ?_⟩ + · -- replay the coins, then compare the output with `[true]` + have hswap : ComputableInO (fun p : α × List Bool => (p.2, enc p.1)) (encPair enc encBits) + (encPair encBits encBits) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) + (fun p => (encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length)) := + (ComputableInO.snd enc encBits).prod + ((ComputableInO.of_eq (f := fun x : α => enc x) (encIn := enc) (encMid := encBits) + fun _ => rfl).comp (ComputableInO.fst enc encBits)) + have hrun := (ComputableInO.of_linear + (MultiTapePTM.computableInLinearTimeAndSpace_runClosedCoins machine)).comp hswap + obtain ⟨cr, hcr⟩ := hrun.length_le_time + have heq := ComputableInO.eqWords.comp ((ComputableInO.const (encIn := encPair enc encBits) + (encMid := encBits) [true]).prod hrun) + have hfun : ((fun p : List Bool × List Bool => decide (p.1 = p.2)) ∘ + fun p : α × List Bool => ([true], ((fun q : List Bool × List Bool => + machine.runClosedCoins q.1 q.2) ∘ fun p : α × List Bool => (p.2, enc p.1)) p)) = V := by + funext p + simp [V, eq_comm] + rw [hfun] at heq + -- every part is linear in the encoded pair, including the replayed output + have hbound (p : α × List Bool) : + (encPair enc encBits p).length + ((encPair enc encBits p).length + + ((encPair enc encBits p).length + (enc p.1).length) + + (encPair encBits encBits (p.2, enc p.1)).length) + + 2 * ((machine.runClosedCoins p.2 (enc p.1)).length + 2) ≤ + (9 + 10 * cr) * ((encPair enc encBits p).length + 1) := by + have hc := hcr p + simp only [Function.comp_apply, encBits_apply] at hc + have hle : (enc p.1).length ≤ (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + have hsw : (encPair encBits encBits (p.2, enc p.1)).length ≤ + 2 * (encPair enc encBits p).length := by + simp only [encPair_apply, List.length_append, length_frame, encBits_apply] + omega + generalize (encPair enc encBits p).length = N at * + generalize (machine.runClosedCoins p.2 (enc p.1)).length = R at * + generalize (encPair encBits encBits (p.2, enc p.1)).length = W at * + have hR : R ≤ cr * (5 * N + 1) := hc.trans (Nat.mul_le_mul_left cr (by omega)) + nlinarith + refine heq.mono (9 + 10 * cr) (fun p => ?_) fun p => ?_ + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + nlinarith + · have := hbound p + simp only [Function.comp_apply, List.length_singleton] at this ⊢ + omega + · -- at `L` coins, the halted run is distributed as the replays + obtain ⟨hhalt, hyes, hno⟩ := hQ a + have hT : c₁ * t (enc a).length + c₂ ≤ L := + le_trans (by nlinarith) hL + have heval : ProbComp.eval (machine.runClosed L (enc a)) = + (BitString.uniformList L).map fun w => machine.runClosedCoins w (enc a) := by + rw [MultiTapePTM.eval_runClosed_eq_map_coins] + rw [← machine.eval_runClosed_eq_of_halted _ hT hhalt, heval, + BitString.uniformList_map_apply, two_thirds_le_div_iff] at hyes hno + refine ⟨fun ha => ?_, fun ha => ?_⟩ + · simpa only [acceptCount, V, decide_eq_true_eq] using hyes ha + · refine (hno ha).trans (Nat.mul_le_mul_left 3 (Finset.card_le_card fun w hw => ?_)) + simp only [Finset.mem_filter, Finset.mem_univ, true_and, V, Bool.not_eq_true', + decide_eq_false_iff_not] at hw ⊢ + rw [hw] + simp + +end Verifier + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time/SampleVerify.lean b/Complexity/Computability/Complexity/Classes/Time/SampleVerify.lean new file mode 100644 index 0000000000..f21a52592d --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/SampleVerify.lean @@ -0,0 +1,171 @@ +/- +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.Machines.Turing.MultiTape.Complexity.BigO +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed +public import Complexity.Probability.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler +import Complexity.Computability.Machines.Turing.MultiTape.Run +import Complexity.Probability.PMF.Bind + +/-! +# Sampling a random string and running a verifier, within explicit time + +A fair-coin machine can draw a uniformly random string `w` of length `ℓ a` and output the verdict +`V (a, w)` of a deterministic verifier on the pair `(a, w)`, within the time it takes to write +`ℓ a` in unary and to run the verifier, up to constant factors +(`Cslib.Complexity.exists_machine_sampleVerify`). The machine is a closed fair-coin composition: + +* a deterministic machine writes `frame (enc a)` followed by `ℓ a` ones; +* the fixed sampler `Turing.MultiTapePTM.pairSampler` copies the framed instance and replaces the + ones by fair coins; +* a deterministic machine runs the verifier. + +Every run halts within the clock, and the output is distributed as `[V (a, w)]` for `w` uniform of +length `ℓ a`. Read nondeterministically, the machine guesses and verifies a certificate +(`Cslib.Complexity.setOf_exists_mem_NTIME`); read probabilistically, it samples and verifies +(`Cslib.Complexity.mem_PromiseBPTIME_of_verifier`). Unlike the polynomial compiler of PPT +programs (`Cslib.Probability.IsPPTOn.exists_halting_machine`), the clock keeps the time bound up to +constant factors. + +## Main results + +* `Cslib.Complexity.exists_machine_sampleVerify`: the sample-and-verify machine within explicit + time, with its output distribution. +-/ + +public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +variable {α : Type} {enc : α ↪ List Bool} + +/-- **Sample and verify, within explicit time.** If a verifier `V` is computable within time +`T (a, w)` on encoded pairs, and the length `ℓ a` of the random string is computable in unary +within time `Tℓ a`, and `(enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C` for every +string `w` of length `ℓ a`, then a fair-coin machine with a binary alphabet and finitely many +states halts on every run within time `c₁ * t (enc a).length + c₂` and outputs `[V (a, w)]` for a +uniformly random `w` of length `ℓ a`. -/ +theorem exists_machine_sampleVerify {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} + {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} + (hℓ : ComputableInO ℓ enc encUnary Tℓ Sℓ) + (hV : ComputableInO V (encPair enc encBits) encBool T S) + (ht : ∀ a w, w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : + ∃ (c₁ c₂ k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State), + ∀ a, (∀ final ∈ (ProbComp.eval (machine.runClosedConfigFrom (c₁ * t (enc a).length + c₂) + (machine.initialConfig (enc a)))).support, final.tapes.state = none) ∧ + ProbComp.eval (machine.runClosed (c₁ * t (enc a).length + c₂) (enc a)) = + (BitString.uniformList (ℓ a)).map fun w => [V (a, w)] := by + -- the deterministic preparation and the verifier, as machines + obtain ⟨c₁, ⟨k₁, Q₁, _, tm₁, h₁⟩, -⟩ := + (ComputableInO.of_eq (f := fun a : α => a) (encIn := enc) (encMid := enc) fun _ => rfl).prod hℓ + obtain ⟨c₃, ⟨k₃, Q₃, _, tm₃, h₃⟩, -⟩ := hV + let L (a : α) : ℕ := ℓ a + let u (a : α) : List Bool := frame (enc a) ++ List.replicate (L a) true + let t₁ (a : α) : ℕ := c₁ * ((enc a).length + Tℓ a + 1) + let t₂ (a : α) : ℕ := (u a).length + 1 + let t₃ (a : α) : ℕ := c₃ * (C * t (enc a).length + C + 1) + have hrun₁ (a : α) := (h₁ a).runFrom_of_le (le_refl (t₁ a)) + have hlen₁ (a : α) : (u a).length ≤ t₁ a := (h₁ a).length_output_le + -- the first phase writes the framed instance and the unary length of the random string + let M₁ : MultiTapePTM k₁ Bool Q₁ := MultiTapePTM.ofDeterministic tm₁ + have hfirst₁ (a : α) : ∀ final ∈ (ProbComp.eval + (M₁.runClosedConfigFrom (t₁ a) (M₁.initialConfig (enc a)))).support, + final.tapes.state = none := by + intro final hfinal + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₁ a).1 + have hout₁ (a : α) : ProbComp.eval (M₁.runClosed (t₁ a) (enc a)) = PMF.pure (u a) := by + rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₁ a).2] + rfl + -- the sampler copies the framed instance and draws the random string + have hsecond₁ (a : α) : ∀ word ∈ (ProbComp.eval (M₁.runClosed (t₁ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (MultiTapePTM.pairSampler.runClosedConfigFrom (t₂ a) + (MultiTapePTM.pairSampler.initialConfig word))).support, final.tapes.state = none := by + intro word hword + rw [hout₁ a, PMF.mem_support_pure_iff] at hword + subst hword + exact MultiTapePTM.pairSampler_halted (enc a) (List.replicate (L a) true) + let P₁₂ := MultiTapePTM.pairSampler.comp M₁ false + let t₁₂ (a : α) : ℕ := t₁ a + (t₁ a + 4 + t₂ a) + have heval₁₂ (a : α) : ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a)) = + (BitString.uniformList (L a)).map (frame (enc a) ++ ·) := by + rw [MultiTapePTM.eval_comp M₁ MultiTapePTM.pairSampler false (enc a) (t₁ a) (t₂ a) + (hfirst₁ a) (hsecond₁ a), hout₁ a, Probability.PMF.monad_bind_eq_bind, PMF.pure_bind] + simpa only [List.length_replicate, u] using + MultiTapePTM.eval_pairSampler (enc a) (List.replicate (L a) true) + have hhalt₁₂ (a : α) := MultiTapePTM.comp_halted M₁ MultiTapePTM.pairSampler false (enc a) + (t₁ a) (t₂ a) (hfirst₁ a) (hsecond₁ a) + -- the verifier runs on every sampled pair within the uniform clock `t₃` + let M₃ : MultiTapePTM k₃ Bool Q₃ := MultiTapePTM.ofDeterministic tm₃ + have hrun₃ (a : α) (w : List Bool) (hw : w.length = L a) := + (h₃ (a, w)).runFrom_of_le (J := t₃ a) (Nat.mul_le_mul_left c₃ (by + have := ht a w hw + omega)) + have hword (a : α) {word : List Bool} + (hword : word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support) : + ∃ w : List Bool, w.length = L a ∧ word = encPair enc encBits (a, w) := by + rw [heval₁₂ a] at hword + obtain ⟨w, hw, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hword + exact ⟨w, BitString.mem_support_uniformList_iff.mp hw, rfl⟩ + have hsecond₂ (a : α) : ∀ word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support, + ∀ final ∈ (ProbComp.eval (M₃.runClosedConfigFrom (t₃ a) (M₃.initialConfig word))).support, + final.tapes.state = none := by + intro word hw final hfinal + obtain ⟨w, hwlen, rfl⟩ := hword a hw + rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal + subst hfinal + exact (hrun₃ a w hwlen).1 + let P := M₃.comp P₁₂ false + let total (a : α) : ℕ := t₁₂ a + (t₁₂ a + 4 + t₃ a) + have hhalt (a : α) := MultiTapePTM.comp_halted P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) + (hsecond₂ a) + -- the output is the verdict on a uniformly random string + have heval (a : α) : ProbComp.eval (P.runClosed (total a) (enc a)) = + (BitString.uniformList (ℓ a)).map fun w => [V (a, w)] := by + rw [MultiTapePTM.eval_comp P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) (hsecond₂ a), + Probability.PMF.monad_bind_eq_bind, heval₁₂ a, PMF.bind_map, ← PMF.bind_pure_comp] + refine Probability.PMF.bind_congr_on_support _ _ _ fun w hw => ?_ + have hwlen : w.length = L a := BitString.mem_support_uniformList_iff.mp hw + simp only [Function.comp_apply] + rw [MultiTapePTM.eval_runClosed_ofDeterministic] + exact congrArg PMF.pure (hrun₃ a w hwlen).2 + -- the composed clock is within `O(t)` + have hle (a : α) : total a ≤ (6 * c₁ + c₃) * C * t (enc a).length + + ((6 * c₁ + c₃) * (C + 1) + 14) := by + set X := C * t (enc a).length + C + 1 + have hX₁ : t₁ a ≤ c₁ * X := Nat.mul_le_mul_left c₁ (by + have := ht a (List.replicate (L a) false) (List.length_replicate ..) + omega) + have htotal : total a ≤ 6 * t₁ a + 14 + t₃ a := by + have := hlen₁ a + simp only [total, t₁₂, t₂] + omega + have hX₃ : t₃ a = c₃ * X := rfl + calc total a ≤ 6 * (c₁ * X) + 14 + c₃ * X := by + have := Nat.mul_le_mul_left 6 hX₁ + rw [hX₃] at htotal + omega + _ = (6 * c₁ + c₃) * C * t (enc a).length + ((6 * c₁ + c₃) * (C + 1) + 14) := by + simp only [X] + ring + refine ⟨(6 * c₁ + c₃) * C, (6 * c₁ + c₃) * (C + 1) + 14, _, _, inferInstance, P, fun a => ?_⟩ + refine ⟨?_, ?_⟩ + · rw [P.eval_runClosedConfigFrom_eq_of_halted _ (hle a) (hhalt a)] + exact hhalt a + · rw [P.eval_runClosed_eq_of_halted _ (hle a) (hhalt a)] + exact heval a + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time/Verifier.lean b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean index 89b4f594ab..d8bf71efd4 100644 --- a/Complexity/Computability/Complexity/Classes/Time/Verifier.lean +++ b/Complexity/Computability/Complexity/Classes/Time/Verifier.lean @@ -9,15 +9,12 @@ module public import Complexity.Computability.Complexity.Classes.Time import Complexity.Computability.Complexity.Classes.NP.Nondeterministic +import Complexity.Computability.Complexity.Classes.Time.SampleVerify import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts -import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Composition -import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PairSampler import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput -import Complexity.Computability.Machines.Turing.MultiTape.Run import Complexity.Probability.BitString -import Complexity.Probability.PMF.Bind /-! # Nondeterministic time through verifiers, with explicit bounds @@ -33,14 +30,12 @@ two directions here keep it. `{a | ∃ w, w.length = ℓ a ∧ V (a, w) = true}` lies in `NTIME enc t` whenever `(enc a).length + Tℓ a + T (a, w)` is within `O(t (enc a).length)` on certificates of that length. The certificate length may depend on the instance, not only on its encoded length. - The machine is the nondeterministic reading of a closed fair-coin composition: - - a deterministic machine writes `frame (enc a)` followed by `ℓ` ones; - - the fixed sampler `Turing.MultiTapePTM.pairSampler` copies the framed instance and replaces - the ones by fair coins; - - a deterministic machine runs the verifier. - - Its computation paths are exactly the coin replays, so it accepts exactly when some - certificate is accepted, and every branch halts within the composed clock. + The machine is the nondeterministic reading of the sample-and-verify machine + (`Cslib.Complexity.exists_machine_sampleVerify`), a closed fair-coin composition that writes + `frame (enc a)` followed by `ℓ` ones, replaces the ones by fair coins with the fixed sampler + `Turing.MultiTapePTM.pairSampler`, and runs the verifier. Its computation paths are exactly the + coin replays, so it accepts exactly when some certificate is accepted, and every branch halts + within the clock. * **Verifiers from nondeterministic time** (`Cslib.Complexity.exists_verifier_of_mem_NTIME`). A problem in `NTIME enc t` has a verifier that is computable in linear time on encoded pairs: check that the certificate, read as coins of the choice table @@ -81,116 +76,25 @@ theorem setOf_exists_mem_NTIME {V : α × List Bool → Bool} {ℓ : α → ℕ} (hV : ComputableInO V (encPair enc encBits) encBool T S) (ht : ∀ a w, w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} ∈ NTIME enc t := by - -- the deterministic preparation and the verifier, as machines - obtain ⟨c₁, ⟨k₁, Q₁, _, tm₁, h₁⟩, -⟩ := - (ComputableInO.of_eq (f := fun a : α => a) (encIn := enc) (encMid := enc) fun _ => rfl).prod hℓ - obtain ⟨c₃, ⟨k₃, Q₃, _, tm₃, h₃⟩, -⟩ := hV - let L (a : α) : ℕ := ℓ a - let u (a : α) : List Bool := frame (enc a) ++ List.replicate (L a) true - let t₁ (a : α) : ℕ := c₁ * ((enc a).length + Tℓ a + 1) - let t₂ (a : α) : ℕ := (u a).length + 1 - let t₃ (a : α) : ℕ := c₃ * (C * t (enc a).length + C + 1) - have hrun₁ (a : α) := (h₁ a).runFrom_of_le (le_refl (t₁ a)) - have hlen₁ (a : α) : (u a).length ≤ t₁ a := (h₁ a).length_output_le - -- the first phase writes the framed instance and the unary certificate length - let M₁ : MultiTapePTM k₁ Bool Q₁ := MultiTapePTM.ofDeterministic tm₁ - have hfirst₁ (a : α) : ∀ final ∈ (ProbComp.eval - (M₁.runClosedConfigFrom (t₁ a) (M₁.initialConfig (enc a)))).support, - final.tapes.state = none := by - intro final hfinal - rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal - subst hfinal - exact (hrun₁ a).1 - have hout₁ (a : α) : ProbComp.eval (M₁.runClosed (t₁ a) (enc a)) = PMF.pure (u a) := by - rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₁ a).2] - rfl - -- the sampler copies the framed instance and guesses the certificate - have hsecond₁ (a : α) : ∀ word ∈ (ProbComp.eval (M₁.runClosed (t₁ a) (enc a))).support, - ∀ final ∈ (ProbComp.eval (MultiTapePTM.pairSampler.runClosedConfigFrom (t₂ a) - (MultiTapePTM.pairSampler.initialConfig word))).support, final.tapes.state = none := by - intro word hword - rw [hout₁ a, PMF.mem_support_pure_iff] at hword - subst hword - exact MultiTapePTM.pairSampler_halted (enc a) (List.replicate (L a) true) - let P₁₂ := MultiTapePTM.pairSampler.comp M₁ false - let t₁₂ (a : α) : ℕ := t₁ a + (t₁ a + 4 + t₂ a) - have heval₁₂ (a : α) : ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a)) = - (BitString.uniformList (L a)).map (frame (enc a) ++ ·) := by - rw [MultiTapePTM.eval_comp M₁ MultiTapePTM.pairSampler false (enc a) (t₁ a) (t₂ a) - (hfirst₁ a) (hsecond₁ a), hout₁ a, Probability.PMF.monad_bind_eq_bind, PMF.pure_bind] - simpa only [List.length_replicate, u] using - MultiTapePTM.eval_pairSampler (enc a) (List.replicate (L a) true) - have hhalt₁₂ (a : α) := MultiTapePTM.comp_halted M₁ MultiTapePTM.pairSampler false (enc a) - (t₁ a) (t₂ a) (hfirst₁ a) (hsecond₁ a) - -- the verifier runs on every guessed pair within the uniform clock `t₃` - let M₃ : MultiTapePTM k₃ Bool Q₃ := MultiTapePTM.ofDeterministic tm₃ - have hrun₃ (a : α) (w : List Bool) (hw : w.length = L a) := - (h₃ (a, w)).runFrom_of_le (J := t₃ a) (Nat.mul_le_mul_left c₃ (by - have := ht a w hw - omega)) - have hword (a : α) {word : List Bool} - (hword : word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support) : - ∃ w : List Bool, w.length = L a ∧ word = encPair enc encBits (a, w) := by - rw [heval₁₂ a] at hword - obtain ⟨w, hw, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hword - exact ⟨w, BitString.mem_support_uniformList_iff.mp hw, rfl⟩ - have hsecond₂ (a : α) : ∀ word ∈ (ProbComp.eval (P₁₂.runClosed (t₁₂ a) (enc a))).support, - ∀ final ∈ (ProbComp.eval (M₃.runClosedConfigFrom (t₃ a) (M₃.initialConfig word))).support, - final.tapes.state = none := by - intro word hw final hfinal - obtain ⟨w, hwlen, rfl⟩ := hword a hw - rw [MultiTapePTM.eval_runClosedConfigFrom_ofDeterministic, PMF.mem_support_pure_iff] at hfinal - subst hfinal - exact (hrun₃ a w hwlen).1 - let P := M₃.comp P₁₂ false - let total (a : α) : ℕ := t₁₂ a + (t₁₂ a + 4 + t₃ a) - -- the nondeterministic reading decides the problem - have hdec : P.toNTM.DecidesInTime enc - {a | ∃ w : List Bool, w.length = ℓ a ∧ V (a, w) = true} total := by - intro a - have htime : P.toNTM.RunsInTime (enc a) (total a) := P.runsInTime_toNTM - (MultiTapePTM.comp_halted P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) (hsecond₂ a)) - refine ⟨htime, ?_⟩ - rw [MultiTapeNTM.accepts_iff_exists_time_eq htime, - P.exists_computationPath_toNTM_iff (P := fun cfg => cfg.output = [true])] - have hiff : (∃ final ∈ (ProbComp.eval (P.runClosedConfigFrom (total a) - (P.initialConfig (enc a)))).support, final.tapes.output = [true]) ↔ - [true] ∈ (ProbComp.eval (P.runClosed (total a) (enc a))).support := by - rw [MultiTapePTM.runClosed_eq_map, ProbComp.eval_map, PMF.mem_support_map_iff] - rw [hiff, MultiTapePTM.eval_comp P₁₂ M₃ false (enc a) (t₁₂ a) (t₃ a) (hhalt₁₂ a) - (hsecond₂ a), Probability.PMF.monad_bind_eq_bind, PMF.mem_support_bind_iff] - constructor - · rintro ⟨w, hw, hV⟩ - refine ⟨encPair enc encBits (a, w), ?_, ?_⟩ - · rw [heval₁₂ a] - exact (PMF.mem_support_map_iff _ _ _).mpr - ⟨w, BitString.mem_support_uniformList_iff.mpr hw, rfl⟩ - · rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hw).2, PMF.mem_support_pure_iff] - simp [hV] - · rintro ⟨word, hw, hacc⟩ - obtain ⟨w, hwlen, rfl⟩ := hword a hw - rw [MultiTapePTM.eval_runClosed_ofDeterministic, (hrun₃ a w hwlen).2, - PMF.mem_support_pure_iff] at hacc - exact ⟨w, hwlen, by simpa using hacc⟩ - -- the composed clock is within `O(t)` - refine ⟨(6 * c₁ + c₃) * C, (6 * c₁ + c₃) * (C + 1) + 14, _, _, inferInstance, P.toNTM, - hdec.mono fun a => ?_⟩ - set X := C * t (enc a).length + C + 1 - have hX₁ : t₁ a ≤ c₁ * X := Nat.mul_le_mul_left c₁ (by - have := ht a (List.replicate (L a) false) (List.length_replicate ..) - omega) - have htotal : total a ≤ 6 * t₁ a + 14 + t₃ a := by - have := hlen₁ a - simp only [total, t₁₂, t₂] - omega - have hX₃ : t₃ a = c₃ * X := rfl - calc total a ≤ 6 * (c₁ * X) + 14 + c₃ * X := by - have := Nat.mul_le_mul_left 6 hX₁ - rw [hX₃] at htotal - omega - _ = (6 * c₁ + c₃) * C * t (enc a).length + ((6 * c₁ + c₃) * (C + 1) + 14) := by - simp only [X] - ring + obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := exists_machine_sampleVerify hℓ hV ht + refine ⟨c₁, c₂, k, State, hfinite, machine.toNTM, fun a => ?_⟩ + -- the nondeterministic reading accepts exactly when some sampled string is accepted + have htime : machine.toNTM.RunsInTime (enc a) (c₁ * t (enc a).length + c₂) := + machine.runsInTime_toNTM (hmachine a).1 + refine ⟨htime, ?_⟩ + rw [MultiTapeNTM.accepts_iff_exists_time_eq htime, + machine.exists_computationPath_toNTM_iff (P := fun cfg => cfg.output = [true])] + set T := c₁ * t (enc a).length + c₂ + have hiff : (∃ final ∈ (ProbComp.eval (machine.runClosedConfigFrom T + (machine.initialConfig (enc a)))).support, final.tapes.output = [true]) ↔ + [true] ∈ (ProbComp.eval (machine.runClosed T (enc a))).support := by + rw [MultiTapePTM.runClosed_eq_map, ProbComp.eval_map, PMF.mem_support_map_iff] + rw [hiff, (hmachine a).2, PMF.mem_support_map_iff] + constructor + · rintro ⟨w, hw, hVw⟩ + exact ⟨w, BitString.mem_support_uniformList_iff.mpr hw, by rw [hVw]⟩ + · rintro ⟨w, hw, hVw⟩ + exact ⟨w, BitString.mem_support_uniformList_iff.mp hw, by simpa using hVw⟩ /-- **A linear-time verifier for nondeterministic time.** A problem in `NTIME enc t` has a verifier computable in linear time on encoded pairs. For a constant `c`, every certificate length diff --git a/ComplexityTests/PromiseBPTIME.lean b/ComplexityTests/PromiseBPTIME.lean new file mode 100644 index 0000000000..5927431e6d --- /dev/null +++ b/ComplexityTests/PromiseBPTIME.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Complexity.Computability.Complexity.Classes.Promise.Time +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators + +/-! The explicit-time verifier characterization of `PromiseBPTIME` on concrete bounds. A +deterministic linear-time decider is a sample-and-verify machine with no coins, so it solves every +promise problem it separates, and its problem is in `BPTIME`. A promise problem in linear time +survives the round trip through its linear-time coin-replay verifier and sample and verify, at the +same linear bound, so both explicit-time hypotheses are satisfiable together. -/ + +public section + +namespace ComplexityTests.PromiseBPTIME + +open Cslib Cslib.Complexity Turing Turing.MultiTapeTM + +/-- `c * n + c` in unary, within linear time and space. -/ +private theorem computableInO_linear_unary (c : ℕ) : + ComputableInO (fun x : List Bool => c * x.length + c) encBits encUnary + (fun x => x.length) (fun x => x.length) := by + induction c with + | zero => + simpa using ComputableInO.const (encIn := encBits) (encMid := encUnary) 0 + | succ c ih => + have hstep := ComputableInO.lengthUnary.append + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 1) + (g := fun x : List Bool => x.length + 1) (encOut := encUnary) + fun x => by simp [encUnary_apply, List.replicate_add] + have h := ih.append hstep (g := fun x : List Bool => (c + 1) * x.length + (c + 1)) + (encOut := encUnary) fun x => by + simp only [encUnary_apply, ← List.replicate_add] + congr 1 + ring + exact h.mono 3 (fun x => by simp only [encBits_apply]; omega) + (fun x => by simp only [encBits_apply]; omega) + +/-- **A deterministic linear-time decider, with no coins.** Every promise problem separated by a +problem in `DTIME n` is in `PromiseBPTIME n`. -/ +theorem mem_PromiseBPTIME_of_mem_DTIME {A : Set (List Bool)} {Q : PromiseProblem (List Bool)} + (hA : A ∈ DTIME encBits fun n => n) (hyes : Q.yes ⊆ A) (hno : Q.no ⊆ Aᶜ) : + Q ∈ PromiseBPTIME encBits fun n => n := by + have hV := (computableInO_indicator_of_mem_DTIME hA).comp (ComputableInO.fst encBits encBits) + refine mem_PromiseBPTIME_of_verifier (ℓ := fun _ => 0) (t := fun n => n) (C := 6) + (ComputableInO.const (encIn := encBits) (encMid := encUnary) 0) hV (fun x w hw => ?_) + (fun x hx => ?_) fun x hx => ?_ + · simp only [List.length_eq_zero_iff] at hw + subst hw + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, List.length_nil] + omega + · simp [acceptCount_zero, indicator, hyes hx] + · simp [acceptCount_zero, indicator, show x ∉ A from hno hx] + +/-- Through the bridge with `BPTIME`, a problem in `DTIME n` is in `BPTIME n`. -/ +example {A : Set (List Bool)} (hA : A ∈ DTIME encBits fun n => n) : + A ∈ BPTIME encBits fun n => n := + ofSet_mem_PromiseBPTIME_iff.mp + (mem_PromiseBPTIME_of_mem_DTIME hA le_rfl fun _ h => h) + +/-- **Round trip at linear time.** A promise problem in linear time has a linear-time coin-replay +verifier, and sampling strings of length `c * n + c` for it solves the problem in linear time +again. Both explicit-time hypotheses are satisfiable together. -/ +theorem mem_PromiseBPTIME_linear_of_verifier_roundTrip {Q : PromiseProblem (List Bool)} + (hQ : Q ∈ PromiseBPTIME encBits fun n => n) : Q ∈ PromiseBPTIME encBits fun n => n := by + obtain ⟨V, c, hV, hbound⟩ := exists_verifier_of_mem_PromiseBPTIME hQ + exact mem_PromiseBPTIME_of_verifier (ℓ := fun x : List Bool => c * x.length + c) + (t := fun n => n) (C := c + 4) (computableInO_linear_unary c) hV + (fun x w hw => by + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, hw] + nlinarith) + (fun x hx => (hbound x _ (by simp [encBits_apply])).1 hx) + fun x hx => (hbound x _ (by simp [encBits_apply])).2 hx + +/-- The lift of `BPTIME` is contained in `PromiseBPTIME`, at a concrete bound. -/ +example : promiseClass (BPTIME encBits fun n => n) ⊆ PromiseBPTIME encBits fun n => n := + promiseClass_BPTIME_subset_PromiseBPTIME + +end ComplexityTests.PromiseBPTIME diff --git a/ROADMAP.md b/ROADMAP.md index 966929f763..45ef667742 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -184,6 +184,11 @@ index links to canonical definitions rather than keeping a second set. `f log f = o(g)` hierarchy, which needs the diagonal to clock the universal machine's own steps, noninteger polynomial degrees, and sharp nondeterministic and alternating time hierarchies with certified simulators. +- **Probabilistic time hierarchies** ([#2084]): the hierarchy for promise problems + (`PromiseBPTIME`), by delayed diagonalization following He (ECCC TR25-004), and the + one-bit-advice hierarchy for languages of van Melkebeek and Pervyshev. `PromiseBPTIME` and its + explicit-time sample-and-verify characterization are in place (`Classes/Promise/Time`). The + advice-free hierarchy for `BPTIME` itself is open and is not a target. - The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold its input. - **Space:** Savitch bounds for general space-constructible functions. @@ -736,3 +741,4 @@ not planned, not as proved. [#1817]: https://github.com/cslib-community/complexitylib/issues/1817 [#1885]: https://github.com/cslib-community/complexitylib/pull/1885 [#2019]: https://github.com/cslib-community/complexitylib/issues/2019 +[#2084]: https://github.com/cslib-community/complexitylib/issues/2084 diff --git a/references.bib b/references.bib index 36330860a1..9e22afc1a5 100644 --- a/references.bib +++ b/references.bib @@ -2335,6 +2335,15 @@ @article{Haussler1992 doi = {10.1016/0890-5401(92)90010-D} } +@techreport{He2025, + author = {He, Songhua}, + title = {A note on a hierarchy theorem for promise-{BPTIME}}, + institution = {Electronic Colloquium on Computational Complexity}, + number = {TR25-004}, + year = {2025}, + url = {https://eccc.weizmann.ac.il/report/2025/004/} +} + @inproceedings{HemaspaandraEtAl2018, author = {Hemaspaandra, Edith and Hemaspaandra, Lane A. and Spakowski, Holger and Watanabe, Osamu}, From ff253f6f61ce71aabb0022d416667920b9d41dc7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:49:30 -0400 Subject: [PATCH 4/5] doc(Classes/Promise): cite Goldreich's survey without an unverified locator; test a concrete member Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/Promise/Time.lean | 4 ++-- ComplexityTests/PromiseBPTIME.lean | 13 +++++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Promise/Time.lean b/Complexity/Computability/Complexity/Classes/Promise/Time.lean index 1e4460fa80..6bf6a9f3d4 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Time.lean @@ -25,7 +25,7 @@ encoding under `enc` has length `n`, by a fair-coin machine with a binary alphab many states (`Turing.MultiTapePTM.SolvesWithBoundedErrorInTime`). As for `BPTIME`, every run of that many steps halts, on every instance. The output must be `[true]` with probability at least `2 / 3` on the yes-instances and `[false]` with probability at least `2 / 3` on the no-instances; -nothing is required on instances outside the promise [Goldreich, Definition 1.2][Goldreich2006]. +nothing is required on instances outside the promise [Goldreich][Goldreich2006]. A decision problem is in the class exactly when it is in `BPTIME` (`Cslib.Complexity.ofSet_mem_PromiseBPTIME_iff`). @@ -140,7 +140,7 @@ variable {α : Type*} for constants `c₁` and `c₂`, on instances whose encoding under `enc` has length `n`, by a fair-coin machine with a binary alphabet and finitely many states: every run of that many steps has halted, on every instance, and the output is `[true]` on the yes-instances and `[false]` on the -no-instances with probability at least `2 / 3` [Goldreich, Definition 1.2][Goldreich2006]. -/ +no-instances with probability at least `2 / 3` [Goldreich][Goldreich2006]. -/ @[expose] def PromiseBPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (PromiseProblem α) := {Q | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State), diff --git a/ComplexityTests/PromiseBPTIME.lean b/ComplexityTests/PromiseBPTIME.lean index 5927431e6d..3f6676ad84 100644 --- a/ComplexityTests/PromiseBPTIME.lean +++ b/ComplexityTests/PromiseBPTIME.lean @@ -64,6 +64,19 @@ example {A : Set (List Bool)} (hA : A ∈ DTIME encBits fun n => n) : ofSet_mem_PromiseBPTIME_iff.mp (mem_PromiseBPTIME_of_mem_DTIME hA le_rfl fun _ h => h) +/-- The promise problem with every word a yes-instance, solved by sampling no coins and +accepting: a concrete member of `PromiseBPTIME n`. -/ +example : (⟨Set.univ, ∅, Set.disjoint_empty _⟩ : PromiseProblem (List Bool)) ∈ + PromiseBPTIME encBits fun n => n := by + refine mem_PromiseBPTIME_of_verifier (V := fun _ => true) (ℓ := fun _ => 0) (t := fun n => n) + (C := 4) (ComputableInO.const (encIn := encBits) (encMid := encUnary) 0) + (ComputableInO.const (encIn := encPair encBits encBits) (encMid := encBool) true) + (fun x w hw => ?_) (fun x _ => by simp) fun x hx => absurd hx (Set.notMem_empty x) + simp only [List.length_eq_zero_iff] at hw + subst hw + simp only [encBits_apply, encPair_apply, List.length_append, length_frame, List.length_nil] + omega + /-- **Round trip at linear time.** A promise problem in linear time has a linear-time coin-replay verifier, and sampling strings of length `c * n + c` for it solves the problem in linear time again. Both explicit-time hypotheses are satisfiable together. -/ From 101286199f671df61a4fb07b05bd5308e84600cc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 14:16:13 -0500 Subject: [PATCH 5/5] refactor(Foundations): share the two-thirds dyadic fraction lemma `Classes/Time` and `Classes/Promise/Time` each proved the same private `two_thirds_le_div_iff`. Keep one public copy, `ENNReal.two_div_three_le_natCast_div_two_pow_iff`, in a small Foundations companion and use it from both modules. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Complexity/Classes/Promise/Time.lean | 28 +++-------- .../Complexity/Classes/Time.lean | 24 ++------- .../Foundations/Analysis/ENNRealFraction.lean | 50 +++++++++++++++++++ 4 files changed, 60 insertions(+), 43 deletions(-) create mode 100644 Complexity/Foundations/Analysis/ENNRealFraction.lean diff --git a/Complexity.lean b/Complexity.lean index 985e0ccb9d..a1fc8f0208 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2840,6 +2840,7 @@ public import Complexity.Foundations.Algebra.GeometricTail public import Complexity.Foundations.Algebra.Shear public import Complexity.Foundations.Analysis.Asymptotics.Exponential public import Complexity.Foundations.Analysis.BernoulliInequality +public import Complexity.Foundations.Analysis.ENNRealFraction public import Complexity.Foundations.Analysis.ENNRealTsum public import Complexity.Foundations.Analysis.Fourier.ZModProd public import Complexity.Foundations.Analysis.HarmonicMean diff --git a/Complexity/Computability/Complexity/Classes/Promise/Time.lean b/Complexity/Computability/Complexity/Classes/Promise/Time.lean index 6bf6a9f3d4..3e032f1243 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Time.lean @@ -15,6 +15,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimi import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput +import Complexity.Foundations.Analysis.ENNRealFraction /-! # Bounded-error probabilistic time for promise problems @@ -185,25 +186,6 @@ section Verifier variable {α : Type} {enc : α ↪ List Bool} -/-- A probability of at least `2 / 3` is a fraction of at least two thirds. -/ -private theorem two_thirds_le_div_iff {c n : ℕ} : - (2 / 3 : ℝ≥0∞) ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c := by - rw [ENNReal.le_div_iff_mul_le (Or.inl (pow_ne_zero _ two_ne_zero)) - (Or.inl (ENNReal.pow_ne_top ENNReal.ofNat_ne_top)), div_eq_mul_inv, mul_right_comm, - ← div_eq_mul_inv, ENNReal.div_le_iff (by norm_num) (by norm_num)] - constructor - · intro h - have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by - push_cast - rw [mul_comm (3 : ℝ≥0∞)] - exact h - exact_mod_cast this - · intro h - have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by exact_mod_cast h - push_cast at this - rw [mul_comm (c : ℝ≥0∞)] - exact this - /-- The probability that the verdict on a uniformly random string of length `n` is `b` is the fraction of the strings with that verdict. -/ private theorem uniformList_map_verdict_apply (V : α × List Bool → Bool) (a : α) (n : ℕ) @@ -228,9 +210,11 @@ theorem mem_PromiseBPTIME_of_verifier {Q : PromiseProblem α} {V : α × List Bo Q ∈ PromiseBPTIME enc t := by obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := exists_machine_sampleVerify hℓ hV ht refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hmachine a).1, fun ha => ?_, fun ha => ?_⟩⟩ - · rw [(hmachine a).2, uniformList_map_verdict_apply, two_thirds_le_div_iff] + · rw [(hmachine a).2, uniformList_map_verdict_apply, + ENNReal.two_div_three_le_natCast_div_two_pow_iff] simpa only [beq_true] using hyes a ha - · rw [(hmachine a).2, uniformList_map_verdict_apply, two_thirds_le_div_iff] + · rw [(hmachine a).2, uniformList_map_verdict_apply, + ENNReal.two_div_three_le_natCast_div_two_pow_iff] simpa only [beq_false] using hno a ha /-- **A linear-time verifier for promise-problem probabilistic time.** A promise problem in @@ -307,7 +291,7 @@ theorem exists_verifier_of_mem_PromiseBPTIME {Q : PromiseProblem α} {t : ℕ (BitString.uniformList L).map fun w => machine.runClosedCoins w (enc a) := by rw [MultiTapePTM.eval_runClosed_eq_map_coins] rw [← machine.eval_runClosed_eq_of_halted _ hT hhalt, heval, - BitString.uniformList_map_apply, two_thirds_le_div_iff] at hyes hno + BitString.uniformList_map_apply, ENNReal.two_div_three_le_natCast_div_two_pow_iff] at hyes hno refine ⟨fun ha => ?_, fun ha => ?_⟩ · simpa only [acceptCount, V, decide_eq_true_eq] using hyes ha · refine (hno ha).trans (Nat.mul_le_mul_left 3 (Finset.card_le_card fun w hw => ?_)) diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean index 57c0226098..73831d7901 100644 --- a/Complexity/Computability/Complexity/Classes/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Time.lean @@ -20,6 +20,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayIn import Complexity.Computability.Probabilistic.PPT.Capture import Complexity.Computability.Probabilistic.PPT.Clock import Complexity.Computability.Probabilistic.Sampling +import Complexity.Foundations.Analysis.ENNRealFraction import Complexity.Probability.PMF.Map import Mathlib.Data.Set.Finite.List @@ -370,25 +371,6 @@ theorem mem_NP_iff_exists_mem_NTIME {α : Type} {enc : α ↪ List Bool} {A : Se open Cslib.Probability open scoped ENNReal -/-- A probability of at least `2 / 3` is a fraction of at least two thirds. -/ -private theorem two_thirds_le_div_iff {c n : ℕ} : - (2 / 3 : ℝ≥0∞) ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c := by - rw [ENNReal.le_div_iff_mul_le (Or.inl (pow_ne_zero _ two_ne_zero)) - (Or.inl (ENNReal.pow_ne_top ENNReal.ofNat_ne_top)), div_eq_mul_inv, mul_right_comm, - ← div_eq_mul_inv, ENNReal.div_le_iff (by norm_num) (by norm_num)] - constructor - · intro h - have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by - push_cast - rw [mul_comm (3 : ℝ≥0∞)] - exact h - exact_mod_cast this - · intro h - have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by exact_mod_cast h - push_cast at this - rw [mul_comm (c : ℝ≥0∞)] - exact this - /-- An injective map keeps the probability of the image of a value. -/ private theorem map_apply_of_injective {β γ : Type} {p : PMF β} {f : β → γ} (hf : Function.Injective f) (b : β) : p.map f (f b) = p b := by @@ -428,7 +410,7 @@ theorem mem_BPP_iff_exists_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A : map_apply_of_injective encBool.injective] simp only [program, ProbComp.eval_map, BitString.eval_sampleList] rw [BitString.uniformList_map_apply] - exact two_thirds_le_div_iff.mpr (hA.two_mul_le a) + exact ENNReal.two_div_three_le_natCast_div_two_pow_iff.mpr (hA.two_mul_le a) · rintro ⟨d, c₁, c₂, k, State, hfinite, machine, hA⟩ -- replay the coins refine ⟨Polynomial.C c₁ * Polynomial.X ^ d + Polynomial.C c₂, @@ -444,7 +426,7 @@ theorem mem_BPP_iff_exists_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A : simp have hprob := (hA a).2 rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, - two_thirds_le_div_iff] at hprob + ENNReal.two_div_three_le_natCast_div_two_pow_iff] at hprob dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt] rw [heval] constructor diff --git a/Complexity/Foundations/Analysis/ENNRealFraction.lean b/Complexity/Foundations/Analysis/ENNRealFraction.lean new file mode 100644 index 0000000000..2bbc1e3cc7 --- /dev/null +++ b/Complexity/Foundations/Analysis/ENNRealFraction.lean @@ -0,0 +1,50 @@ +/- +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.Init +public import Mathlib.Basic.ENNReal.Inv + +/-! +# Dyadic fractions in `ℝ≥0∞` + +A count `c` out of `2 ^ n` equally likely strings is a probability `c / 2 ^ n`. Bounded-error +acceptance thresholds compare it with `2 / 3`; this file turns that comparison into one between +natural numbers. + +## Main results + +* `ENNReal.two_div_three_le_natCast_div_two_pow_iff`: `2 / 3 ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c`. +-/ + +@[expose] public section + +open scoped ENNReal + +namespace ENNReal + +/-- A dyadic fraction `c / 2 ^ n` is at least two thirds exactly when `2 * 2 ^ n ≤ 3 * c`. -/ +theorem two_div_three_le_natCast_div_two_pow_iff {c n : ℕ} : + (2 / 3 : ℝ≥0∞) ≤ c / 2 ^ n ↔ 2 * 2 ^ n ≤ 3 * c := by + rw [ENNReal.le_div_iff_mul_le (Or.inl (pow_ne_zero _ two_ne_zero)) + (Or.inl (ENNReal.pow_ne_top ENNReal.ofNat_ne_top)), div_eq_mul_inv, mul_right_comm, + ← div_eq_mul_inv, ENNReal.div_le_iff (by norm_num) (by norm_num)] + constructor + · intro h + have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by + push_cast + rw [mul_comm (3 : ℝ≥0∞)] + exact h + exact_mod_cast this + · intro h + have : ((2 * 2 ^ n : ℕ) : ℝ≥0∞) ≤ ((3 * c : ℕ) : ℝ≥0∞) := by exact_mod_cast h + push_cast at this + rw [mul_comm (c : ℝ≥0∞)] + exact this + +end ENNReal