corollaryroutineinferred_dep

Promise BPL equals promise L

So promise BPL equals promise L

promise-class form used by the effective simulation

Corollary·cor:promise-bpl·§12.3 The class equality and promise separation

Statement (paper)

Under these conventions,

\mathsf{PromiseBPL}=\mathsf{PromiseL}

In plain English

Under the paper's stated conventions, the promise version of bounded-error randomized logspace equals the promise version of deterministic logspace:

\mathsf{PromiseBPL}=\mathsf{PromiseL}

Why it's here

This lifts the fixed inverse-polynomial-accuracy derandomization theorem from a statement about particular algorithms to a statement about the promise classes. Any promise problem solved by a bounded-error randomized logspace machine is thus solved deterministically in logspace, and later results on effective simulation and separation rely on this equality.

Classified routine:

Direct consequence of the paper's fixed-precision deterministic logspace approximation theorem (thm-fixed-precision): approximate the acceptance probability to within 1/6 and threshold at 1/2, the standard reduction from probability estimation to promise-class equality.

Uses

thmDeterministic logspace approximation of acceptance probability

Used by

claimFixed deterministic library decides interpreter promise

Sources

PaperOpen

Section: §12.3 The class equality and promise separation
Page: —
Label: cor:promise-bpl
Line: sections/conclusion.tex:309

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The proof of cor:promise-bpl (conclusion.tex 315-318) reads "The same $d=3$ approximation and threshold $1/2$ used in the preceding proof". That is an application of Theorem fixed-precision, but the corollary has no uses.