claimroutine

Precision choice beats coordinate factor N

Precision

p=O(B)

makes

\Pr[|\bar W_L-W_L|>\Delta/8]\le1/8

at the start

absorbs the conditioning factor

N

into the precision

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

Statement (paper)

With

a=u=f=b_L

and the fixed linear coefficient of

M_{\rm top}=O(B)

chosen large enough that

p\ge r+3+\frac{C_NB+\lceil\log_2 C_{\rm tail}\rceil+3}{8}

, one has

\Pr\bigl[|\bar W_L(z)-W_L(z)|>\Delta/8\mid X_f(z)=1\bigr]\le 1/8

; in particular the bound in Equation is at most

C_{\rm tail}\,2^{C_NB-8p+8r+24}\le 2^{-3}

In plain English

With the linear coefficient of

M_{\rm top}=O(B)

large enough that

p\ge r+3+\frac{C_NB+\lceil\log_2 C_{\rm tail}\rceil+3}{8}

, the conditional probability that

|\bar W_L(z)-W_L(z)|>\Delta/8

given

X_f(z)=1

is at most

1/8

. The tail bound is at most

C_{\rm tail}\,2^{C_NB-8p+8r+24}\le 2^{-3}

Why it's here

This applies the conditional eighth-moment bound at the specified start

z

with the error bound from the fixed-precision estimators. The conditioning cost, a factor

N

that is exponential in

B

, is absorbed by choosing the precision

p

larger by an amount linear in

B

. That makes the failure probability at

z

at most

1/8

, which the next claim uses to read off accurate dyadic digits of

\bar W_L(z)

Classified routine:

Direct parameter bookkeeping: combines the conditional eighth-moment bound (lem-final-majority) with the estimator error bound (thm-fp-estimators) via Markov's inequality, absorbing the exponential-in-B conditioning factor by choosing the precision larger by an amount linear in B.

Uses

lemRank channel retention estimatesthmFixed-precision estimators meet error boundlemConditional moment bound at a specified start

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:166

Leannot aligned

Phase 2 aligns this node to a Lean declaration.