propositionroutine

Upper score budget for pair experiments

Proposition·bud:upper·§5.2 Three fixed pair experiments

Statement (paper)

For each i∈{Q,P,Pθ}i\in\{Q,P,P\theta\}, Di≤o(S)+10δ2λCi. D_i\le o(S)+10\delta^2\lambda C_i.

In plain English

In each of the three pair experiments QQ, PP, PθP\theta, the quantity DiD_i is at most o(S)o(S) plus 10δ2λCi10\delta^2\lambda C_i.

Why it's here

This is the upper half of the score budget. For pairs with distinct endpoints, the product formula cancels the logarithmic size at every place. Only central-window excesses remain, and these are rare enough to cost 10δ2λCi10\delta^2\lambda C_i. Equal-endpoint collisions cost o(S)o(S) by the pair-law and rare-exception bounds. The common-variation argument compares this upper bound with a lower bound of order λCi\lambda C_i to force CiC_i to be small.
Classified routine:
A bookkeeping consequence of the interval overlap envelope, the pair-law bounds and the rare-exception moment bounds, combined via the product formula for distinct endpoints. It is one half of the paper's score-budget argument rather than a new idea in itself.

Uses

lemInterval overlap envelope and interior mass boundlemEdge marginals uniform; P-collision boundedlemChoice of hierarchy parameters K, L, klemRare exceptions: comparison, first moments, joint bounds

Used by

propCommon variation is negligibleclaimCommon variation is negligible by budget comparisonclaimCenter rare exceptions bounded by point onesclaimPoint-star common variation is negligible

Inside the proof

claimPlace identity and flanking positive-charge intervalsclaimRare positives lie on one side onlyclaimCentral-window excess and product-formula cancellationclaimAveraging bounds distinct-pair budget by 10δ²λC_iclaimEqual-endpoint collisions contribute o(S)

Sources

PaperOpen
Section
§5.2 Three fixed pair experiments
Page
—
Label
bud:upper
Line
sections/04-budgets.tex:293
Leannot aligned

Phase 2 aligns this node to a Lean declaration.