LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 cubic Fourier identity for BLR

Statement

For a fixed $f : F_{2}^{n} \to F_{2}$ , $n \geq 0$ , put $h (x) = (- 1)^{f (x)}$ . If the BLR acceptance probability is $α$ , then $2 α - 1 = E_{x, y} h (x) h (y) h (x + y) = \sum_{a \in F_{2}^{n}} \hat{h} (a)^{3},$ where $x, y$ are independent uniform points and the Fourier coefficients are real and normalized.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Every real cube function has the stated normalized Fourier expansion and the characters are orthonormal (Character orthogonality, inversion and Parseval).

Proof

1.1

The product $h (x) h (y) h (x + y)$ is one exactly when $f (x) + f (y) + f (x + y) = 0$ modulo two, and minus one otherwise. Thus its expectation is $α - (1 - α) = 2 α - 1$ , including $α = 0, 1$ .

givenalgebra

1.2

Apply Fourier inversion to each of the three factors. The expectation of the resulting finite sum is $\sum_{a, b, c} \hat{h} (a) \hat{h} (b) \hat{h} (c) E_{x, y} χ_{a} (x) χ_{b} (y) χ_{c} (x + y)$ .

F1algebra

2.1

Using $χ_{c} (x + y) = χ_{c} (x) χ_{c} (y)$ and independence of $x, y$ , each expectation factors as $(E_{x} χ_{a} (x) χ_{c} (x)) (E_{y} χ_{b} (y) χ_{c} (y))$ . Orthogonality makes this one exactly when $a = b = c$ and zero otherwise. The sum is therefore $\sum_{a} \hat{h} (a)^{3}$ , as asserted. This is also valid for $n = 0$ , where every sum has one term, and for constant $f$ , where $h$ is the constant sign $1$ or $- 1$ .

F1step 1.1step 1.2algebra∎

Depends on

Character orthogonality, inversion and Parseval

Used by

BLR acceptance implies agreement with a linear function Theorem

Dependency tree · two levels

2 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, January 2007 web draft, Theorem 19.9 proof pp.390–391 (standard reference, not scraped)