corollaryroutine

Deterministic search for accepting computations

So an accepting computation is found deterministically when pM(x)≥(n+2)−cp_{\mathcal M}(x)\ge(n+2)^{-c}
search version of the main theorem
Corollary·cor:certified-search·§12.5 Certified accepting computations

Statement (paper)

Fix a randomized logarithmic-space machine M\mathcal M that halts within a fixed polynomial bound T(n)≥1T(n)\ge1 on every input and every coin sequence, and fix an integer c≥0c\ge0. There is a uniform deterministic logarithmic-space, polynomial-time transducer that outputs an accepting computation of M\mathcal M whenever pM(x)≥(n+2)−c. p_{\mathcal M}(x)\ge(n+2)^{-c}. On every other input it outputs either an accepting computation or a failure symbol. If every accepting run of M\mathcal M emits a valid witness for a specified relation, the transducer can instead output such a witness with the same guarantee.

In plain English

For a randomized log-space machine M\mathcal M with polynomial running time and a fixed cc, a deterministic log-space, polynomial-time transducer outputs an accepting computation whenever the acceptance probability pM(x)p_{\mathcal M}(x) is at least (n+2)−c(n+2)^{-c}. On other inputs it outputs an accepting computation or a failure symbol, and the same holds for outputting a valid witness when accepting runs emit witnesses.

Why it's here

This turns the fixed inverse-polynomial accuracy of the preceding theorem from a decision procedure into a search procedure. It deterministically finds a concrete accepting run or witness, not just a yes/no answer, whenever acceptance is not too unlikely.
Classified routine:
A direct consequence of the paper's fixed-precision approximation theorem (thm-fixed-precision). It applies the standard search-to-decision technique of fixing coin bits one at a time, keeping each extension whose estimated conditional acceptance probability stays above a threshold, as in the method of conditional probabilities.

Uses

thmDeterministic logspace approximation of acceptance probability

Used by

Nothing in the paper

Sources

PaperOpen
Section
§12.5 Certified accepting computations
Page
—
Label
cor:certified-search
Line
sections/conclusion.tex:396
Leannot aligned

Phase 2 aligns this node to a Lean declaration.