claimroutineinferred_dep

Truncated digits give accurate dyadic values

Truncated digits give dyadic

v_\sigma

within

3\Delta/8

on over 3/4 of environments

turns the reward stream into a short accurate dyadic value

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

Statement (paper)

For each master environment, with

K=r+6

, the dyadic number

v_\sigma=a_\sigma2^{-K}

obtained from the digits

w_j\in\{-6,\ldots,6\}

\bar W_L(z)

is computed using

O(K)

bits, and on more than three quarters of the environments conditioned on

X_f(z)=1

it satisfies

|v_\sigma-p_{\mathcal M}(x)|<3\Delta/8

In plain English

For each master environment, the dyadic value

v_\sigma=a_\sigma2^{-K}

with

K=r+6

, built from the digits

w_j\in\{-6,\ldots,6\}

\bar W_L(z)

, is computed with

O(K)

bits. On more than three quarters of the environments conditioned on

X_f(z)=1

, it lies within

3\Delta/8

p_{\mathcal M}(x)

Why it's here

This turns the digit stream of the averaged stage-L reward into a short dyadic number that is close to the acceptance probability on most environments. It combines the one-sided

\Delta/8

bound on

W_L(z)

, the statistical concentration of

\bar W_L(z)

from the preceding claim, and the arithmetic interface's exact digits to control truncation error. The binary-search median step then uses this accuracy for the retained encodings.

Classified routine:

Direct bookkeeping combining the earlier claims (one-sided Δ/8 bound on W_L(z), the concentration of the averaged reward) with the exact digit stream of the arithmetic interface, plus a standard truncation-error estimate for signed-digit expansions.

Uses

thmUniform numerical interface for arithmetic recipesclaimStage-L reward approximates acceptance probabilityclaimPrecision choice beats coordinate factor N

Used by

claimBinary-search median is accurate

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Truncated digits give dyadic accurate values" rests on claim-thm-fixed-precision-1
info
inferred_dep
outline: "Truncated digits give dyadic accurate values" rests on claim-thm-fixed-precision-2