claimroutineinferred_dep

Clean active tasks meet target bounds

Block-clean active tasks meet the target bounds of the clean error reserve
clean half of the coupled induction
Claim·§9.5 Closing the coupled induction·inside propActual runs stay close to clean runs

Statement (paper)

In the strong induction on the statistical budget, for every active task of budget M∈IbM\in\mathcal I_b and precision pp, the block-clean version of the task satisfies the target estimates of Proposition , with the spare constants there. This holds because lower-block children coincide in a block coupling and already satisfy their actual target bounds, and same-block clean children satisfy the clean target bounds at smaller budgets.

In plain English

In the strong induction on the statistical budget, every active task of budget M∈IbM\in\mathcal I_b and precision pp has a block-clean version that satisfies the target estimates of Proposition est-clean, with the spare constants given there.

Why it's here

This closes the clean half of the coupled induction. Lower-block children coincide with the clean run in the block coupling and already meet their actual target bounds, while same-block clean children meet the clean bounds at smaller budgets, so the hypotheses of the error-reserve proposition (prop-est-clean) hold. The salt-free clean calculation (lem-fp-clean) and the prefix estimates (lem-est-prefix) make that proposition applicable to the clean run. The claim therefore supplies the clean estimate that is later added to the coupling discrepancy to give the final target error bounds.
Classified routine:
An inductive bookkeeping step inside the coupled induction. It checks the hypotheses of prop-est-clean using the block coupling (lower-block children coincide), the strong induction hypothesis for same-block children, lem-fp-clean and lem-est-prefix.

Uses

lemClean calculation is independent of the saltpropError reserve after compression and clampinglemMean prefixes small, noise prefixes tiny

Used by

claimCoupling plus clean bound gives target

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Clean active target bounds within induction" rests on lem:est-prefix