claimroutineinferred_dep

Binary-search median is accurate

Binary-search upper median satisfies

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

produces the final deterministic approximation

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

Statement (paper)

Let

E\ge1

be the number of retained encodings and

h=\lfloor E/2\rfloor+1

. The binary search over

[0,2^K]

outputs the least integer

a

such that at least

h

retained encodings satisfy

a_\sigma\le a

, which is the upper median of the multiset

\{a_\sigma\}

counted with repetitions. Since more than three quarters of its members satisfy Equation , so does the median, and hence

z_x=a2^{-K}

satisfies

|z_x-p_{\mathcal M}(x)|<3\Delta/8\le(n+2)^{-d}

In plain English

With

E\ge1

retained encodings and

h=\lfloor E/2\rfloor+1

, the binary search over

[0,2^K]

returns the upper median

a

of the values

a_\sigma

, and

z_x=a2^{-K}

satisfies

|z_x-p_{\mathcal M}(x)|<3\Delta/8\le(n+2)^{-d}

Why it's here

Since more than three quarters of the retained encodings give an accurate dyadic value, the median must also be accurate, so a deterministic median computation over the enumerated list gives the required approximation. It combines the exact enumeration of retained encodings with the accuracy of the individual truncated values to finish the proof of the parent theorem.

Classified routine:

Standard median-amplification argument: if more than half (here three quarters) of the values lie in an interval, the median does too, and a logspace binary search over counts finds it. It follows directly from the accuracy claim (claim-thm-fixed-precision-3) and the enumerability claim (claim-thm-fixed-precision-4).

Uses

claimTruncated digits give accurate dyadic valuesclaimConditional environment law is enumerable

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Binary-search median is accurate" rests on claim-thm-fixed-precision-3
info
inferred_dep
outline: "Binary-search median is accurate" rests on claim-thm-fixed-precision-4