claimroutineinferred_dep

Decoded vector lands in projected answer set

Decoded vector lies in the projected answer set πˉA\bar\pi\mathcal A
links decoder output to the short answer set
Claim·§5.6 Decoding the row advice·inside lemFourier decoding agrees with positive probability

Statement (paper)

Every frequency Φ∈θσ+H∗⊗Z′\Phi\in\theta_\sigma+H^*\otimes Z' with ∣f^σ(Φ)∣2>0|\widehat f_\sigma(\Phi)|^2>0 and σ∣H≠0\sigma|_H\ne0 has the form Φ=(σ∣H)⊗z′+Ψ\Phi=(\sigma|_H)\otimes z'+\Psi with Ψ∈H∗⊗Z′\Psi\in H^*\otimes Z', satisfies Φ(h)∈z′+Z′\Phi(h)\in z'+Z' for the decoder's choice of hh, and the vector returned by the OO-decoder on such a frequency lies in πˉA\bar\pi\mathcal A.

In plain English

Any frequency Φ\Phi in the coset θσ+H∗⊗Z′\theta_\sigma+H^*\otimes Z' with nonzero Fourier weight and σ∣H≠0\sigma|_H\ne0 can be written as (σ∣H)⊗z′+Ψ(\sigma|_H)\otimes z'+\Psi with Ψ∈H∗⊗Z′\Psi\in H^*\otimes Z', satisfies Φ(h)∈z′+Z′\Phi(h)\in z'+Z' at the decoder's chosen hh, and the vector the OO-decoder returns from it lies in πˉA\bar\pi\mathcal A.

Why it's here

This shows that a decoder frequency drawn from the indicated coset gives a vector in the projected answer set πˉA\bar\pi\mathcal A, where A\mathcal A is the short answer set from the good row advice. Together with the previous claim's bound on the probability of landing in that coset, it yields the agreement probability in the parent lemma. The coset structure is what forces the evaluation Φ(h)\Phi(h) into z′+Z′z'+Z'.
Classified routine:
Direct unpacking of the coset structure from the previous claim together with the definition of the O-decoder and the short answer set from lem-good-row-advice. This is a bookkeeping step inside the Fourier decoding argument, not a new idea.

Uses

claimFourier mass on indicated frequency cosetlemGood row advice is common and gives short answer sets

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.6 Decoding the row advice
Page
—
Label
—
Line
sections/04-matrix.tex:737
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Decoded vector lands in projected answer set" rests on claim-lem-fourier-coset-decoding-2
  • info
    inferred_dep
    outline: "Decoded vector lands in projected answer set" rests on lem:good-row-advice