From cdd8f312bcddc149c6cf2a500aac843be1ad2f69 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:39:53 -0400 Subject: [PATCH 1/3] feat(Classes/PP): unbounded-error probabilistic time PPTIME Define Turing.MultiTapePTM.DecidesByMajorityInTime and Cslib.Complexity.PPTIME, the strict-majority counterpart of BPTIME on the same fair-coin machines, and prove PPTIME_mono, BPTIME_subset_PPTIME, the count form decidesByMajorityInTime_iff, and mem_PP_iff_exists_mem_PPTIME, the machine characterisation of the verifier-based PP. Statement groundwork for #1833. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Computability/Complexity/Classes/PP.lean | 4 +- .../Complexity/Classes/PP/Time.lean | 221 ++++++++++++++++++ .../Complexity/Classes/Time.lean | 3 + ComplexityTests/PPTime.lean | 72 ++++++ 5 files changed, 300 insertions(+), 1 deletion(-) create mode 100644 Complexity/Computability/Complexity/Classes/PP/Time.lean create mode 100644 ComplexityTests/PPTime.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28..0ef68184e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1121,6 +1121,7 @@ public import Complexity.Computability.Complexity.Classes.PP.Bit public import Complexity.Computability.Complexity.Classes.PP.Characterization public import Complexity.Computability.Complexity.Classes.PP.Closure public import Complexity.Computability.Complexity.Classes.PP.Oracle +public import Complexity.Computability.Complexity.Classes.PP.Time public import Complexity.Computability.Complexity.Classes.PP.TruthTable public import Complexity.Computability.Complexity.Classes.Padding public import Complexity.Computability.Complexity.Classes.Padding.Polynomial diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean index 37f7c119a..adc5b38ba 100644 --- a/Complexity/Computability/Complexity/Classes/PP.lean +++ b/Complexity/Computability/Complexity/Classes/PP.lean @@ -27,7 +27,9 @@ verifier (`BPP_subset_PP`). Gill requires a strict majority on members, as here; the variant with a non-strict majority defines the same class (`Cslib.Complexity.mem_PP_iff_decidesByNonstrictMajority`). The -characterisation by probabilistic machines is not proved here. +characterisation by fair-coin machines deciding by strict majority within polynomial time is +`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`, in +`Complexity.Computability.Complexity.Classes.PP.Time`. ## Main definitions diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean new file mode 100644 index 000000000..5775864e3 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -0,0 +1,221 @@ +/- +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.PP +public import Complexity.Computability.Complexity.Classes.Time +import Complexity.Computability.Complexity.Classes.SharpP.Probability +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput +import Complexity.Computability.Probabilistic.PPT.Capture +import Complexity.Computability.Probabilistic.PPT.Clock +import Complexity.Computability.Probabilistic.Sampling + +/-! +# Unbounded-error probabilistic time + +`Cslib.Complexity.PPTIME enc t` consists of the problems decided by strict majority within time +`O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, by a fair-coin machine with a +binary alphabet and finitely many states (`Turing.MultiTapePTM.DecidesByMajorityInTime`): every +run on that many coins has halted, and `a ∈ A` exactly when the run outputs `[true]` with +probability more than `1 / 2` [Gill][Gill1977]. It is the unbounded-error counterpart of +`Cslib.Complexity.BPTIME`, with the same machines and clocks. + +A fair-coin machine draws one coin per live step, so its acceptance probability within the clock +`t` is the number of accepting coin strings of length `t` divided by `2 ^ t`. Deciding by majority +is therefore the comparison `2 ^ t < 2 * count` of that count, an `Cslib.Complexity.acceptCount` +of the coin replay `Turing.MultiTapePTM.runClosedCoins` +(`Turing.MultiTapePTM.decidesByMajorityInTime_iff`). + +`PP` (`Cslib.Complexity.PP`) is defined through polynomial-time verifiers reading random strings. +It is the union of the classes `PPTIME (n ^ k)` (`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`), +by the argument for `BPP` and `BPTIME` (`Cslib.Complexity.mem_BPP_iff_exists_mem_BPTIME`): a +verifier run on sampled coins is a fair-coin machine with a halting polynomial clock, and a +fair-coin machine halting within `T` steps is a verifier replaying `T` coins. A bounded-error +decider decides by majority (`Cslib.Complexity.BPTIME_subset_PPTIME`). + +## Main definitions + +* `Turing.MultiTapePTM.DecidesByMajorityInTime`: strict majority within a clock. +* `Cslib.Complexity.PPTIME`: unbounded-error probabilistic time. + +## Main results + +* `Turing.MultiTapePTM.decidesByMajorityInTime_iff`: the majority condition as a count of + accepting coin strings. +* `Cslib.Complexity.PPTIME_mono`: `PPTIME` is monotone in the time bound. +* `Cslib.Complexity.BPTIME_subset_PPTIME`: bounded error is a strict majority. +* `Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`: `PP` is the union of the classes + `PPTIME (n ^ k)`. + +## References + +* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib +open scoped ENNReal + +variable {k : ℕ} {State : Type} {α : Type*} + +/-- `machine` decides `A` by strict majority within `t`, relative to the encoding `enc`: on every +encoded instance `enc a`, every run of `t a` steps with fair coins has halted, and `a ∈ A` exactly +when the run outputs `[true]` with probability more than `1 / 2` [Gill][Gill1977]. -/ +def DecidesByMajorityInTime (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) + (A : Set α) (t : α → ℕ) : Prop := + ∀ a, (∀ final ∈ (ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ A ↔ 1 / 2 < ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) + +/-- Time bounds can be increased: a halted run ignores further coins. -/ +theorem DecidesByMajorityInTime.mono {machine : MultiTapePTM k Bool State} + {enc : α ↪ List Bool} {A : Set α} {t t' : α → ℕ} + (h : machine.DecidesByMajorityInTime enc A t) (ht : ∀ a, t a ≤ t' a) : + machine.DecidesByMajorityInTime enc A t' := fun a => by + obtain ⟨hhalt, hmem⟩ := 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] + +/-- A probability `c / 2 ^ n` exceeds one half exactly when `2 ^ n < 2 * c`. -/ +private theorem half_lt_div_iff {c n : ℕ} : + (1 / 2 : ℝ≥0∞) < c / 2 ^ n ↔ 2 ^ n < 2 * c := by + have h2n : (2 : ℝ≥0∞) ^ n ≠ 0 := pow_ne_zero _ two_ne_zero + have h2n' : (2 : ℝ≥0∞) ^ n ≠ ⊤ := ENNReal.pow_ne_top ENNReal.ofNat_ne_top + rw [ENNReal.lt_div_iff_mul_lt (Or.inl h2n) (Or.inl h2n'), one_div, mul_comm, + ← div_eq_mul_inv, ENNReal.div_lt_iff (Or.inl two_ne_zero) (Or.inl ENNReal.ofNat_ne_top), + show ((c : ℝ≥0∞) * 2) = ((2 * c : ℕ) : ℝ≥0∞) by push_cast; ring, + show ((2 : ℝ≥0∞) ^ n) = ((2 ^ n : ℕ) : ℝ≥0∞) by push_cast; rfl] + exact Nat.cast_lt + +/-- **Deciding by majority is a count comparison.** A fair-coin machine decides `A` by strict +majority within `t` exactly when, on every instance, every run has halted by the clock and +`a ∈ A` exactly when more than half of the coin strings of length `t a` make the coin replay +`Turing.MultiTapePTM.runClosedCoins` output `[true]`. -/ +theorem decidesByMajorityInTime_iff {machine : MultiTapePTM k Bool State} + {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} : + machine.DecidesByMajorityInTime enc A t ↔ ∀ a, + (∀ final ∈ (ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ A ↔ 2 ^ t a < 2 * Complexity.acceptCount + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) + (enc a) (t a)) := by + refine forall_congr' fun a => and_congr_right' (iff_congr Iff.rfl ?_) + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, ← half_lt_div_iff] + simp only [Complexity.acceptCount, decide_eq_true_eq] + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM +open Cslib.Probability +open scoped ENNReal + +variable {α : Type*} + +/-- The problems decidable by strict majority 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, +and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2` +[Gill][Gill1977]. -/ +def PPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := + {A | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) + (machine : MultiTapePTM k Bool State), + machine.DecidesByMajorityInTime enc A fun a => c₁ * t (enc a).length + c₂} + +/-- `PPTIME` is monotone in the time bound. -/ +theorem PPTIME_mono {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : + PPTIME enc t₁ ⊆ PPTIME enc t₂ := by + rintro A ⟨c₁, c₂, k, State, hfinite, machine, hA⟩ + exact ⟨c₁, c₂, k, State, hfinite, machine, + hA.mono fun a => Nat.add_le_add_right (Nat.mul_le_mul_left _ (h _)) _⟩ + +/-- **Bounded error is a strict majority**: a machine outputting the right answer with probability +at least `2 / 3` outputs `[true]` with probability at least `2 / 3` on members, and at most `1 / 3` +on the others. -/ +theorem BPTIME_subset_PPTIME {enc : α ↪ List Bool} {t : ℕ → ℕ} : + BPTIME enc t ⊆ PPTIME enc t := by + rintro A ⟨c₁, c₂, k, State, hfinite, machine, hA⟩ + refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hA a).1, ?_⟩⟩ + have hprob := (hA a).2 + set p := ProbComp.eval (machine.runClosed (c₁ * t (enc a).length + c₂) (enc a)) + have hhalf : (1 / 2 : ℝ≥0∞) < 2 / 3 := by + refine (ENNReal.toReal_lt_toReal (ENNReal.div_ne_top (by norm_num) (by norm_num)) + (ENNReal.div_ne_top (by norm_num) (by norm_num))).mp ?_ + simp only [ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_ofNat] + norm_num + by_cases ha : a ∈ A + · simp only [MultiTapeTM.indicator, ha, ↓reduceIte] at hprob + exact iff_of_true ha (hhalf.trans_le hprob) + · simp only [MultiTapeTM.indicator, ha, ↓reduceIte] at hprob + refine iff_of_false ha fun hlt => ?_ + -- the outputs `[true]` and `[false]` together have probability at most one + have hsum : p [true] + p [false] ≤ 1 := by + calc p [true] + p [false] = ∑ x ∈ {[true], [false]}, p x := by + rw [Finset.sum_pair (by simp)] + _ ≤ ∑' x, p x := sum_le_tsum _ + _ = 1 := p.tsum_coe + have h1 : (1 / 2 : ℝ≥0∞) + 1 / 2 < p [true] + 1 / 2 := + ENNReal.add_lt_add_right (by norm_num) hlt + rw [ENNReal.add_halves] at h1 + exact (h1.trans_le ((add_le_add le_rfl (hhalf.le.trans hprob)).trans hsum)).false + +/-- **`PP` is the union of the classes `PPTIME (n ^ k)`** [Gill][Gill1977]: a polynomial-time +verifier run on uniformly sampled random strings is a fair-coin machine halting within a +polynomial clock, and a fair-coin machine halting within the clock `T` is a verifier replaying +random strings of length `T`. -/ +theorem mem_PP_iff_exists_mem_PPTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} : + A ∈ PP enc ↔ ∃ k, A ∈ PPTIME enc (· ^ k) := by + rw [mem_PP] + constructor + · rintro ⟨p, V, hV, hA⟩ + -- sample a random string and run the verifier on it + let program (a : α) : ProbComp Bool := + (fun w => V (a, w)) <$> BitString.sampleList (p.eval (enc a).length) + have hcount : ComputableInPolyTime (fun a => p.eval (enc a).length) enc encUnary := + (ComputableInPolyTime.unary_eval p).comp (ComputableInPolyTime.encoding_length enc) + have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with hV + obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hprogram.exists_halting_machine + refine ⟨d, c * 2 ^ d, c, k, State, hfinite, machine, + MultiTapePTM.DecidesByMajorityInTime.mono (t := fun a => c * ((enc a).length + 1) ^ d) + (fun a => ⟨hhalt (enc a), ?_⟩) fun a => Nat.mul_add_one_pow_le_two_pow c d _⟩ + -- the encoded output `[true]` has the probability of `true` + have htrue : + (ProbComp.eval (program a)).map encBool [true] = ProbComp.eval (program a) true := by + simp [PMF.map_apply, encBool_apply] + rw [← heval a, htrue] + simp only [program, ProbComp.eval_map, BitString.eval_sampleList] + rw [BitString.uniformList_map_apply, ← acceptCount, MultiTapePTM.half_lt_div_iff] + exact hA a + · rintro ⟨d, c₁, c₂, k, State, hfinite, machine, hA⟩ + -- replay the coins + refine ⟨Polynomial.C c₁ * Polynomial.X ^ d + Polynomial.C c₂, + fun x => decide (machine.runClosedCoins x.2 (enc x.1) = [true]), + ComputableInPolyTime.decide_eq' + ((MultiTapePTM.computableInPolyTime_runClosedCoins machine).comp + ((ComputableInPolyTime.snd enc encBits).prod + ((ComputableInPolyTime.of_eq (encOut := encBits) fun _ => rfl).comp + (ComputableInPolyTime.fst enc encBits)))) + (ComputableInPolyTime.const [true]), fun a => ?_⟩ + have heval : (Polynomial.C c₁ * Polynomial.X ^ d + Polynomial.C c₂).eval (enc a).length = + c₁ * (enc a).length ^ d + c₂ := by + simp + rw [heval, ((MultiTapePTM.decidesByMajorityInTime_iff.mp hA) a).2] + rfl + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean index 93d2df6a1..57c022609 100644 --- a/Complexity/Computability/Complexity/Classes/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Time.lean @@ -45,6 +45,9 @@ instances, with a bound `t : ℕ → ℕ` of the length `n` of the encoded insta members and `[false]` for the others, with probability at least `2 / 3` [Arora and Barak, Definition 7.2][AroraBarak09]. +The unbounded-error class `Cslib.Complexity.PPTIME enc t`, decided by strict majority by the same +fair-coin machines, is in `Complexity.Computability.Complexity.Classes.PP.Time`. + Each polynomial class of the library is the union of the corresponding classes of time `O(n ^ k)`, as in the textbook [Arora and Barak, Definition 1.13, Theorem 2.6, Definition 7.2][AroraBarak09]: diff --git a/ComplexityTests/PPTime.lean b/ComplexityTests/PPTime.lean new file mode 100644 index 000000000..3e01f752b --- /dev/null +++ b/ComplexityTests/PPTime.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.Classes.Inclusions +import Complexity.Computability.Complexity.Classes.PP.Time +import Complexity.Computability.Probabilistic.PPT.Clock +import Complexity.Tactic.PPT + +/-! Unbounded-error probabilistic time: members obtained from `P` through `BPP`, `PP` and +`BPTIME`, and a halting fair-coin machine that outputs `[true]` with probability exactly `1 / 2`, +which decides `∅` by strict majority but not `Set.univ`. -/ + +namespace ComplexityTests.PPTime + +open Cslib Cslib.Complexity Cslib.Probability Turing Turing.MultiTapeTM +open scoped ENNReal + +/-- Everything is decided by the constant `true`. -/ +theorem univ_mem_P : (Set.univ : Set (List Bool)) ∈ P encBits := + ⟨fun _ => true, .const true, fun _ => by simp⟩ + +/-- The words starting with `true`: neither empty nor everything. -/ +theorem headD_mem_P : {w : List Bool | w.headD false = true} ∈ P encBits := + ⟨fun w => w.headD false, by fun_prop, fun _ => Iff.rfl⟩ + +/-- `Set.univ` and the words starting with `true` are decided by strict majority in polynomial +time, through `PP`, and for the latter also through `BPTIME`. -/ +example : + (∃ k, (Set.univ : Set (List Bool)) ∈ PPTIME encBits (· ^ k)) ∧ + (∃ k, {w : List Bool | w.headD false = true} ∈ PPTIME encBits (· ^ k)) ∧ + (∃ k, {w : List Bool | w.headD false = true} ∈ PPTIME encBits (· ^ k)) := + ⟨mem_PP_iff_exists_mem_PPTIME.mp (BPP_subset_PP (P_subset_BPP univ_mem_P)), + mem_PP_iff_exists_mem_PPTIME.mp (BPP_subset_PP (P_subset_BPP headD_mem_P)), + let ⟨k, hk⟩ := mem_BPP_iff_exists_mem_BPTIME.mp (P_subset_BPP headD_mem_P) + ⟨k, BPTIME_subset_PPTIME hk⟩⟩ + +/-- A membership in `PPTIME (n ^ k)` gives back `PP`. -/ +example {A : Set (List Bool)} {k : ℕ} (h : A ∈ PPTIME encBits (· ^ k)) : A ∈ PP encBits := + mem_PP_iff_exists_mem_PPTIME.mpr ⟨k, h⟩ + +/-- **Strictness matters.** A halting fair-coin machine that outputs `[true]` with probability +exactly `1 / 2` decides `∅` by strict majority, and does not decide `Set.univ`. -/ +example : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) + (t : List Bool → ℕ), machine.DecidesByMajorityInTime encBits ∅ t ∧ + ¬ machine.DecidesByMajorityInTime encBits Set.univ t := by + have hcoin : IsPPTOn encBits encBool (fun _ => ProbComp.uniform Bool) := by fun_prop + obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hcoin.exists_halting_machine + have hhalf (w : List Bool) : + ProbComp.eval (machine.runClosed (c * ((encBits w).length + 1) ^ d) (encBits w)) [true] = + 1 / 2 := by + rw [← heval w] + simp [PMF.map_apply, encBool_apply] + refine ⟨k, State, hfinite, machine, fun w => c * ((encBits w).length + 1) ^ d, + fun w => ⟨hhalt w, ?_⟩, fun h => ?_⟩ + · rw [hhalf] + simp + · have := ((h []).2.mp (Set.mem_univ _)) + rw [hhalf] at this + exact lt_irrefl _ this + +/-- The count form of the majority condition: a machine deciding `Set.univ` by strict majority +accepts more than half of the coin strings of clock length on every word. -/ +example {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) {t : List Bool → ℕ} + (h : machine.DecidesByMajorityInTime encBits Set.univ t) (w : List Bool) : + 2 ^ t w < 2 * acceptCount + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) w (t w) := + ((MultiTapePTM.decidesByMajorityInTime_iff.mp h) w).2.mp (Set.mem_univ w) + +end ComplexityTests.PPTime From 6f551680dd16ee5045925ad1d2643da3a62d2cc1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:54:12 -0400 Subject: [PATCH 2/3] refactor(Classes/PP): derive the majority count form from acceptCount_le_half_iff Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/PP/Time.lean | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean index 5775864e3..53c78531d 100644 --- a/Complexity/Computability/Complexity/Classes/PP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -90,16 +90,15 @@ theorem DecidesByMajorityInTime.mono {machine : MultiTapePTM k Bool State} exact hhalt · rwa [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] -/-- A probability `c / 2 ^ n` exceeds one half exactly when `2 ^ n < 2 * c`. -/ -private theorem half_lt_div_iff {c n : ℕ} : - (1 / 2 : ℝ≥0∞) < c / 2 ^ n ↔ 2 ^ n < 2 * c := by - have h2n : (2 : ℝ≥0∞) ^ n ≠ 0 := pow_ne_zero _ two_ne_zero - have h2n' : (2 : ℝ≥0∞) ^ n ≠ ⊤ := ENNReal.pow_ne_top ENNReal.ofNat_ne_top - rw [ENNReal.lt_div_iff_mul_lt (Or.inl h2n) (Or.inl h2n'), one_div, mul_comm, - ← div_eq_mul_inv, ENNReal.div_lt_iff (Or.inl two_ne_zero) (Or.inl ENNReal.ofNat_ne_top), - show ((c : ℝ≥0∞) * 2) = ((2 * c : ℕ) : ℝ≥0∞) by push_cast; ring, - show ((2 : ℝ≥0∞) ^ n) = ((2 ^ n : ℕ) : ℝ≥0∞) by push_cast; rfl] - exact Nat.cast_lt +/-- More than half of the random words are accepted exactly when they are accepted with +probability more than one half. -/ +private theorem half_lt_uniformList_map_iff {β : Type} (V : β × List Bool → Bool) (b : β) + (n : ℕ) : 1 / 2 < ((BitString.uniformList n).map fun w => V (b, w)) true ↔ + 2 ^ n < 2 * Complexity.acceptCount V b n := by + have hne : ((BitString.uniformList n).map fun w => V (b, w)) true ≠ ⊤ := PMF.apply_ne_top _ _ + rw [← not_iff_not, not_lt, not_lt, Complexity.acceptCount_le_half_iff, + ← ENNReal.toReal_le_toReal hne (by simp)] + simp /-- **Deciding by majority is a count comparison.** A fair-coin machine decides `A` by strict majority within `t` exactly when, on every instance, every run has halted by the clock and @@ -115,8 +114,16 @@ theorem decidesByMajorityInTime_iff {machine : MultiTapePTM k Bool State} (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) (enc a) (t a)) := by refine forall_congr' fun a => and_congr_right' (iff_congr Iff.rfl ?_) - rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, ← half_lt_div_iff] - simp only [Complexity.acceptCount, decide_eq_true_eq] + -- the probability of `[true]` is the accepted fraction of the coin strings + have hprob : ProbComp.eval (machine.runClosed (t a) (enc a)) [true] = + ((BitString.uniformList (t a)).map fun w => + decide (machine.runClosedCoins w (enc a) = [true])) true := by + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, + BitString.uniformList_map_apply] + simp only [decide_eq_true_eq] + rw [hprob] + exact half_lt_uniformList_map_iff + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) _ _ end Turing.MultiTapePTM @@ -200,7 +207,7 @@ theorem mem_PP_iff_exists_mem_PPTIME {α : Type} {enc : α ↪ List Bool} {A : S simp [PMF.map_apply, encBool_apply] rw [← heval a, htrue] simp only [program, ProbComp.eval_map, BitString.eval_sampleList] - rw [BitString.uniformList_map_apply, ← acceptCount, MultiTapePTM.half_lt_div_iff] + rw [MultiTapePTM.half_lt_uniformList_map_iff] exact hA a · rintro ⟨d, c₁, c₂, k, State, hfinite, machine, hA⟩ -- replay the coins From 9d3a07815efe9d48e13fef808b0264ca57cecf9f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:27:52 -0400 Subject: [PATCH 3/3] doc(Classes/PP): state the PPTIME threshold as a library convention Address the #1847 review: stop attributing the timed predicate to Gill. The module docstring now records the convention: strict acceptance, ties reject, outputs other than `[true]` unconstrained. It also records that the agreement with `PP` is a union over polynomial clocks and that no fixed-time comparison with other conventions is proved. Gill stays as background in the references. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/PP/Time.lean | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean index 53c78531d..ed5778dab 100644 --- a/Complexity/Computability/Complexity/Classes/PP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -24,9 +24,19 @@ import Complexity.Computability.Probabilistic.Sampling `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, by a fair-coin machine with a binary alphabet and finitely many states (`Turing.MultiTapePTM.DecidesByMajorityInTime`): every run on that many coins has halted, and `a ∈ A` exactly when the run outputs `[true]` with -probability more than `1 / 2` [Gill][Gill1977]. It is the unbounded-error counterpart of +probability more than `1 / 2`. It is the unbounded-error counterpart of `Cslib.Complexity.BPTIME`, with the same machines and clocks. +**Convention.** Unbounded-error probabilistic computation goes back to Gill [Gill1977]. The timed +predicate here is this library's convention, not a transcription of a source definition: acceptance +is strict and ties reject. A nonmember may output `[true]` with probability exactly `1 / 2`, and +its other outputs are unconstrained, so it need not output `[false]` with probability more than +`1 / 2`. This is the threshold of the library's verifier-based `PP` +(`Cslib.Complexity.DecidesByMajority`), and the two agree at polynomial time +(`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`). That equivalence is a union over all polynomial +clocks; for a fixed time bound, no comparison with conventions that require a strict majority of +`[false]` on nonmembers is proved here. + A fair-coin machine draws one coin per live step, so its acceptance probability within the clock `t` is the number of accepting coin strings of length `t` divided by `2 ^ t`. Deciding by majority is therefore the comparison `2 ^ t < 2 * count` of that count, an `Cslib.Complexity.acceptCount` @@ -71,7 +81,9 @@ variable {k : ℕ} {State : Type} {α : Type*} /-- `machine` decides `A` by strict majority within `t`, relative to the encoding `enc`: on every encoded instance `enc a`, every run of `t a` steps with fair coins has halted, and `a ∈ A` exactly -when the run outputs `[true]` with probability more than `1 / 2` [Gill][Gill1977]. -/ +when the run outputs `[true]` with probability more than `1 / 2`. Ties reject, and outputs other +than `[true]` are unconstrained; this is the library's convention, described in the module +docstring. -/ def DecidesByMajorityInTime (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (t : α → ℕ) : Prop := ∀ a, (∀ final ∈ (ProbComp.eval @@ -138,8 +150,8 @@ variable {α : Type*} /-- The problems decidable by strict majority 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, -and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2` -[Gill][Gill1977]. -/ +and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2`. Ties reject +(`Turing.MultiTapePTM.DecidesByMajorityInTime`). -/ def PPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := {A | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State), @@ -182,7 +194,7 @@ theorem BPTIME_subset_PPTIME {enc : α ↪ List Bool} {t : ℕ → ℕ} : rw [ENNReal.add_halves] at h1 exact (h1.trans_le ((add_le_add le_rfl (hhalf.le.trans hprob)).trans hsum)).false -/-- **`PP` is the union of the classes `PPTIME (n ^ k)`** [Gill][Gill1977]: a polynomial-time +/-- **`PP` is the union of the classes `PPTIME (n ^ k)`**: a polynomial-time verifier run on uniformly sampled random strings is a fair-coin machine halting within a polynomial clock, and a fair-coin machine halting within the clock `T` is a verifier replaying random strings of length `T`. -/