claimroutineinferred_dep

Slice correlation survives nontrivial restriction

Average slice correlation over nontrivial restrictions is at least

\alpha/8

input for locating Fourier mass on a coset

Claim·§5.6 Decoding the row advice·inside lemFourier decoding agrees with positive probability

Statement (paper)

With

Z'=\bar\pi Z

b=N|_{Z'}

and

C_\sigma=\E\bigl[f_\sigma(N)(-1)^{\sigma(Nz')}\mid N|_{Z'}=b\bigr]

for

\sigma\in K^*

, one has

\E_\sigma\bigl[\mathbf 1_{\{\sigma|_H\ne0\}}|C_\sigma|\bigr]\ge\alpha/8

In plain English

With

Z'=\bar\pi Z

b=N|_{Z'}

and

C_\sigma=\E[f_\sigma(N)(-1)^{\sigma(Nz')}\mid N|_{Z'}=b]

, the average over

\sigma\in K^*

|C_\sigma|

restricted to those

\sigma

with

\sigma|_H\ne0

is at least

\alpha/8

Why it's here

The projected-witness lemma gives a correlation of at least

\alpha/4

between the

O

-prover's answer and

M_Oz'+u

on the slice. This claim rewrites that correlation as an average over characters

\sigma

of the slice correlations

C_\sigma

and shows that the

\sigma

with

\sigma|_H=0

cannot carry more than half of it, leaving

\alpha/8

for nontrivial restrictions. This is the input that the next claim uses to locate Fourier mass on the coset indicated by

\theta_\sigma

Classified routine:

Writes the correlation from the projected-witness lemma as an average over characters (standard Fourier expansion over

K^*

) and bounds the

\sigma|_H=0

part by half; this is bookkeeping that follows from lem-projected-witness.

Uses

lemGood advice transfers to projected slice

Used by

claimFourier mass on indicated frequency coset

Sources

PaperOpen

Section: §5.6 Decoding the row advice
Page: —
Label: —
Line: sections/04-matrix.tex:688

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Slice correlation with nontrivial restriction" rests on lem:projected-witness