claimroutineinferred_dep

Fixed deterministic library decides interpreter promise

Fixed deterministic machine

A

decides the interpreter's 2/3 vs 1/3 promise

derandomizes the fixed interpreter once for all

Claim·§13.2 Fixing one deterministic library·inside thmEffective compiler from randomized to deterministic logspace

Statement (paper)

There is one fixed ordinary finite-tape deterministic decision machine

A

, with one input head confined to the endmarked input and initially at its left endmarker, such that on every input of length

m

it halts, it accepts whenever

\Pr[U\text{ accepts}]\ge 2/3

and rejects whenever

\Pr[U\text{ accepts}]\le 1/3

, and every work head stays in

[-(\lambda_m+1),\lambda_m+1]

relative to its origin.

In plain English

There is one fixed deterministic machine

A

with a single input head on the endmarked input that always halts on inputs of length

m

. It accepts when the interpreter

U

accepts with probability at least

2/3

, rejects when that probability is at most

1/3

, and keeps every work head within

[-(\lambda_m+1),\lambda_m+1]

of its origin.

Why it's here

This claim derandomizes the fixed interpreter

U

of the compiler-interpreter lemma once and for all. It applies the fixed-precision approximation theorem to

U

and thresholds the estimate to separate the

\ge 2/3

and

\le 1/3

cases, which is the promise-BPL step. The later claims use

A

as the single deterministic library and simulate it on padded inputs within the stated work-head bound.

Classified routine:

A direct consequence of the paper's earlier fixed-precision approximation theorem (equivalently its PromiseBPL = PromiseL corollary) applied to the fixed interpreter U, with thresholding of the estimate and bookkeeping on the work-head bound.

Uses

thmDeterministic logspace approximation of acceptance probabilitylemFixed interpreter with enforced resource boundscorPromise BPL equals promise L

Used by

claimCallback compiles virtual padded input readsclaimSimultaneous work-space bound on all tapes

Sources

PaperOpen

Section: §13.2 Fixing one deterministic library
Page: —
Label: —
Line: sections/compiler.tex:193

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Fixed deterministic library separating interpreter thresholds" rests on thm:fixed-precision
info
inferred_dep
outline: "Fixed deterministic library separating interpreter thresholds" rests on lem:compiler-interpreter
info
inferred_dep
outline: "Fixed deterministic library separating interpreter thresholds" rests on cor:promise-bpl