propositionroutinestructure_uncertain

Common variation is negligible

Proposition·com:variation·§6.2 Classification and suppression of common variation

Statement (paper)

For the center-star and point--template-star experiments of ,

C_Q+C_{P\theta}=o(S).

Moreover their rare exception means satisfy

\E_\kappa H_q^*\le\E_\mu H_p^*+o(S).

In plain English

In the center-star and point–template-star experiments, the total common contribution satisfies

C_Q+C_{P\theta}=o(S)

. Moreover the center rare exception mean is at most the point one up to a lower-order error:

\E_\kappa H_q^*\le\E_\mu H_p^*+o(S)

Why it's here

The proof classifies candidate configurations on each template slice to show that common variation forces a proportional score, with the transfer lemma locating the true point state. Summing over slices gives a lower bound of order

\lambda(C_Q+C_{P\theta})

on the score budget, which the upper budget can match only if

C_Q+C_{P\theta}=o(S)

. The rare-exception lower bound then turns the resulting

o(S)

score of the

Q

experiment into the comparison of rare means.

Classified routine:

This follows from the paper's earlier pieces: the upper score budget (bud-upper), the transfer lemma and the rare-exception lower bound are combined in a case classification and summed over slices. It is the bookkeeping step within the paper's new budget framework rather than a separate new idea.

Uses

lemTransfer from sampled histories to actual pointpropRare-exception lower bound on pair scorespropUpper score budget for pair experiments

Used by

propRare point exceptions have positive masslemPoint profiles approximate wedge differencesclaimFailure forces small exceptions and small TclaimSmall star variations force small f on common levels

Inside the proof

claimTemplate slices and bad-slot probabilityclaimSlice score lower bound via classificationclaimCommon variation is negligible by budget comparisonclaimCenter rare exceptions bounded by point ones

Figures

Four states sit at the corners of a square formed by two horizontal and two vertical gray lines. Open circles at bottom-left and top-right are the candidate center states $y_1=(a,b)$ and $y_2=(a',b')$. Filled blue circles at bottom-right $(a,b')$ and top-left $(a',b)$ are the two point states in their common strict cross. The horizontal sides are labeled $Y=1$ and the vertical sides $Y=0$, showing that within this four-state configuration an edge bit together with either endpoint state determines the state at the other endpoint. — Figure 2schematicp. 31
Two candidate center states differing in both coordinates admit exactly two point states in their common strict cross. The filled points are those opposite corners. Within this four-state configuration, the bit of a consistent edge and the state at either endpoint determine the state at the other endpoint. Rows have fixed first label and columns have fixed second label. The diagram displays coordinate equalities of states, not geometric positions of the original plane points.
What it shows
Four states sit at the corners of a square formed by two horizontal and two vertical gray lines. Open circles at bottom-left and top-right are the candidate center states $y_1=(a,b)$ and $y_2=(a',b')$ . Filled blue circles at bottom-right $(a,b')$ and top-left $(a',b)$ are the two point states in their common strict cross. The horizontal sides are labeled $Y=1$ and the vertical sides $Y=0$ , showing that within this four-state configuration an edge bit together with either endpoint state determines the state at the other endpoint.
Read from the image by claude-opus-5.5 · confidence 72%
SupportspropCommon variation is negligibleclaimSlice score lower bound via classification

Sources

PaperOpen

Section: §6.2 Classification and suppression of common variation
Page: —
Label: com:variation
Line: sections/05-common-levels.tex:246

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
structure_uncertain
Proof uses com:ghost via eq. com:mixture and the bad-mass estimate, though the skeleton refs list only com:transfer; ext:band likewise uses ext:profiles via equation refs.