From b753a96a5dc69d1def1f70f9cab8ef7882716312 Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 08:00:45 +0000 Subject: [PATCH 1/3] feat(CountingSimulation): simulate PromiseBPP completions conditionally --- Complexity.lean | 2 + .../Complexity/Classes/Constructible.lean | 11 +++ .../Classes/CountingSimulation/Promise.lean | 83 +++++++++++++++++++ .../Computability/Complexity/Classes/PP.lean | 41 ++++++--- .../Complexity/Classes/Promise/PP.lean | 49 +++++++++++ .../PromiseCountingSimulation.lean | 39 +++++++++ ComplexityTests/PromisePP.lean | 55 ++++++++++++ 7 files changed, 267 insertions(+), 13 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean create mode 100644 Complexity/Computability/Complexity/Classes/Promise/PP.lean create mode 100644 ComplexityTests/PromiseCountingSimulation.lean create mode 100644 ComplexityTests/PromisePP.lean diff --git a/Complexity.lean b/Complexity.lean index 3e9cd54e70..6c6d99ffa8 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1118,6 +1118,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Blo public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments public import Complexity.Computability.Complexity.Classes.CountingSimulation.Guarded public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Promise public import Complexity.Computability.Complexity.Classes.DP public import Complexity.Computability.Complexity.Classes.EXP public import Complexity.Computability.Complexity.Classes.FewP @@ -1227,6 +1228,7 @@ public import Complexity.Computability.Complexity.Classes.ParityP public import Complexity.Computability.Complexity.Classes.ParityP.Closure public import Complexity.Computability.Complexity.Classes.Promise.Basic public import Complexity.Computability.Complexity.Classes.Promise.Circuit +public import Complexity.Computability.Complexity.Classes.Promise.PP public import Complexity.Computability.Complexity.Classes.Promise.Probabilistic public import Complexity.Computability.Complexity.Classes.Promise.Randomized public import Complexity.Computability.Complexity.Classes.Promise.Reduction diff --git a/Complexity/Computability/Complexity/Classes/Constructible.lean b/Complexity/Computability/Complexity/Classes/Constructible.lean index 46cc7fb9d0..118c29cad0 100644 --- a/Complexity/Computability/Complexity/Classes/Constructible.lean +++ b/Complexity/Computability/Complexity/Classes/Constructible.lean @@ -41,6 +41,7 @@ length is supplied by the quantitative API (`Turing.MultiTapeTM.ComputableInO.le * `Cslib.Complexity.timeConstructible_two_pow`, `Cslib.Complexity.timeConstructible_two_pow_two_pow`, `Cslib.Complexity.timeConstructible_succ_pow`, + `Cslib.Complexity.TimeConstructible.succ`, `Cslib.Complexity.TimeConstructible.succ_mul`: time-constructible bounds. * `Cslib.Complexity.spaceConstructible_const`, `Cslib.Complexity.spaceConstructible_id`, `Cslib.Complexity.spaceConstructible_succ`, `Cslib.Complexity.spaceConstructible_succ_pow`, @@ -101,6 +102,16 @@ theorem TimeConstructible.of_computableInO {t : ℕ → ℕ} {T S : List Bool · simp only [encBits_apply] exact Nat.mul_le_mul_left k (Nat.add_le_add_right (hS x) 1) +/-- Adding one to a time-constructible bound preserves time constructibility. -/ +theorem TimeConstructible.succ {t : ℕ → ℕ} (ht : TimeConstructible t) : + TimeConstructible fun n => t n + 1 := by + have h := (ComputableInO.of_linear ComputableInLinearTimeAndSpace.natSucc).comp + ht.computableInO + refine TimeConstructible.of_computableInO (s := fun n => t n + (encNat (t n)).length) 2 h + (fun x => ?_) fun _ => le_rfl + have hlen := length_encNat_le (t x.length) + omega + /-- `2 ^ n` is time-constructible: its binary digits are `n` zeros followed by a one. -/ theorem timeConstructible_two_pow : TimeConstructible (2 ^ ·) := TimeConstructible.of_computableInO 1 diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean new file mode 100644 index 0000000000..4b95cae7db --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean @@ -0,0 +1,83 @@ +/- +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.CountingSimulation.BlockNetworks +public import Complexity.Computability.Complexity.Classes.Promise.PP + +/-! +# Conditional deterministic completions of PromiseBPP + +Every problem in `PromiseBPP` has a strict-majority completion in `PP`. Applying the counting +simulation to that completion gives one total deterministic machine that separates the yes- and +no-instances, with the counting simulation's joint time and workspace bounds. The contraction +algorithm for admissible explicit networks remains an explicit hypothesis. + +The polynomial clock is `T n = (n + 1) ^ (k + 2) + 1`, for some `k` depending on the completion. +It is time-constructible and at least `max n 2`, including at `n = 0`. The simulation uses time +`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`. Outside the promise, the completion +may answer either way. This does not give a `BPP` completion, a gate-count bound, or a bound +subexponential in input length for every polynomial clock. + +These are corollaries of the existing majority and counting interfaces, addressing the promise +extension of #1833. They do not discharge the contraction hypothesis or the unconditional +simulation objective. + +## Main results + +* `exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm`: the joint bounds for a + problem in `PP`, at a polynomial clock meeting the simulation's hypotheses. +* `exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm`: a deterministic completion of + a `PromiseBPP` problem with the same joint bounds. +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM Cslib.Circuits.Frontier.ExplicitTensorNetwork + +variable {α : Type} {enc : α ↪ List Bool} + +/-- A problem in `PP` is decidable by one machine within the counting simulation's time and +polynomial-workspace bounds, at a polynomial clock, conditional on the contraction algorithm. -/ +theorem exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm + (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) + ExplicitAdmissible) {L : Set α} (hL : L ∈ PP enc) : + ∃ k C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * (((enc a).length + 1) ^ (k + 2) + 1) / + Nat.sqrt (Nat.log 2 (((enc a).length + 1) ^ (k + 2) + 1)))) + (fun a => (((enc a).length + 1) ^ (k + 2) + 1) ^ d) := by + obtain ⟨k, hk⟩ := mem_PP_iff_exists_mem_PPTIME.mp hL + have hT := (timeConstructible_succ_pow (k := k + 2) (by omega)).succ + have hbound (n : ℕ) : max n 2 ≤ (n + 1) ^ (k + 2) + 1 := by + have := Nat.le_self_pow (by omega : k + 2 ≠ 0) (n + 1) + omega + have hclock (n : ℕ) : n ^ k ≤ (n + 1) ^ (k + 2) + 1 := + (Nat.pow_le_pow_left (Nat.le_succ n) k).trans + ((Nat.pow_le_pow_right (by omega) (by omega)).trans (Nat.le_succ _)) + obtain ⟨C, d, h⟩ := exists_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm + A hT hbound (PPTIME_mono hclock hk) + exact ⟨k, C, d, h⟩ + +/-- Every `PromiseBPP` problem has a total deterministic completion with simultaneous time +`2 ^ O(T / √(log T))` and workspace polynomial in the polynomial clock `T`, conditional on the +explicit contraction algorithm. No answer is prescribed outside the promise. -/ +theorem exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm + (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) + ExplicitAdmissible) {Q : PromiseProblem α} (hQ : Q ∈ PromiseBPP enc) : + ∃ (L : Set α) (k C d : ℕ), Q.yes ⊆ L ∧ Disjoint L Q.no ∧ + DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * (((enc a).length + 1) ^ (k + 2) + 1) / + Nat.sqrt (Nat.log 2 (((enc a).length + 1) ^ (k + 2) + 1)))) + (fun a => (((enc a).length + 1) ^ (k + 2) + 1) ^ d) := by + obtain ⟨L, hL, hyes, hno⟩ := PromiseBPP_subset_promiseClass_PP hQ + obtain ⟨k, C, d, h⟩ := exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm A hL + exact ⟨L, k, C, d, hyes, hno, h⟩ + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean index adc5b38ba6..69dfef0aee 100644 --- a/Complexity/Computability/Complexity/Classes/PP.lean +++ b/Complexity/Computability/Complexity/Classes/PP.lean @@ -38,6 +38,8 @@ characterisation by fair-coin machines deciding by strict majority within polyno ## Main results +* `Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.solvedBy_majority`: bounded error + gives a strict-majority solver on the promise. * `Cslib.Complexity.DecidesWithBoundedError.decidesByMajority`: bounded error gives a majority. * `Cslib.Complexity.BPP_subset_PP`. @@ -74,24 +76,37 @@ theorem mem_PP {A : Set α} : A ∈ PP enc ↔ ∃ (p : Polynomial ℕ) (V : α ComputableInPolyTime V (encPair enc encBits) encBool ∧ DecidesByMajority enc p V A := Iff.rfl +/-- A bounded-error verifier solves its promise problem by strict majority. Ties reject, and +there is no error-margin requirement outside the promise. -/ +theorem PromiseProblem.SolvesWithBoundedError.solvedBy_majority {p : Polynomial ℕ} + {V : α × List Bool → Bool} {Q : PromiseProblem α} + (h : Q.SolvesWithBoundedError enc p V) : + Q.SolvedBy (fun a => decide + (2 ^ p.eval (enc a).length < 2 * acceptCount V a (p.eval (enc a).length))) := by + constructor + · intro a ha + have hyes := (h a).1 ha + have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length) + unfold BoundedErrorAt at hyes + rw [← acceptCount] at hyes + simp only [decide_eq_true_eq] + omega + · intro a ha + have hno := (h a).2 ha + have hsum := acceptCount_add_card_filter_eq_false + (V := V) (a := a) (n := p.eval (enc a).length) + unfold BoundedErrorAt at hno + simp only [decide_eq_false_iff_not] + omega + /-- Bounded error gives a majority: a decider that is right on at least two thirds of the random strings accepts the members of its problem, and only them, on more than half. -/ theorem DecidesWithBoundedError.decidesByMajority {p : Polynomial ℕ} {V : α × List Bool → Bool} {A : Set α} (h : DecidesWithBoundedError enc p V A) : DecidesByMajority enc p V A := by intro a - have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length) - have hpos := Nat.one_le_two_pow (n := p.eval (enc a).length) - constructor - · intro ha - have := (h a).1 ha - unfold BoundedErrorAt at this - rw [← acceptCount] at this - omega - · intro hlt - by_contra ha - have := (h a).2 ha - unfold BoundedErrorAt at this - omega + simpa only [decide_eq_true_eq] using + (PromiseProblem.solvedBy_ofSet.mp + (PromiseProblem.SolvesWithBoundedError.solvedBy_majority h) a) /-- **`BPP ⊆ PP`.** -/ theorem BPP_subset_PP : BPP enc ⊆ PP enc := diff --git a/Complexity/Computability/Complexity/Classes/Promise/PP.lean b/Complexity/Computability/Complexity/Classes/Promise/PP.lean new file mode 100644 index 0000000000..e8847e5eff --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Promise/PP.lean @@ -0,0 +1,49 @@ +/- +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.Promise.Basic + +/-! +# Strict-majority completions of bounded-error promise problems + +A verifier for `PromiseBPP` gives a language in `PP` separating its yes- and no-instances: +accept exactly when strictly more than half of its random strings are accepted. This is a direct +consequence of the existing bounded-error and strict-majority definitions. Ties are rejected; +outside the promise, no bounded-error margin is asserted for the completion. + +## Main results + +* `Cslib.Complexity.PromiseBPP_subset_promiseClass_PP`: every bounded-error promise problem + has a strict-majority completion in `PP`. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +/-- Every problem in `PromiseBPP` has a completion in `PP`, using the same seeded verifier. +The completion accepts by strict majority, including on inputs outside the promise. -/ +theorem PromiseBPP_subset_promiseClass_PP {α : Type} {enc : α ↪ List Bool} : + PromiseBPP enc ⊆ promiseClass (PP enc) := by + rintro Q ⟨p, V, hV, hQ⟩ + let L : Set α := {a | 2 ^ p.eval (enc a).length < + 2 * acceptCount V a (p.eval (enc a).length)} + have hsolve := hQ.solvedBy_majority + refine ⟨L, ⟨p, V, hV, fun _ => Iff.rfl⟩, ?_, ?_⟩ + · intro a ha + exact of_decide_eq_true (hsolve.1 a ha) + · refine Set.disjoint_right.mpr fun a ha hL => ?_ + have hno := hsolve.2 a ha + simp only [decide_eq_false_iff_not] at hno + exact hno hL + +end Cslib.Complexity diff --git a/ComplexityTests/PromiseCountingSimulation.lean b/ComplexityTests/PromiseCountingSimulation.lean new file mode 100644 index 0000000000..8dcf047724 --- /dev/null +++ b/ComplexityTests/PromiseCountingSimulation.lean @@ -0,0 +1,39 @@ +/- +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.CountingSimulation.Promise +import ComplexityTests.PromisePP + +/-! The conditional counting simulation on a genuinely partial promise. + +The completion contains `[true]` and excludes `[false]`; its one machine retains both resource +bounds. The verifier's exact tie on the empty word is checked in `ComplexityTests.PromisePP`. +-/ + +namespace ComplexityTests.PromiseCountingSimulation + +open Cslib.Complexity Cslib.Complexity.CountingSimulation Turing.MultiTapeTM + Cslib.Circuits.Frontier.ExplicitTensorNetwork ComplexityTests.PromiseProbabilistic + ComplexityTests.PromisePP + +/-- A concrete partial promise gets a total deterministic completion with the joint bounds. +The contraction algorithm is the only unproved interface assumed by this client. -/ +example (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) + ExplicitAdmissible) : + ∃ (L : Set (List Bool)) (k C d : ℕ), [true] ∈ L ∧ [false] ∉ L ∧ + DecidableInTimeAndSpace L encBits + (fun a => 2 ^ (C * ((a.length + 1) ^ (k + 2) + 1) / + Nat.sqrt (Nat.log 2 ((a.length + 1) ^ (k + 2) + 1)))) + (fun a => ((a.length + 1) ^ (k + 2) + 1) ^ d) := by + have hQ : partialSingletonBit ∈ PromiseBPP encBits := + ⟨1, partialVerifier, partialVerifier_polyTime, + solvesWithBoundedError_partialSingletonBit⟩ + obtain ⟨L, k, C, d, hyes, hno, h⟩ := + exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm A hQ + refine ⟨L, k, C, d, hyes rfl, ?_, h⟩ + exact Set.disjoint_right.mp hno rfl + +end ComplexityTests.PromiseCountingSimulation diff --git a/ComplexityTests/PromisePP.lean b/ComplexityTests/PromisePP.lean new file mode 100644 index 0000000000..1a37e09e8e --- /dev/null +++ b/ComplexityTests/PromisePP.lean @@ -0,0 +1,55 @@ +/- +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.Promise.PP +import ComplexityTests.PromiseProbabilistic + +/-! A strict-majority completion of a genuinely partial promise problem. + +The reused verifier answers the first input bit on the promised singleton words, but answers a +fair coin on the empty word. Majority still solves the promise, with ties rejecting on `[]`. +-/ + +namespace ComplexityTests.PromisePP + +open Cslib.Complexity Turing.MultiTapeTM ComplexityTests.PromiseProbabilistic + +/-- The fixture's computed fallback can be expressed through an emptiness test and fixed heads. -/ +theorem partialVerifier_polyTime : + ComputableInPolyTime partialVerifier (encPair encBits encBits) encBool := by + have heq : partialVerifier = fun p : List Bool × List Bool => + if p.1.isEmpty then p.2.headD false else p.1.headD false := by + funext ⟨x, r⟩ + cases x <;> rfl + rw [heq] + fun_prop + +/-- Majority solves the promised yes- and no-instances even though the empty word has no gap. -/ +example : partialSingletonBit.SolvedBy (fun a => decide + (2 ^ 1 < 2 * acceptCount partialVerifier a 1)) := by + simpa only [Polynomial.eval_one] using + solvesWithBoundedError_partialSingletonBit.solvedBy_majority + +/-- The unpromised empty word is an exact tie and is rejected by the strict-majority rule. -/ +example : ([] : List Bool) ∉ partialSingletonBit.promise ∧ + acceptCount partialVerifier [] 1 = 1 ∧ + decide (2 ^ 1 < 2 * acceptCount partialVerifier [] 1) = false := by + constructor + · simp [partialSingletonBit, PromiseProblem.promise] + · decide + +/-- The class-level inclusion supplies a `PP` language containing the yes-word and excluding the +no-word, with no requirement on how that language answers other words. -/ +example : ∃ L ∈ PP encBits, [true] ∈ L ∧ [false] ∉ L := by + have hQ : partialSingletonBit ∈ PromiseBPP encBits := + ⟨1, partialVerifier, partialVerifier_polyTime, + solvesWithBoundedError_partialSingletonBit⟩ + obtain ⟨L, hL, hyes, hno⟩ := PromiseBPP_subset_promiseClass_PP hQ + refine ⟨L, hL, hyes rfl, ?_⟩ + intro hm + exact Set.disjoint_left.mp hno hm rfl + +end ComplexityTests.PromisePP From e2b86d72d7239bf673f01201dc2b1e1f3c62fdcc Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 08:10:10 +0000 Subject: [PATCH 2/3] chore: credit Christian Reitwiessner in new file headers --- .../Complexity/Classes/CountingSimulation/Promise.lean | 4 ++-- Complexity/Computability/Complexity/Classes/Promise/PP.lean | 4 ++-- ComplexityTests/PromiseCountingSimulation.lean | 4 ++-- ComplexityTests/PromisePP.lean | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean index 4b95cae7db..b38aa7def9 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Christian Reitwiessner -/ module diff --git a/Complexity/Computability/Complexity/Classes/Promise/PP.lean b/Complexity/Computability/Complexity/Classes/Promise/PP.lean index e8847e5eff..feda796778 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/PP.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/PP.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Christian Reitwiessner -/ module diff --git a/ComplexityTests/PromiseCountingSimulation.lean b/ComplexityTests/PromiseCountingSimulation.lean index 8dcf047724..f6855d1a0c 100644 --- a/ComplexityTests/PromiseCountingSimulation.lean +++ b/ComplexityTests/PromiseCountingSimulation.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Christian Reitwiessner -/ import Complexity.Computability.Complexity.Classes.CountingSimulation.Promise diff --git a/ComplexityTests/PromisePP.lean b/ComplexityTests/PromisePP.lean index 1a37e09e8e..50a219a181 100644 --- a/ComplexityTests/PromisePP.lean +++ b/ComplexityTests/PromisePP.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Christian Reitwiessner -/ import Complexity.Computability.Complexity.Classes.Promise.PP From 91b95cac2fc3be247f8e6af158960e25c296cb8a Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 15:28:31 +0000 Subject: [PATCH 3/3] fix(complexity): preserve caller clocks in promise simulation Replace the existential polynomial-clock statements with a native PromiseBPTIME contract and a strict-majority PPTIME completion at the same affine clock. Apply main FastSimulation to obtain one unconditional deterministic completion with the caller-supplied T and independent polynomial workspace. Preserve the verifier-defined PromiseBPP-to-PP theorem and distinguish the unproved quantitative verifier/native comparison. Concrete native tests cover both promised singleton words, an off-promise exact tie and a fixed quadratic-clock deterministic certificate. Strict affected-module and PP client builds, module lint, full style, aggregate, hygiene and whitespace checks pass. Independent Codex review approved the substantive delta; full hosted validation is pending. AI-assisted with Codex; new file credits Christian Reitwiessner. --- Complexity.lean | 1 + .../Classes/CountingSimulation/Promise.lean | 83 ++++-------- .../Complexity/Classes/Promise/Time.lean | 128 ++++++++++++++++++ .../PromiseCountingSimulation.lean | 116 +++++++++++++--- 4 files changed, 249 insertions(+), 79 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Promise/Time.lean diff --git a/Complexity.lean b/Complexity.lean index 2460210898..80806033ed 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1284,6 +1284,7 @@ public import Complexity.Computability.Complexity.Classes.Promise.PP public import Complexity.Computability.Complexity.Classes.Promise.Probabilistic public import Complexity.Computability.Complexity.Classes.Promise.Randomized public import Complexity.Computability.Complexity.Classes.Promise.Reduction +public import Complexity.Computability.Complexity.Classes.Promise.Time public import Complexity.Computability.Complexity.Classes.RP public import Complexity.Computability.Complexity.Classes.RP.Closure public import Complexity.Computability.Complexity.Classes.RepeatedTrials diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean index b38aa7def9..5471d89e5d 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Promise.lean @@ -7,77 +7,46 @@ Authors: Christian Reitwiessner module -- upstream: candidate -public import Complexity.Computability.Complexity.Classes.CountingSimulation.BlockNetworks -public import Complexity.Computability.Complexity.Classes.Promise.PP +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastSimulation +public import Complexity.Computability.Complexity.Classes.Promise.Time /-! -# Conditional deterministic completions of PromiseBPP +# Deterministic promise completions at a prescribed clock -Every problem in `PromiseBPP` has a strict-majority completion in `PP`. Applying the counting -simulation to that completion gives one total deterministic machine that separates the yes- and -no-instances, with the counting simulation's joint time and workspace bounds. The contraction -algorithm for admissible explicit networks remains an explicit hypothesis. +A native bounded-error promise solver running in time `T` has a strict-majority completion in +`PPTIME T`, at the same clock. The unconditional counting simulation then gives one deterministic +machine deciding that completion in time `2 ^ (C T / √⌊log₂ T⌋)` and workspace `T ^ d`. +The caller supplies `T`, its constructibility and `max n 2 ≤ T n`. Only the simulation constants +are existential: the time scale cannot be weakened by choosing a larger polynomial afterward. -The polynomial clock is `T n = (n + 1) ^ (k + 2) + 1`, for some `k` depending on the completion. -It is time-constructible and at least `max n 2`, including at `n = 0`. The simulation uses time -`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and workspace `T n ^ d`. Outside the promise, the completion -may answer either way. This does not give a `BPP` completion, a gate-count bound, or a bound -subexponential in input length for every polynomial clock. - -These are corollaries of the existing majority and counting interfaces, addressing the promise -extension of #1833. They do not discharge the contraction hypothesis or the unconditional -simulation objective. +Answers outside the promise are unrestricted. This is not a bounded-error total completion. +The verifier-defined `PromiseBPP` completion in `PP` is separately proved in `Promise.PP`; +no clock-preserving equivalence between that verifier definition and `PromiseBPTIME` is asserted. ## Main results -* `exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm`: the joint bounds for a - problem in `PP`, at a polynomial clock meeting the simulation's hypotheses. -* `exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm`: a deterministic completion of - a `PromiseBPP` problem with the same joint bounds. +* `exists_completion_of_mem_PromiseBPTIME`: one deterministic completion with the prescribed + subexponential time and independent polynomial-workspace bounds. -/ public section namespace Cslib.Complexity.CountingSimulation -open Turing.MultiTapeTM Cslib.Circuits.Frontier.ExplicitTensorNetwork - -variable {α : Type} {enc : α ↪ List Bool} - -/-- A problem in `PP` is decidable by one machine within the counting simulation's time and -polynomial-workspace bounds, at a polynomial clock, conditional on the contraction algorithm. -/ -theorem exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm - (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) - ExplicitAdmissible) {L : Set α} (hL : L ∈ PP enc) : - ∃ k C d : ℕ, DecidableInTimeAndSpace L enc - (fun a => 2 ^ (C * (((enc a).length + 1) ^ (k + 2) + 1) / - Nat.sqrt (Nat.log 2 (((enc a).length + 1) ^ (k + 2) + 1)))) - (fun a => (((enc a).length + 1) ^ (k + 2) + 1) ^ d) := by - obtain ⟨k, hk⟩ := mem_PP_iff_exists_mem_PPTIME.mp hL - have hT := (timeConstructible_succ_pow (k := k + 2) (by omega)).succ - have hbound (n : ℕ) : max n 2 ≤ (n + 1) ^ (k + 2) + 1 := by - have := Nat.le_self_pow (by omega : k + 2 ≠ 0) (n + 1) - omega - have hclock (n : ℕ) : n ^ k ≤ (n + 1) ^ (k + 2) + 1 := - (Nat.pow_le_pow_left (Nat.le_succ n) k).trans - ((Nat.pow_le_pow_right (by omega) (by omega)).trans (Nat.le_succ _)) - obtain ⟨C, d, h⟩ := exists_decidableInTimeAndSpace_of_mem_PPTIME_of_contractionAlgorithm - A hT hbound (PPTIME_mono hclock hk) - exact ⟨k, C, d, h⟩ +open _root_.Turing.MultiTapeTM -/-- Every `PromiseBPP` problem has a total deterministic completion with simultaneous time -`2 ^ O(T / √(log T))` and workspace polynomial in the polynomial clock `T`, conditional on the -explicit contraction algorithm. No answer is prescribed outside the promise. -/ -theorem exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm - (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) - ExplicitAdmissible) {Q : PromiseProblem α} (hQ : Q ∈ PromiseBPP enc) : - ∃ (L : Set α) (k C d : ℕ), Q.yes ⊆ L ∧ Disjoint L Q.no ∧ +/-- A native promise problem at caller-supplied time `T` has a deterministic completion within +`2 ^ O(T / √log T)` time and polynomial workspace, with one realizing machine. -/ +theorem exists_completion_of_mem_PromiseBPTIME {α : Type} {enc : α ↪ List Bool} + {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) + {Q : PromiseProblem α} (hQ : Q ∈ PromiseBPTIME enc T) : + ∃ (L : Set α) (C d : ℕ), Q.yes ⊆ L ∧ Disjoint L Q.no ∧ DecidableInTimeAndSpace L enc - (fun a => 2 ^ (C * (((enc a).length + 1) ^ (k + 2) + 1) / - Nat.sqrt (Nat.log 2 (((enc a).length + 1) ^ (k + 2) + 1)))) - (fun a => (((enc a).length + 1) ^ (k + 2) + 1) ^ d) := by - obtain ⟨L, hL, hyes, hno⟩ := PromiseBPP_subset_promiseClass_PP hQ - obtain ⟨k, C, d, h⟩ := exists_decidableInTimeAndSpace_of_mem_PP_of_contractionAlgorithm A hL - exact ⟨L, k, C, d, hyes, hno, h⟩ + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := by + obtain ⟨L, hL, hyes, hno⟩ := PromiseBPTIME_subset_promiseClass_PPTIME hQ + obtain ⟨C, d, h⟩ := + exists_decidableInTimeAndSpace_two_pow_div_sqrt_log_two_of_mem_PPTIME hT hTn hL + exact ⟨L, C, d, hyes, hno, h⟩ end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/Promise/Time.lean b/Complexity/Computability/Complexity/Classes/Promise/Time.lean new file mode 100644 index 0000000000..c3bfe88d4f --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Promise/Time.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.PP.Time +public import Complexity.Computability.Complexity.Classes.Promise.Basic + +/-! +# Bounded-error promise computation at a prescribed time + +`PromiseBPTIME enc T` fixes a native fair-coin machine and an affine clock `c₁ * T n + c₂` +before the input. Every run halts within that clock, including off-promise runs. On yes-instances +the output is `[true]` with probability at least `2/3`, and on no-instances it is `[false]` with +probability at least `2/3`. No probability gap or answer is required outside the promise. + +This is the library's time-indexed native-machine convention, extending `BPTIME` to partial +promises. It does not define the class through bounded-error total completions. A strict-majority +completion belongs to `PPTIME` at the same caller-supplied clock, with ties rejecting; this is not +a bounded-error completion in `BPTIME`. + +## Main definitions + +* `Turing.MultiTapePTM.SolvesPromiseWithBoundedErrorInTime`: native clock and error contract. +* `Cslib.Complexity.PromiseBPTIME`: bounded-error promise computation in affine time. + +## Main results + +* `PromiseBPTIME_mono`: increasing the time bound preserves membership. +* `promiseClass_BPTIME_subset_PromiseBPTIME`: total bounded-error completions give witnesses. +* `PromiseBPTIME_subset_promiseClass_PPTIME`: a strict-majority completion at the same time scale. +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib.Complexity + +variable {α : Type} {k : ℕ} {State : Type} + +/-- Every run halts by `t`; bounded error is required only on the two sides of the promise. -/ +@[expose] def SolvesPromiseWithBoundedErrorInTime (machine : MultiTapePTM k Bool State) + (enc : α ↪ List Bool) (Q : PromiseProblem α) (t : α → ℕ) : Prop := + ∀ a, (∀ final ∈ (Cslib.ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ Q.yes → 2 / 3 ≤ Cslib.ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) ∧ + (a ∈ Q.no → 2 / 3 ≤ Cslib.ProbComp.eval (machine.runClosed (t a) (enc a)) [false]) + +/-- A sufficiently long clock may be enlarged without changing the output law. -/ +theorem SolvesPromiseWithBoundedErrorInTime.mono + {machine : MultiTapePTM k Bool State} {enc : α ↪ List Bool} {Q : PromiseProblem α} + {t t' : α → ℕ} (h : machine.SolvesPromiseWithBoundedErrorInTime enc Q t) + (ht : ∀ a, t a ≤ t' a) : machine.SolvesPromiseWithBoundedErrorInTime enc Q t' := by + intro a + obtain ⟨hhalt, hyes, hno⟩ := h a + refine ⟨?_, ?_⟩ + · rw [machine.eval_runClosedConfigFrom_eq_of_halted _ (ht a) hhalt] + exact hhalt + · rw [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] + exact ⟨hyes, hno⟩ + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM +open scoped ENNReal + +variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} + +/-- Native bounded-error promise problems with fixed machine parameters and affine time `T`. +All encoded inputs terminate, but the error conditions only constrain promised inputs. -/ +@[expose] def PromiseBPTIME (enc : α ↪ List Bool) (T : ℕ → ℕ) : Set (PromiseProblem α) := + {Q | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) + (machine : MultiTapePTM k Bool State), + machine.SolvesPromiseWithBoundedErrorInTime enc Q fun a => c₁ * T (enc a).length + c₂} + +/-- Membership is monotone in the caller's time bound. -/ +theorem PromiseBPTIME_mono {T₁ T₂ : ℕ → ℕ} (h : ∀ n, T₁ n ≤ T₂ n) : + PromiseBPTIME enc T₁ ⊆ PromiseBPTIME enc T₂ := by + rintro Q ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩ + exact ⟨c₁, c₂, k, State, hfinite, machine, hQ.mono fun a => + Nat.add_le_add_right (Nat.mul_le_mul_left _ (h _)) _⟩ + +/-- A bounded-error total completion supplies a native bounded-error promise solver. -/ +theorem promiseClass_BPTIME_subset_PromiseBPTIME : + promiseClass (BPTIME enc T) ⊆ PromiseBPTIME enc T := by + rintro Q ⟨L, ⟨c₁, c₂, k, State, hfinite, machine, hL⟩, hyes, hno⟩ + refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hL a).1, ?_, ?_⟩⟩ + · intro ha + simpa only [indicator, hyes ha, ↓reduceIte] using (hL a).2 + · intro ha + have hnot : a ∉ L := fun h => Set.disjoint_right.mp hno ha h + simpa only [indicator, hnot, ↓reduceIte] using (hL a).2 + +/-- Accepting by strict majority completes the promise in `PPTIME` without changing its clock. +The completion may have an exact tie outside the promise; it need not belong to `BPTIME`. -/ +theorem PromiseBPTIME_subset_promiseClass_PPTIME : + PromiseBPTIME enc T ⊆ promiseClass (PPTIME enc T) := by + rintro Q ⟨c₁, c₂, k, State, hfinite, machine, hQ⟩ + let L : Set α := {a | 1 / 2 < + ProbComp.eval (machine.runClosed (c₁ * T (enc a).length + c₂) (enc a)) [true]} + have hhalf : (1 / 2 : ℝ≥0∞) < 2 / 3 := by + refine (ENNReal.toReal_lt_toReal (ENNReal.div_ne_top (by norm_num) (by norm_num)) + (ENNReal.div_ne_top (by norm_num) (by norm_num))).mp ?_ + simp only [ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_ofNat] + norm_num + refine ⟨L, ⟨c₁, c₂, k, State, hfinite, machine, + fun a => ⟨(hQ a).1, Iff.rfl⟩⟩, ?_, ?_⟩ + · intro a ha + exact hhalf.trans_le ((hQ a).2.1 ha) + · refine Set.disjoint_right.mpr fun a ha hL => ?_ + let p := ProbComp.eval (machine.runClosed (c₁ * T (enc a).length + c₂) (enc a)) + have hsum : p [true] + p [false] ≤ 1 := by + simpa only [Finset.sum_pair (by decide : ([true] : List Bool) ≠ [false]), PMF.tsum_coe] using + (sum_le_tsum ({[true], [false]} : Finset (List Bool)) (f := fun w => p w)) + have hfalse : (1 / 2 : ℝ≥0∞) ≤ p [false] := hhalf.le.trans ((hQ a).2.2 ha) + have hlt := ENNReal.add_lt_add_right (by norm_num : (1 / 2 : ℝ≥0∞) ≠ ⊤) hL + rw [ENNReal.add_halves] at hlt + exact (hlt.trans_le ((add_le_add le_rfl hfalse).trans hsum)).false + +end Cslib.Complexity diff --git a/ComplexityTests/PromiseCountingSimulation.lean b/ComplexityTests/PromiseCountingSimulation.lean index f6855d1a0c..1e68a6ab22 100644 --- a/ComplexityTests/PromiseCountingSimulation.lean +++ b/ComplexityTests/PromiseCountingSimulation.lean @@ -7,33 +7,105 @@ Authors: Christian Reitwiessner import Complexity.Computability.Complexity.Classes.CountingSimulation.Promise import ComplexityTests.PromisePP -/-! The conditional counting simulation on a genuinely partial promise. +/-! A fixed-clock native counting simulation on a genuinely partial promise. -The completion contains `[true]` and excludes `[false]`; its one machine retains both resource -bounds. The verifier's exact tie on the empty word is checked in `ComplexityTests.PromisePP`. +The native machine answers the promised singleton words without error and uses a fair coin on the +empty word. The deterministic completion retains the caller's explicit quadratic clock. -/ namespace ComplexityTests.PromiseCountingSimulation -open Cslib.Complexity Cslib.Complexity.CountingSimulation Turing.MultiTapeTM - Cslib.Circuits.Frontier.ExplicitTensorNetwork ComplexityTests.PromiseProbabilistic - ComplexityTests.PromisePP - -/-- A concrete partial promise gets a total deterministic completion with the joint bounds. -The contraction algorithm is the only unproved interface assumed by this client. -/ -example (A : ContractionAlgorithm (encPair encNat encExplicitNetwork) (fun G => G.2.contraction) - ExplicitAdmissible) : - ∃ (L : Set (List Bool)) (k C d : ℕ), [true] ∈ L ∧ [false] ∉ L ∧ - DecidableInTimeAndSpace L encBits - (fun a => 2 ^ (C * ((a.length + 1) ^ (k + 2) + 1) / - Nat.sqrt (Nat.log 2 ((a.length + 1) ^ (k + 2) + 1)))) - (fun a => ((a.length + 1) ^ (k + 2) + 1) ^ d) := by - have hQ : partialSingletonBit ∈ PromiseBPP encBits := - ⟨1, partialVerifier, partialVerifier_polyTime, - solvesWithBoundedError_partialSingletonBit⟩ - obtain ⟨L, k, C, d, hyes, hno, h⟩ := - exists_completion_of_mem_PromiseBPP_of_contractionAlgorithm A hQ - refine ⟨L, k, C, d, hyes rfl, ?_, h⟩ +open Cslib Cslib.Complexity Cslib.Complexity.CountingSimulation Turing Turing.MultiTapeTM + ComplexityTests.PromiseProbabilistic + +/-- Read the first input symbol, or a fair coin when there is no symbol, and halt. -/ +private def partialMachine : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ coin := .step + { inputTape := 0, workTapes := Fin.elim0, output := some (symbol.getD coin), state := none } + Empty.elim Empty.elim + +private theorem partialMachine_halts (input : List Bool) : + ∀ final ∈ (ProbComp.eval + (partialMachine.runClosedConfigFrom 1 (partialMachine.initialConfig input))).support, + final.tapes.state = none := by + intro final hfinal + rw [MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins, PMF.mem_support_map_iff] at hfinal + obtain ⟨coins, hcoins, rfl⟩ := hfinal + obtain ⟨coin, rfl⟩ := List.length_eq_one_iff.mp + (BitString.mem_support_uniformList_iff.mp hcoins) + cases input <;> cases coin <;> rfl + +private theorem partialMachine_singleton (b : Bool) : + ProbComp.eval (partialMachine.runClosed 1 [b]) [b] = 1 := by + rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + have hcard : (Finset.univ.filter fun r : Fin 1 → Bool => + partialMachine.runClosedCoins (List.ofFn r) [b] = [b]).card = 2 := by + cases b <;> decide + rw [hcard] + norm_num [ENNReal.div_self] + +/-- Unlike a padded polynomial chosen by the simulation, this clock is fixed by the client. -/ +private def clock (n : ℕ) : ℕ := (n + 1) ^ 2 + 1 + +private theorem clock_pos (n : ℕ) : 1 ≤ clock n := by + unfold clock + omega + +private theorem partialMachine_halts_clock (input : List Bool) : + ∀ final ∈ (ProbComp.eval + (partialMachine.runClosedConfigFrom (clock input.length) + (partialMachine.initialConfig input))).support, final.tapes.state = none := by + rw [MultiTapePTM.eval_runClosedConfigFrom_eq_of_halted partialMachine _ + (clock_pos input.length) (partialMachine_halts input)] + exact partialMachine_halts input + +/-- Both sides of the promise have native witnesses with this same explicit clock. -/ +private theorem partialSingletonBit_mem_PromiseBPTIME : + partialSingletonBit ∈ PromiseBPTIME encBits clock := by + refine ⟨1, 0, 0, Unit, inferInstance, partialMachine, fun input => ?_⟩ + simp only [Nat.one_mul, Nat.add_zero] + refine ⟨partialMachine_halts_clock input, ?_, ?_⟩ + · intro hyes + obtain rfl : input = [true] := hyes + simp only [encBits_apply] + rw [MultiTapePTM.eval_runClosed_eq_of_halted partialMachine _ + (clock_pos _) (partialMachine_halts _), partialMachine_singleton] + exact ENNReal.div_le_of_le_mul (by norm_num) + · intro hno + obtain rfl : input = [false] := hno + simp only [encBits_apply] + rw [MultiTapePTM.eval_runClosed_eq_of_halted partialMachine _ + (clock_pos _) (partialMachine_halts _), partialMachine_singleton] + exact ENNReal.div_le_of_le_mul (by norm_num) + +/-- The native machine's unpromised empty input is an exact tie at the declared clock. -/ +example : ([] : List Bool) ∉ partialSingletonBit.promise ∧ + ProbComp.eval (partialMachine.runClosed (clock 0) []) [true] = 1 / 2 := by + constructor + · simp [partialSingletonBit, PromiseProblem.promise] + · rw [MultiTapePTM.eval_runClosed_eq_of_halted partialMachine _ + (clock_pos _) (partialMachine_halts _), + MultiTapePTM.eval_runClosed_apply_eq_acceptCount, + show partialMachine.acceptCount [] 1 = 1 by decide] + norm_num + +/-- A concrete partial promise gets one total deterministic machine at the client's fixed clock, +with both resource bounds and no assumed contraction algorithm. -/ +example : ∃ (L : Set (List Bool)) (C d : ℕ), [true] ∈ L ∧ [false] ∉ L ∧ + DecidableInTimeAndSpace L encBits + (fun a => 2 ^ (C * ((a.length + 1) ^ 2 + 1) / + Nat.sqrt (Nat.log 2 ((a.length + 1) ^ 2 + 1)))) + (fun a => ((a.length + 1) ^ 2 + 1) ^ d) := by + have hT : TimeConstructible clock := timeConstructible_succ_sq.succ + have hbound (n : ℕ) : max n 2 ≤ clock n := by + have h := Nat.le_self_pow (by omega : 2 ≠ 0) (n + 1) + have hpos : 1 ≤ (n + 1) ^ 2 := Nat.one_le_pow _ _ (by omega) + unfold clock + omega + obtain ⟨L, C, d, hyes, hno, h⟩ := + exists_completion_of_mem_PromiseBPTIME hT hbound partialSingletonBit_mem_PromiseBPTIME + refine ⟨L, C, d, hyes rfl, ?_, h⟩ exact Set.disjoint_right.mp hno rfl end ComplexityTests.PromiseCountingSimulation