claimroutineinferred_dep

Constants chosen to close coupling recurrence

Choosing D2D_2, then D1D_1, then ϵ\epsilon closes the coupling recurrence
makes the recurrence hold with total at most 2−pλM2^{-p}\lambda_M
Claim·§9.5 Closing the coupled induction·inside propActual runs stay close to clean runs

Statement (paper)

Choose D2>CD_2>C so large that ∑d≥12−(D2−C)d≤1/4\sum_{d\ge1}2^{-(D_2-C)d}\le 1/4, then choose D1>D2+1D_1>D_2+1, and finally choose rational ϵ>0\epsilon>0 so small that 12sϵ>C+D1+2\frac1{2s\epsilon}>C+D_1+2. Then, since h∗≤ϵlog⁡2Bh_*\le\epsilon\log_2B, the direct relative charge satisfies 2Ch∗B−1/(2s)≤14λM2^{Ch_*}B^{-1/(2s)}\le\frac14\lambda_M (after increasing the fixed minimum BB to absorb any fixed coefficient), so the child and direct charges together fit within the bound 2−pλM2^{-p}\lambda_M of Equation .

In plain English

Fixing D2D_2 large (so ∑d≥12−(D2−C)d≤1/4\sum_{d\ge1}2^{-(D_2-C)d}\le 1/4), then D1>D2+1D_1>D_2+1, then a small rational ϵ>0\epsilon>0 with 12sϵ>C+D1+2\frac1{2s\epsilon}>C+D_1+2, makes the direct charge 2Ch∗B−1/(2s)2^{Ch_*}B^{-1/(2s)} at most 14λM\frac14\lambda_M for large enough BB. Together with the child charges, this keeps the total within 2−pλM2^{-p}\lambda_M.

Why it's here

This finishes the induction behind the coupling proposition by showing the recurrence from the previous claim closes. D2D_2 makes the child contributions sum to at most a fraction of the bound, and D1D_1 and ϵ\epsilon (via h∗≤ϵlog⁡2Bh_*\le\epsilon\log_2B) make the direct polynomially small charge negligible against λM\lambda_M. The order of choice, D2D_2 then D1D_1 then ϵ\epsilon, is what matters here.
Classified routine:
Choosing constants in a fixed order so that a geometric series and a polynomially small error term fit inside the inductive bound is ordinary bookkeeping. It follows directly from the recurrence in claim-prop-fp-coupling-2 and the depth bound h∗≤ϵlog⁡2Bh_*\le\epsilon\log_2 B.

Uses

claimCoupling recurrence from child charges

Used by

claimCoupling plus clean bound gives targetclaimOrder of constant choices is consistent

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choosing D2, D1, epsilon closes recurrence" rests on claim-prop-fp-coupling-2