claimroutineinferred_dep

Point-star common variation is negligible

Claim·§6.3 A second score forces positive rare mass·inside propRare point exceptions have positive mass

Statement (paper)

Under the present assumptions on both exception means, the common point-star variation satisfies CP=o(S)C_P=o(S).

In plain English

Under the assumptions that both rare-exception means are small, the common point-star variation satisfies CP=o(S)C_P=o(S).

Why it's here

This averages the pointwise slice inequality (claim-com-rare-positive-2) over common levels to bound CPC_P by the point-star score plus error terms. That score is then controlled from above by the budget in bud-upper and from below by the rare-exception bound in bud-rare-lower, which makes CPC_P negligible. This feeds the next claim, which turns small star variations into small ff on common levels.
Classified routine:
A direct consequence of earlier nodes: the pointwise slice inequality (claim-com-rare-positive-2) is averaged over common levels and then combined with the upper budget (bud-upper) and the rare-exception lower bound (bud-rare-lower). This is bookkeeping inside the paper's framework, not a new idea.

Uses

propRare-exception lower bound on pair scoresclaimPointwise point-star slice inequalitypropUpper score budget for pair experiments

Used by

claimSmall star variations force small f on common levels

Sources

PaperOpen
Section
§6.3 A second score forces positive rare mass
Page
—
Label
—
Line
sections/05-common-levels.tex:517
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Point-star common variation C_P=o(S)" rests on claim-com-rare-positive-2
  • info
    inferred_dep
    outline: "Point-star common variation C_P=o(S)" rests on bud:upper