claimroutine

Stage-L reward approximates acceptance probability

Stage-

L

reward satisfies

0\le p_{\mathcal M}(x)-W_L(z)\le\Delta/8

with

L=O(B)

fixes stage and precision for one-sided approximation

Claim·§12.2 A dyadic approximation at the specified start·inside thmDeterministic logspace approximation of acceptance probability

Statement (paper)

With

r=d\lceil\log_2(n+2)\rceil

\Delta=2^{-r}

L=\left\lceil\frac{C_0B+r+3}{H-1}\right\rceil

, and

z

the all-primary copy of the start at stage

L

, one has

r,L=O(B)

and

0\le p_{\mathcal M}(x)-W_L(z)\le\Delta/8

, for every acceptance probability

p_{\mathcal M}(x)

(with no promise). Moreover, there is a fixed

C_N

such that all the resulting stage domains are bounded by

N=2^{C_NB}

In plain English

With

r=d\lceil\log_2(n+2)\rceil

\Delta=2^{-r}

and

L=\lceil (C_0B+r+3)/(H-1)\rceil

, the reward

W_L(z)

at the all-primary start copy

z

satisfies

0\le p_{\mathcal M}(x)-W_L(z)\le\Delta/8

for every input, with no promise on

p_{\mathcal M}(x)

. Also

r,L=O(B)

, and all stage domains are bounded by

N=2^{C_NB}

for a fixed

C_N

Why it's here

This fixes the stage

L

and precision

\Delta

so that the hierarchy reward is a one-sided approximation to the acceptance probability within

\Delta/8

. It does so by applying the geometric error bound

|V_0|2^{-(H-1)l}

from the hierarchy-reward proposition to the reduced system of the model-reduction lemma, with

L

chosen large enough to make that error at most

\Delta/8

. The sizes

r,L=O(B)

and

N=2^{C_NB}

keep all later digit and address computations within

O(B)

bits, which the truncation step relies on.

Classified routine:

Direct parameter bookkeeping: it plugs the stage choice L into the geometric error bound |V_0|2^{-(H-1)l} of the hierarchy-reward proposition, applied to the reduced system from the model-reduction lemma, and checks that the sizes are O(B).

Uses

lemRandomized logspace machines as substochastic systemspropHierarchy reward approximates base acceptance probability

Used by

claimTruncated digits give accurate dyadic values

Sources

PaperOpen

Section: §12.2 A dyadic approximation at the specified start
Page: —
Label: —
Line: sections/conclusion.tex:149

Leannot aligned

Phase 2 aligns this node to a Lean declaration.