claimroutineinferred_dep

Slice score lower bound via classification

Claim·§6.2 Classification and suppression of common variation·inside propCommon variation is negligible

Statement (paper)

For every slice

\theta

, with an absolute constant

C

d_Q(\theta)+d_{P\theta}(\theta)\ge\frac\lambda4\bigl(V_Q(\theta)+V_{P\theta}(\theta)\bigr)-C b_\theta

; this holds in each case of the classification of the candidate set: empty, one candidate state, two candidates sharing a coordinate (all candidates in that row or column, or a third outside it), and no coordinate shared by distinct candidates.

In plain English

For every template slice

\theta

, the sum of the scores

d_Q(\theta)+d_{P\theta}(\theta)

is at least

\frac\lambda4

times the common variation

V_Q(\theta)+V_{P\theta}(\theta)

, minus an error

C b_\theta

with

C

absolute. This is checked case by case over the candidate set: empty, one candidate state, two candidates sharing a row or column, or distinct candidates sharing no coordinate.

Why it's here

This gives the slice-wise inequality that the next claim sums against

\pi_\theta

to compare the score budget

D_Q+D_{P\theta}

with the common contributions

C_Q+C_{P\theta}

. The classification of candidates into strict-cross configurations shows that common variation forces a proportional score, and the bad-slot pairs are absorbed into the

O(b_\theta)

error as set up in the previous claim, with the transfer and ghost lemmas used to locate the true point state inside the selected support.

Classified routine:

A case-by-case verification within the proof of the common-variation lemma. It combines the preceding template-slice claim with the transfer and ghost lemmas to derive a slice-wise inequality, which is bookkeeping and not a new idea in its own right.

Uses

claimTemplate slices and bad-slot probabilitylemTransfer from sampled histories to actual pointlemSampled points rarely hide in light boxes

Used by

claimCommon variation is negligible by budget comparison

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: —
Line: sections/05-common-levels.tex:285

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Slice score lower bound by strict-cross classification" rests on claim-com-variation-1
info
inferred_dep
outline: "Slice score lower bound by strict-cross classification" rests on com:transfer
info
inferred_dep
outline: "Slice score lower bound by strict-cross classification" rests on com:ghost