lemmaroutineinferred_dep

Fourier decoding agrees with positive probability

Two independent Fourier decoders agree with constant probability

gives the agreement bound used in matrix decoding

Lemma·lem:fourier-coset-decoding·§5.6 Decoding the row advice

Statement (paper)

Fix joint data satisfying Lemma . Conditional on these data, the two rules just defined, using independent randomness, agree under

\bar\pi

with probability at least

2^{-\ell r_{\rm s}}(\alpha/8)^2\,2^{-r_{\rm s}}.

In plain English

Given joint data satisfying the projected-witness lemma, the two decoding rules, run with independent randomness, give the same output under

\bar\pi

with probability at least

2^{-\ell r_{\rm s}}(\alpha/8)^2\,2^{-r_{\rm s}}

, conditional on that data.

Why it's here

This is the conditional agreement bound that the matrix decoding proposition uses. The proof turns the

\alpha/4

slice correlation from the projected-witness lemma into Fourier mass on a coset (first two claims), then shows the decoded vector lies in the projected answer set

\bar\pi\mathcal A

(third claim). The short answer set then makes it likely that the other rule's guess matches, which accounts for the extra factor

2^{-r_{\rm s}}

Classified routine:

Standard Fourier-analytic list-decoding argument (correlation with a coset character implies Fourier mass, then decode by sampling from the Fourier distribution). It is adapted here to the projected-witness data of the preceding lemma, with the 2^{-r_s} factor coming from the short answer set.

Uses

lemGood advice transfers to projected slice

Used by

propMatrix test passing yields decoding strategies

Inside the proof

claimSlice correlation survives nontrivial restrictionclaimFourier mass on indicated frequency cosetclaimDecoded vector lands in projected answer set

Figures

A flow diagram with a Referee box at top that samples $U,O,\bar\pi,A,T_O,M_O$, sets $S_O=AM_O$, and sends inputs down two parallel columns. The left column is the Equation decoder receiving $(U,A,T_U,S_U)$ with $T_U=T_O\bar\pi$, $S_U=S_O\bar\pi$; it picks a slice witness and answer set $\mathcal A=(z+Z)\cap\{v:e_0^\top v=1\}$ and samples $a_U$ uniformly from it. The right column is the Projected decoder receiving $(O,A,T_O,S_O)$; it sets $H=\ker A$, chooses $M_0$ with $AM_0=S_O$, samples $\sigma\in K^*$ and $\Phi$ with probability $|\widehat f_\sigma(\Phi)|^2$, and outputs $a_O=\Phi(h)$ for a fixed $h\in H$ with $\sigma(h)=1$. Both outputs satisfy $e_0^\top a=1$ and feed into a bottom box where the referee checks $\bar\pi a_U=a_O$. — Figure 3diagramp. 31
The two decoders use independent random tapes. Neither receives the sampled $M_O$ or the projection $\bar\pi$ ; the right decoder chooses its own representative $M_0$ from the visible advice. Every displayed advice map includes its affine intercept, through the homogeneous coordinate. The transferred slice is used only to analyze these private rules: the right decoder does not use the left witness or answer set. If the left advice is not good, or if $\sigma|_H=0$ on the right, that decoder returns an arbitrary valid answer.
What it shows
A flow diagram with a Referee box at top that samples $U,O,\bar\pi,A,T_O,M_O$ , sets $S_O=AM_O$ , and sends inputs down two parallel columns. The left column is the Equation decoder receiving $(U,A,T_U,S_U)$ with $T_U=T_O\bar\pi$ , $S_U=S_O\bar\pi$ ; it picks a slice witness and answer set $\mathcal A=(z+Z)\cap\{v:e_0^\top v=1\}$ and samples $a_U$ uniformly from it. The right column is the Projected decoder receiving $(O,A,T_O,S_O)$ ; it sets $H=\ker A$ , chooses $M_0$ with $AM_0=S_O$ , samples $\sigma\in K^*$ and $\Phi$ with probability $|\widehat f_\sigma(\Phi)|^2$ , and outputs $a_O=\Phi(h)$ for a fixed $h\in H$ with $\sigma(h)=1$ . Both outputs satisfy $e_0^\top a=1$ and feed into a bottom box where the referee checks $\bar\pi a_U=a_O$ .
Read from the image by claude-opus-5.5 · confidence 80%
SupportsdefProjected advice experimentlemFourier decoding agrees with positive probabilitypropMatrix test passing yields decoding strategieslemGood row advice is common and gives short answer setslemGood advice transfers to projected slice

Sources

PaperOpen

Section: §5.6 Decoding the row advice
Page: —
Label: lem:fourier-coset-decoding
Line: sections/04-matrix.tex:676

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The statement of Lemma 5.8 (sections/04-matrix.tex:678) begins "Fix joint data satisfying Lemma ". This dependency exists only on a child claim, not on the lemma node itself.