claimroutineinferred_dep

Coupling recurrence from child charges

Child charges sum to 2−pλM∑d2−(D2−C)d2^{-p}\lambda_M\sum_d 2^{-(D_2-C)d}
turns escape, bucket and assembly bounds into the recurrence
Claim·§9.5 Closing the coupled induction·inside propActual runs stay close to clean runs

Statement (paper)

For a task of budget M∈IbM\in\mathcal I_b and precision pp, after absorbing the fixed assembly factors into one fixed exponent CC, all coupled child charges are at most 2−pλM∑d=12h∗2−(D2−C)d2^{-p}\lambda_M\sum_{d=1}^{2h_*}2^{-(D_2-C)d}, since a child of budget m∈Ibm\in\mathcal I_b used at group slack dd satisfies λm=λM2−D2(M−m)≤λM2−D2d\lambda_m=\lambda_M2^{-D_2(M-m)}\le\lambda_M2^{-D_2d}, groups with larger slack have identical children and contribute zero, and separate post-assembly queries with constant positive budget drop use d=1d=1. Together with Equation , this gives the complete coupling recurrence.

In plain English

For a task of budget M∈IbM\in\mathcal I_b and precision pp, all coupled child discrepancy charges sum to at most 2−pλM∑d=12h∗2−(D2−C)d2^{-p}\lambda_M\sum_{d=1}^{2h_*}2^{-(D_2-C)d} for one fixed exponent CC. Combined with the direct collision charge bound, this gives the full coupling recurrence.

Why it's here

Each child of budget mm used at group slack dd has λm≤λM2−D2d\lambda_m\le\lambda_M2^{-D_2d}, so the 2Cd2^{Cd} amplification from the escape, bucket and assembly steps is beaten by choosing D2D_2 large. Groups of larger slack have identical actual and clean children and contribute nothing, and post-assembly queries are treated as slack d=1d=1. This leaves a geometric sum plus the direct collision term, which the next claim closes by choosing D2D_2, D1D_1 and ϵ\epsilon.
Classified routine:
Bookkeeping step that combines the escape, bucket and assembly lemmas (lem-fp-escape, lem-fp-buckets, lem-atom-assembly) with the definition λ_m = λ_M 2^{-D_2(M-m)}. It reduces the child charges to a geometric sum and adds the direct collision charge from lem-fp-direct.

Uses

lemEscape contribution charged to child discrepancieslemDirect collision charge boundlemAssembly of row and cutoff discrepancieslemBucket discrepancy bound with collision charge

Used by

claimConstants chosen to close coupling recurrence

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Coupling recurrence from escape, collision, assembly" rests on lem:fp-buckets