propositionroutine

Actual runs stay close to clean runs

Actual outputs stay within 2−pλM2^{-p}\lambda_M of clean outputs, λM=2−D1h∗+D2(M−Mb)\lambda_M=2^{-D_1h_*+D_2(M-M_b)}
closes the coupled induction for the estimators
Proposition·prop:fp-coupling·§9.5 Closing the coupled induction

Statement (paper)

The fixed constants can be chosen so that, for every task of budget M∈IbM\in\mathcal I_b and precision pp, each prescribed actual--clean output discrepancy, including every pre-incoming score and witness, is at most 2−pλM,λM=2−D1h∗+D2(M−Mb). 2^{-p}\lambda_M,\qquad \lambda_M=2^{-D_1h_*+D_2(M-M_b)}. The same assertion holds for the ordinary vector metrics. Adding these discrepancies to the clean estimates proves the target error bounds for the actual tables and vectors.

In plain English

With suitably chosen fixed constants, in every task of budget M∈IbM\in\mathcal I_b and precision pp, each actual-versus-clean output discrepancy (including pre-incoming scores and witnesses) is at most 2−pλM2^{-p}\lambda_M, where λM=2−D1h∗+D2(M−Mb)\lambda_M=2^{-D_1h_*+D_2(M-M_b)}. The same holds for the ordinary vector metrics, and adding these discrepancies to the clean estimates gives the target error bounds for the actual tables and vectors.

Why it's here

This closes the coupled induction: it bounds how far the salted actual computation can drift from the salt-free clean one, using the escape-charging and direct collision-cost lemmas together with assembly of child discrepancies. The recurrence is closed by choosing the constants D2D_2, D1D_1 and ϵ\epsilon in a consistent order. Combined with the clean error-reserve bound, it yields the error bounds for the actual estimators in the next theorem.
Classified routine:
Closes the coupled induction by combining the escape-charging, direct collision-charge and assembly lemmas into a recurrence, then choosing the constants D_2, D_1, epsilon in order. This is standard bookkeeping that follows from the earlier nodes.

Uses

lemClean calculation is independent of the saltpropError reserve after compression and clampinglemEscape contribution charged to child discrepancieslemDirect collision charge boundlemAssembly of row and cutoff discrepancieslemPairwise-collision hash from few random bits

Used by

thmFixed-precision estimators meet error bound

Inside the proof

claimClean active tasks meet target boundsclaimCoupling recurrence from child chargesclaimConstants chosen to close coupling recurrenceclaimCoupling plus clean bound gives targetclaimOrder of constant choices is consistent

Sources

PaperOpen
Section
§9.5 Closing the coupled induction
Page
—
Label
prop:fp-coupling
Line
sections/fingerprints.tex:614
Leannot aligned

Phase 2 aligns this node to a Lean declaration.