claimroutineinferred_dep

Clean coordinates have ordinary question law

Coordinates are independently clean with probability β/∣EA∣\beta/|E_A|, ordinary question law
gives cleanness probability and unbiased questions
Claim·§6.2 Vanishing advice on clean coordinates·inside lemAdvice agreement decays with clean coordinates

Statement (paper)

Conditional on AA, the clean indicators (coordinate ii is projected to a singleton and its one advice slope di∈EAd_i\in E_A is zero) are independent, each with probability pA=β/∣EA∣=β 2−dim⁡W−rank⁡Ap_A=\beta/\abs{E_A}=\beta\,2^{-\dim W-\rank A}. Moreover, for every equation occurrence ee and position j∈[3]j\in[3], Pr⁡[ei=e, i is a clean singleton at position j∣A]=ωe β/(3∣EA∣)\Pr[e_i=e,\ i\text{ is a clean singleton at position }j\mid A]=\omega_e\,\beta/(3\abs{E_A}), so that, conditional on being clean, a coordinate has precisely the ordinary equation--variable distribution.

In plain English

Given AA, the coordinates are independently clean (projected to a singleton with zero advice slope) with probability pA=β/∣EA∣=β 2−dim⁡W−rank⁡Ap_A=\beta/|E_A|=\beta\,2^{-\dim W-\rank A}. For each equation occurrence ee and position jj, the probability that ei=ee_i=e and ii is a clean singleton at position jj is ωeβ/(3∣EA∣)\omega_e\beta/(3|E_A|), so a clean coordinate has the usual equation–variable question distribution.

Why it's here

Because the advice slope is uniform in EAE_A and independent of the question and projection data (previous claim), the zero-slope event costs a flat factor 1/∣EA∣1/|E_A| that does not depend on which equation or position was chosen. Cleanness is therefore independent across coordinates and unbiased with respect to the question law, which gives the binomial clean count and the game-question law of clean pairs used in the following claims.
Classified routine:
A direct consequence of the preceding claim that the advice slopes are independent and uniform on EAE_A: the zero-slope event multiplies the singleton-projection probability β\beta by 1/∣EA∣1/|E_A|, and independence across coordinates is bookkeeping on top of that.

Uses

claimAdvice coefficients are independent uniform

Used by

claimClean pairs are independent game questionsclaimAveraging over binomial clean count

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Clean coordinates have ordinary question law" rests on claim-lem-clean-1