lemmaroutine

Small rare exceptions force small prediction score

Lemma·com:prediction-score·§6.3 A second score forces positive rare mass

Statement (paper)

If EμHp∗=o(S)\E_\mu H_p^*=o(S), then T≤o(S)T\le o(S).

In plain English

If the expected good rare point exceptions EμHp∗\E_\mu H_p^* are o(S)o(S), then the second score TT is also at most o(S)o(S).

Why it's here

This is the implication that links the two scores: if rare point exceptions vanish relative to SS, the prediction score TT cannot be of order SS. Proposition 6.5 uses it by contradiction, since assuming the liminf of EμHp∗/S\E_\mu H_p^*/S is zero gives T≤o(S)T\le o(S), which clashes with a lower bound on TT and so forces positive rare mass.
Classified routine:
A direct bookkeeping step comparing the paper's second (prediction) score with the rare-exception count; it only links two quantities the paper itself defines and has no external source. It serves as one half of the contradiction argument in Proposition 6.5.

Uses

Nothing else in the paper

Used by

propRare point exceptions have positive massclaimFailure forces small exceptions and small T

Sources

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

Phase 2 aligns this node to a Lean declaration.