claimroutine

Advice coefficients are independent uniform

Advice intercept and slope columns are independent uniform in EAE_A
gives advice coefficients a data-free law
Claim·§6.2 Vanishing advice on clean coordinates·inside lemAdvice agreement decays with clean coordinates

Statement (paper)

Conditional on AA, the questions and the projection choices, the intercept cOc_O and all block slope columns of DO=(TO,SO):LO→EA=W⊕im⁡AD_O=(T_O,S_O):L_O\to E_A=W\oplus\im A are independent uniform elements of EAE_A. This coefficient law depends only on whether a block is an equation or a singleton, and not on any equation ID, variable ID, or selected position; in particular, cOc_O is independent of all block data.

In plain English

Conditioned on AA, the questions and the projection choices, the intercept cOc_O and every block slope column of DO=(TO,SO)D_O=(T_O,S_O) are independent uniform elements of EA=W⊕im⁡AE_A=W\oplus\im A. The law depends only on whether a block is an equation or a singleton, not on any equation ID, variable ID or selected position.

Why it's here

This gives the advice coefficients an explicit, data-independent law. In particular cOc_O is independent of all block data, and each slope column is uniform in EAE_A. The next claim uses this to compute the probability that a coordinate is clean, namely that it is projected to a singleton and its advice slope is zero, which is β/∣EA∣\beta/|E_A|.
Classified routine:
Follows directly from how the paper's reduction samples the advice map (independent uniform coefficients in EAE_A). This is a bookkeeping observation about the construction's randomness, not a new technique.

Uses

Nothing else in the paper

Used by

claimClean coordinates have ordinary question law

Sources

PaperOpen
Section
§6.2 Vanishing advice on clean coordinates
Page
—
Label
—
Line
sections/05-clean.tex:107
Leannot aligned

Phase 2 aligns this node to a Lean declaration.