claimroutineinferred_dep

Rare levels also small, giving contradiction

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

Statement (paper)

Under the assumption that \liminf_{t\to\infty}\E_\mu H_p^*/S=0 (along a subsequence), the integral of the minority-bit probability ff over good rare levels is o(S)o(S), and damaged levels contribute at most Wb/2=o(S)W_b/2=o(S). Together with ∫Cf=o(S)\int_{\mathcal C}f=o(S) this gives S=∫f=o(S)S=\int f=o(S), a contradiction.

In plain English

If lim inf⁡EμHp∗/S=0\liminf \E_\mu H_p^*/S=0 along a subsequence, then ∫f\int f over good rare levels is o(S)o(S), and damaged levels contribute at most Wb/2=o(S)W_b/2=o(S). Combined with ∫Cf=o(S)\int_{\mathcal C}f=o(S) on common levels, this yields S=∫f=o(S)S=\int f=o(S), a contradiction.

Why it's here

This closes the proof by contradiction of the positivity proposition: the previous claim handles common levels, and this one shows the good rare levels (via the comparison f≤hP+hQ+mf\le h_P+h_Q+m from the rare-moments lemma and the assumed smallness of the exception mass) and the damaged levels are also negligible. All of ∫f=S\int f=S is then o(S)o(S), which is impossible, so the liminf must be positive.
Classified routine:
Direct bookkeeping that closes the contradiction: it combines the comparison f≤hP+hQ+mf\le h_P+h_Q+m from the rare-moments lemma with the previous claim's bound on common levels. Summing the three contributions shows ∫f=o(S)\int f=o(S).

Uses

lemRare exceptions: comparison, first moments, joint boundsclaimSmall star variations force small f on common levels

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Rare levels small too, contradiction S=o(S)" rests on claim-com-rare-positive-4