claimroutineinferred_dep

Coupling plus clean bound gives target

Coupling bound plus clean bound gives total error at most Cb2−pC_b2^{-p}
final triangle-inequality step of the coupling proof
Claim·§9.5 Closing the coupled induction·inside propActual runs stay close to clean runs

Statement (paper)

Since 0≤M−Mb<h∗0\le M-M_b<h_*, one has λM≤2−(D1−D2)h∗\lambda_M\le 2^{-(D_1-D_2)h_*}, which is uniformly as small as required after the same minimum-size padding. Hence, by the triangle inequality, adding the coupling bound to the spare clean active bound, for example Cb2−p/2C_b2^{-p}/2, gives an error at most Cb2−pC_b2^{-p}; the inactive target bounds are the previously fixed bounded-range bounds.

In plain English

Because 0≤M−Mb<h∗0\le M-M_b<h_*, the coupling factor satisfies λM≤2−(D1−D2)h∗\lambda_M\le 2^{-(D_1-D_2)h_*}, which is as small as needed after minimum-size padding. Adding this coupling bound to the spare clean active bound (e.g. Cb2−p/2C_b2^{-p}/2) gives total error at most Cb2−pC_b2^{-p}, while inactive target bounds are the previously fixed bounded-range ones.

Why it's here

This closes the coupled induction: the clean active bounds from the earlier claim and the recurrence-closing choice of D2,D1,ϵD_2,D_1,\epsilon give a tiny coupling discrepancy, and a triangle inequality turns clean estimate plus discrepancy into the target error bound for the actual tables and vectors. It is the final step of the proposition, converting actual-versus-clean closeness into the stated error guarantee.
Classified routine:
A direct consequence of the earlier claims (clean active bounds and the constant choices closing the coupling recurrence), finished with a triangle inequality and the observation that the coupling factor is small. It is bookkeeping, not a new idea.

Uses

claimClean active tasks meet target boundsclaimConstants chosen to close coupling recurrence

Used by

Nothing in the paper

Sources

PaperOpen
Section
§9.5 Closing the coupled induction
Page
—
Label
—
Line
sections/fingerprints.tex:693
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Coupling plus clean bound gives target" rests on claim-prop-fp-coupling-1
  • info
    inferred_dep
    outline: "Coupling plus clean bound gives target" rests on claim-prop-fp-coupling-3