claimroutineinferred_dep

Rare positives lie on one side only

Claim·§5.2 Three fixed pair experiments·inside propUpper score budget for pair experiments

Statement (paper)

If some rare positive is counted at a fixed base vv, then all positive charges at vv lie on one side, that is, all in I−I_- or all in I+I_+. Their coefficients are at most 22, and their total is at most 2Tv2T_v.

In plain English

If a rare positive is counted at a fixed base vv, then all positive charges at vv lie entirely in I−I_- or entirely in I+I_+. Their coefficients are at most 22 and their total is at most 2Tv2T_v.

Why it's here

The previous claim confines positive charges at vv to the two intervals I−I_- and I+I_+ of length TvT_v on either side of [b,b′][b,b']. This claim shows that a rare positive forces all of them into just one of these intervals, with bounded coefficients and total at most 2Tv2T_v. This is what the central-window and product-formula cancellation step relies on once only common positives remain.
Classified routine:
This is a bookkeeping step inside the score-budget proof. It follows from the preceding place-identity claim, which confines positive charges to the flanking intervals I±I_\pm, by a direct case analysis on valuations at a fixed place.

Uses

claimPlace identity and flanking positive-charge intervals

Used by

claimCentral-window excess and product-formula cancellation

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Rare positives lie on one side only" rests on claim-bud-upper-1