LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The BLR test supplies a nearby unique linear decoder

Statement

Let $n \geq 0$ , $f : F_{2}^{n} \to F_{2}$ , $h (x) = (- 1)^{f (x)}$ , and $\hat{h} (a) = E_{x} [h (x) (- 1)^{a \cdot x}]$ . Define its BLR rejection probability by $ϵ = \Pr_{x, y independent uniform in F_{2}^{n}} [f (x + y) \neq f (x) + f (y)] .$ Let $a_{*}$ be the lexicographically first maximizer of $\hat{h} (a)$ over $a \in F_{2}^{n}$ . If $ϵ < 1 / 2$ , then $dist (f, {WH}_{n} (a_{*})) \leq ϵ$ . If $ϵ < 1 / 4$ , this is the unique linear Walsh–Hadamard word at distance less than $1 / 4$ from $f$ . For every requested $r \in F_{2}^{n}$ , the self-corrector ${Corr}_{f} (r; y) = f (y) + f (r + y)$ , with $y$ uniform, returns $a_{*} \cdot r$ with probability at least $1 - 2 ϵ$ .

Facts & Assumptions

[F1]

${WH}_{n} (a)$ is the truth table of $x \mapsto a \cdot x$ ; relative distance is normalized disagreement on the cube. (Walsh–Hadamard encoding and relative Hamming distance)

[F2]

For normalized Boolean-cube characters, Fourier inversion is $h (x) = \sum_{a} \hat{h} (a) χ_{a} (x)$ . (Character orthogonality, inversion and Parseval)

[F3]

Parseval gives $E_{x} h (x)^{2} = \sum_{a} \hat{h} (a)^{2}$ . (Character orthogonality, inversion and Parseval)

[F4]

Distinct linear Walsh–Hadamard words have relative distance exactly $1 / 2$ (and there are no distinct messages when $n = 0$ ). (Distinct Walsh–Hadamard words differ on half the cube)

[F5]

The two-query corrector chooses uniform $y$ and returns $f (y) + f (r + y)$ . (Two-query linear self-correction)

Proof

Given: Fix $n$ and $f$ as in the statement; the vectors $x, y$ in the rejection probability are independent and uniform.

1.1givenalgebra

The BLR test accepts exactly when $f (x) + f (y) + f (x + y) = 0$ in $F_{2}$ . Thus $h (x) h (y) h (x + y)$ is $1$ on acceptance and $- 1$ on rejection, so $E_{x, y} [h (x) h (y) h (x + y)] = 1 - 2 ϵ$ . For $n = 0$ the only pair is $((), ())$ and the test rejects exactly when $f (()) = 1$ , so $ϵ < 1 / 2$ forces $f (()) = 0$ .

2.1F2step 1.1algebra

Write $χ_{a} (x) = (- 1)^{a \cdot x}$ . By Fourier inversion (F2), $h (x + y) = \sum_{a} \hat{h} (a) χ_{a} (x + y)$ , and $χ_{a} (x + y) = χ_{a} (x) χ_{a} (y)$ . Expanding the expectation in step 1.1 and using independence of $x, y$ gives $E_{x, y} [h (x) h (y) h (x + y)] = \sum_{a} \hat{h} (a) (E_{x} h (x) χ_{a} (x)) (E_{y} h (y) χ_{a} (y)) = \sum_{a} \hat{h} (a)^{3}$ .

3.1F1F3step 2.1constructalgebra

Parseval (F3) and $h^{2} = 1$ give $\sum_{a} \hat{h} (a)^{2} = 1$ . With $M = \max_{a} \hat{h} (a)$ , step 2.1 yields $1 - 2 ϵ = \sum_{a} \hat{h} (a)^{3} \leq M \sum_{a} \hat{h} (a)^{2} = M$ . Choose the first maximizer $a_{*}$ in the finite lexicographic order. Since $\hat{h} (a_{*}) = \Pr [f (x) = a_{*} \cdot x] - \Pr [f (x) \neq a_{*} \cdot x]$ , its Walsh–Hadamard word has distance $(1 - \hat{h} (a_{*})) / 2 \leq ϵ$ .

4.1F4step 3.1algebra

If $ϵ < 1 / 4$ , the word from step 3.1 is within distance $< 1 / 4$ . Any other linear word within distance $< 1 / 4$ would, by the triangle inequality for normalized Hamming distance, be at distance $< 1 / 2$ from it, contradicting (F4); for $n = 0$ there is only one linear word. Thus the nearby word is unique.

5.1F1F5step 3.1algebradischarge-construct∎

By (F5), the corrector returns $f (y) + f (r + y)$ . Each point $y$ and $r + y$ is uniform, so each queried value differs from $a_{*} \cdot y$ or $a_{*} \cdot (r + y)$ with probability $δ = dist (f, {WH}_{n} (a_{*})) \leq ϵ$ . A union bound, without assuming independence of the two error events, shows that with probability at least $1 - 2 ϵ$ both values are correct; then their sum is $a_{*} \cdot r$ . When $n = 0$ , $ϵ < 1 / 2$ forces $f (()) = 0$ , and the singleton-table corrector returns the sole linear value $0$ .

Depends on

Used by

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Arora and Barak, Computational Complexity: A Modern Approach, §18.4.1 Theorem 18.23 and local decoding, printed pp. 363–365; §19.3.2 proof of Theorem 19.9, printed pp. 390–391 (standard reference, not scraped)