theoremroutine

Fixed-precision estimators meet error bound

Actual estimators have error Cb2−pC_b2^{-p} and reward moment ≤ Cbs2−spC_b^s2^{-sp}
fixed-precision estimator guarantee used by the main theorem
Theorem·thm:fp-estimators·§9.5 Closing the coupled induction

Statement (paper)

For every allowed task, with precision pp defined in Equation , the actual row outputs, including the pre-incoming scores and support witnesses, satisfy du,a(Hˉ,H)≤Cb2−p. \mathfrak d_{u,a}(\bar H,H)\le C_b2^{-p}. The clipped vectors have the corresponding ordinary error bound. In particular, every allowed reward query satisfies 1NEσ∑x∈VlXu(x)u∣Wˉl(x)−Wl(x)∣s≤Cbs2−sp. \frac1N\mathbb E_\sigma\sum_{x\in V_l}\frac{X_u(x)}u |\bar W_l(x)-W_l(x)|^s\le C_b^s2^{-sp}. These estimates are uniform over the allowed task parameters and stage, and the constants are independent of the input and of BB.

In plain English

For every allowed task at precision pp, the actual row outputs (with pre-incoming scores and support witnesses) have discrepancy du,a(Hˉ,H)≤Cb2−p\mathfrak d_{u,a}(\bar H,H)\le C_b2^{-p}, and the clipped vectors satisfy the corresponding ordinary error bound. Consequently every allowed reward query obeys 1NEσ∑x∈VlXu(x)u∣Wˉl(x)−Wl(x)∣s≤Cbs2−sp\frac1N\mathbb E_\sigma\sum_{x\in V_l}\frac{X_u(x)}u|\bar W_l(x)-W_l(x)|^s\le C_b^s2^{-sp}, uniformly over allowed task parameters and stage, with constants independent of the input and of BB.

Why it's here

This closes the coupled induction of Section 9: the error-reserve result (prop-est-clean) shows compression, clamping and assembly use only half the budget Cb2−pC_b2^{-p}, and the uniform block coupling (prop-fp-coupling) controls the remaining block-level error, so the bound reproduces itself at each stage. The reward-moment bound is the form later used for fixed inverse-polynomial accuracy in the fixed-precision theorem.
Classified routine:
Direct combination of the error-reserve proposition (prop-est-clean) and the uniform block coupling (prop-fp-coupling) to close the paper's own coupled induction. The reward-moment bound then follows by bookkeeping.

Uses

propActual runs stay close to clean runspropError reserve after compression and clamping

Used by

thmDeterministic logspace approximation of acceptance probabilityclaimPrecision choice beats coordinate factor N

Sources

PaperOpen
Section
§9.5 Closing the coupled induction
Page
—
Label
thm:fp-estimators
Line
sections/fingerprints.tex:725
Leannot aligned

Phase 2 aligns this node to a Lean declaration.