diff --git a/Complexity.lean b/Complexity.lean index b9691b2bbf..7e687ef29e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1397,6 +1397,7 @@ 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.Promise.Time.Verifier public import Complexity.Computability.Complexity.Classes.RP public import Complexity.Computability.Complexity.Classes.RP.Closure public import Complexity.Computability.Complexity.Classes.RepeatedTrials @@ -1459,6 +1460,7 @@ public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.BoundedExists 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.Time.WordRAM public import Complexity.Computability.Complexity.Classes.TimeSpace.Williams @@ -2932,6 +2934,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 c3bfe88d4f..fa2cc61177 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Time.lean @@ -19,9 +19,13 @@ the output is `[true]` with probability at least `2/3`, and on no-instances it i probability at least `2/3`. No probability gap or answer is required outside the promise. This is the library's time-indexed native-machine convention, extending `BPTIME` to partial -promises. It does not define the class through bounded-error total completions. A strict-majority -completion belongs to `PPTIME` at the same caller-supplied clock, with ties rejecting; this is not -a bounded-error completion in `BPTIME`. +promises: a decision problem is in `PromiseBPTIME` exactly when it is in `BPTIME`. It does not +define the class through bounded-error total completions. A strict-majority completion belongs to +`PPTIME` at the same caller-supplied clock, with ties rejecting; this is not a bounded-error +completion in `BPTIME`. + +The characterization by sample-and-verify and coin replay at the same clock, up to constant +factors, is in `Complexity.Computability.Complexity.Classes.Promise.Time.Verifier`. ## Main definitions @@ -30,7 +34,11 @@ a bounded-error completion in `BPTIME`. ## Main results +* `Turing.MultiTapePTM.solvesPromiseWithBoundedErrorInTime_ofSet_iff`, + `ofSet_mem_PromiseBPTIME`: on decision problems, the notions are + `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime` and `BPTIME`. * `PromiseBPTIME_mono`: increasing the time bound preserves membership. +* `mem_PromiseBPTIME_of_subset`: shrinking either side of the promise preserves membership. * `promiseClass_BPTIME_subset_PromiseBPTIME`: total bounded-error completions give witnesses. * `PromiseBPTIME_subset_promiseClass_PPTIME`: a strict-majority completion at the same time scale. -/ @@ -65,6 +73,29 @@ theorem SolvesPromiseWithBoundedErrorInTime.mono · rw [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] exact ⟨hyes, hno⟩ +/-- A machine solving a promise problem solves every promise problem with fewer yes-instances and +fewer no-instances. -/ +theorem SolvesPromiseWithBoundedErrorInTime.of_subset + {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q Q' : PromiseProblem α} + {t : α → ℕ} (h : machine.SolvesPromiseWithBoundedErrorInTime enc Q t) + (hyes : Q'.yes ⊆ Q.yes) (hno : Q'.no ⊆ Q.no) : + machine.SolvesPromiseWithBoundedErrorInTime enc Q' t := fun a => + let ⟨hhalt, hQyes, hQno⟩ := h a + ⟨hhalt, fun ha => hQyes (hyes ha), fun ha => hQno (hno ha)⟩ + +/-- On a decision problem, solving with bounded error is deciding with bounded error. -/ +theorem solvesPromiseWithBoundedErrorInTime_ofSet_iff {machine : MultiTapePTM k Bool State} + {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} : + machine.SolvesPromiseWithBoundedErrorInTime 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 @@ -88,6 +119,21 @@ theorem PromiseBPTIME_mono {T₁ T₂ : ℕ → ℕ} (h : ∀ n, T₁ n ≤ T₂ 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 {Q Q' : PromiseProblem α} (hQ : Q ∈ PromiseBPTIME enc T) + (hyes : Q'.yes ⊆ Q.yes) (hno : Q'.no ⊆ Q.no) : Q' ∈ PromiseBPTIME enc T := + let ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩ := hQ + ⟨c₁, c₂, k, State, hfinite, machine, hQ.of_subset hyes hno⟩ + +/-- A decision problem, as a promise problem, is in `PromiseBPTIME` exactly when it is in +`BPTIME`. -/ +@[simp] +theorem ofSet_mem_PromiseBPTIME {A : Set α} : + PromiseProblem.ofSet A ∈ PromiseBPTIME enc T ↔ A ∈ BPTIME enc T := by + simp only [PromiseBPTIME, BPTIME, Set.mem_ofPred_eq, + MultiTapePTM.solvesPromiseWithBoundedErrorInTime_ofSet_iff] + /-- A bounded-error total completion supplies a native bounded-error promise solver. -/ theorem promiseClass_BPTIME_subset_PromiseBPTIME : promiseClass (BPTIME enc T) ⊆ PromiseBPTIME enc T := by diff --git a/Complexity/Computability/Complexity/Classes/Promise/Time/Verifier.lean b/Complexity/Computability/Complexity/Classes/Promise/Time/Verifier.lean new file mode 100644 index 0000000000..f614c5edd1 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Promise/Time/Verifier.lean @@ -0,0 +1,177 @@ +/- +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.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 +import Complexity.Foundations.Analysis.ENNRealFraction + +/-! +# Verifier characterization of `PromiseBPTIME` within explicit time + +Promise problems [Goldreich][Goldreich2006] in `Cslib.Complexity.PromiseBPTIME enc t` are +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 results + +* `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. He, *A note on a hierarchy theorem for promise-BPTIME*][He2025] +-/ + +public section + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM +open scoped ENNReal + +variable {α : Type} {enc : α ↪ List Bool} + +/-- 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, + 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, + 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 +`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, 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 => ?_)) + 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 Cslib.Complexity 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/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/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 diff --git a/ComplexityTests/PromiseBPTIME.lean b/ComplexityTests/PromiseBPTIME.lean new file mode 100644 index 0000000000..533d6fc758 --- /dev/null +++ b/ComplexityTests/PromiseBPTIME.lean @@ -0,0 +1,98 @@ +/- +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.Verifier +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.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. -/ +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 3e83d52cb5..281213b435 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -186,6 +186,12 @@ index links to canonical definitions rather than keeping a second set. machine's own steps, noninteger polynomial degrees, a word-RAM hierarchy by direct diagonalization with a smaller gap, 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` and + `Classes/Promise/Time/Verifier`). 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. @@ -769,3 +775,4 @@ not planned, not as proved. [#2019]: https://github.com/cslib-community/complexitylib/issues/2019 [#2062]: https://github.com/cslib-community/complexitylib/issues/2062 [#2063]: https://github.com/cslib-community/complexitylib/issues/2063 +[#2084]: https://github.com/cslib-community/complexitylib/issues/2084 diff --git a/references.bib b/references.bib index 8f93baa3e3..240f66ccc5 100644 --- a/references.bib +++ b/references.bib @@ -2389,6 +2389,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},