ExampleConstruction: AI-generatedVerification: 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.

Four coordinates of a Walsh–Hadamard codeword

Example

For $u = (1, 0)$ and $v = (0, 1)$ in $F_{2}^{2}$ , use lexicographic masks $(00, 01, 10, 11)$ . Their Walsh–Hadamard tables are respectively $(0, 0, 1, 1)$ and $(0, 1, 0, 1)$ , so they differ in two of four coordinates. For $f = {WH}_{2} (u)$ , the BLR test accepts the sample $x = 10, y = 01$ .

Facts & Assumptions

Given: The two fixed messages $u = (1, 0)$ and $v = (0, 1)$ , and the fixed BLR sample $x = 10, y = 01$ .

[F1]

A Walsh–Hadamard table evaluates the linear function $r \mapsto a \cdot r$ on masks $r \in F_{2}^{n}$ , indexed lexicographically. (Walsh–Hadamard encoding and relative Hamming distance)

[F2]

Distinct messages in dimension $n \geq 1$ have Walsh–Hadamard tables at relative distance exactly $1 / 2$ . (Distinct Walsh–Hadamard words differ on half the cube)

[F3]

The BLR test chooses independent uniform $x, y$ , queries $f (x), f (y), f (x + y)$ , and accepts exactly when $f (x) + f (y) = f (x + y)$ in $F_{2}$ . (The BLR linearity test over F_2)

[F4]

The nearby-decoder theorem defines $ϵ$ as the rejection probability over the full uniform pair $(x, y)$ and assumes $ϵ < 1 / 2$ . (The BLR test supplies a nearby unique linear decoder)

Verification

technique · direct calculation

1.1F1givenalgebra

Using [F1], the dot products of $u = (1, 0)$ on masks $(00, 01, 10, 11)$ are $0, 0, 1, 1$ , while those of $v = (0, 1)$ are $0, 1, 0, 1$ . These are exactly the coordinates of the two stated tables.

2.1F1F2step 1.1algebra

The displayed tables disagree at masks $01$ and $10$ , and agree at $00$ and $11$ . Thus they differ in exactly $2$ of $4$ positions, so their relative distance is $2 / 4 = 1 / 2$ , also as asserted generally by [F2].

2.2F1F3step 1.1algebra

For $f = {WH}_{2} (u)$ , the chosen sample has $x + y = 10 + 01 = 11$ . The table in step 1.1 gives $f (10) = 1$ , $f (01) = 0$ , and $f (11) = 1$ ; hence $f (x) + f (y) = 1 + 0 = 1 = f (x + y)$ in $F_{2}$ , so this BLR sample accepts by [F3].

3.1F3F4step 2.2algebra∎

Step 2.2 checks one fixed transcript only. It does not calculate the rejection fraction over all uniform pairs for an arbitrary oracle table, which is the $ϵ$ in [F4]; in particular, this sample alone does not establish the nearby-decoder theorem's global premise. No choice principle is used: all vectors and four masks are explicitly listed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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, printed pp. 363–364 (standard reference, not scraped)