lemmaroutine

Edge marginals uniform; P-collision bounded

Lemma·bud:pair-laws·§5.2 Three fixed pair experiments

Statement (paper)

Each edge slot of each experiment, after averaging its base, has the original uniform law on EE. For every p∈Pp\in P, the conditional probability of q=q′q=q' in the PθP\theta experiment, averaged over θ\theta conditional on pp, is at most M/d(p)M/d(p).

In plain English

In each of the three pair experiments (Q, P, Pθ), every edge slot has the uniform law on EE once its base is averaged out. In the PθP\theta experiment, for each p∈Pp\in P, the probability that q=q′q=q', averaged over θ\theta given pp, is at most M/d(p)M/d(p).

Why it's here

The uniform marginals let the budget estimates for the three experiments be compared with the same global quantities. The M/d(p)M/d(p) collision bound controls equal-endpoint pairs, which the product formula cannot handle, so they contribute only o(S)o(S) in the upper score budget.
Classified routine:
Direct verification from the definitions of the three pair experiments: averaging over the base gives the uniform edge law, and the collision bound follows from bounded multiplicity M of edges per direction class at a point of degree d(p).

Uses

Nothing else in the paper

Used by

propUpper score budget for pair experimentspropRare-exception lower bound on pair scoresclaimEqual-endpoint collisions contribute o(S)

Sources

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

Phase 2 aligns this node to a Lean declaration.