propositionroutineinferred_dep

Rare-exception lower bound on pair scores

Proposition·bud:rare-lower·§5.2 Three fixed pair experiments

Statement (paper)

For each of the three pair experiments, let xx be its star vertex and yy an opposite endpoint. Its score integrated outside C\mathcal C is at least 2EHx∗−2EHy∗−o(S), 2\E H_x^*-2\E H_y^*-o(S), where both expectations use the original edge marginals on the appropriate sides. In particular this is 2EκHq∗−2EμHp∗−o(S)2\E_\kappa H_q^*-2\E_\mu H_p^*-o(S) for QQ, and its opposite main term for either PP or PθP\theta.

In plain English

In each of the three pair experiments (Q, P, Pθ), with star vertex xx and an opposite endpoint yy, the score integrated outside C\mathcal C is at least 2EHx∗−2EHy∗−o(S)2\E H_x^*-2\E H_y^*-o(S), using the original edge marginals. For QQ this reads 2EκHq∗−2EμHp∗−o(S)2\E_\kappa H_q^*-2\E_\mu H_p^*-o(S), and for PP or PθP\theta the main term has the opposite sign.

Why it's here

This gives a lower bound on each experiment's score in terms of the rare-exception means at its star vertex and its opposite endpoint. The uniform edge marginals (bud-pair-laws) let both means be taken under the original edge laws, and the joint-exception bounds (bud-rare-moments) make the correlated terms o(S)o(S). The bound can then be set against the upper score budgets in the common-variation and rare-positivity arguments that use it.
Classified routine:
A direct consequence of the earlier nodes: the uniform edge marginals from bud-pair-laws let both means be taken under the original edge laws, and the joint-exception bounds from bud-rare-moments make the correlated terms o(S). The remaining work is bookkeeping of first moments in the pair experiments.

Uses

lemEdge marginals uniform; P-collision boundedlemRare exceptions: comparison, first moments, joint bounds

Used by

propCommon variation is negligiblepropRare point exceptions have positive massclaimCommon variation is negligible by budget comparisonclaimCenter rare exceptions bounded by point onesclaimPoint-star common variation is negligible

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: 04-budgets.tex:433-434: "The integrals of the joint terms I_xI_{y_j} are o(S) by ", from Lemma bud:rare-moments.