Alphabeta Math
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.

Character orthogonality, inversion and Parseval

Statement

For n≥0, real functions h,k on F2n and the normalized characters and coefficients, Exχa(x)χb(x)={1a=b,0a≠b,h(x)=∑ah^(a)χa(x), Exh(x)k(x)=∑ah^(a)k^(a),Exh(x)2=∑ah^(a)2. Any two distinct linear Boolean functions ℓa,ℓb disagree on exactly half the cube.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

Characters are real signs (-1)^(a dot x), and coefficients are their normalized finite inner products with h (Characters and normalized Fourier coefficients).

Proof

1.1F1algebra

From the definitions, χaχb=χa+b and χa(x+y)=χa(x)χa(y). If a=b, their product is one everywhere. If a≠b, some coordinate j of a+b equals one. Pair x with x+ej: the pairing is a fixed-point-free involution and reverses the sign of χa+b. Its sum is zero. This proves orthogonality.

2.1F1step 1.1algebra

For fixed x,y, sum χa(x)χa(y)=χa(x+y) over a. If x=y, this sum is 2n. Otherwise pair a with a+ej at a nonzero coordinate of x+y to get zero. Thus ∑aχa(x)χa(y)=2n1x=y. Substituting the coefficient definition gives ∑ah^(a)χa(x)=2−n∑yh(y)∑aχa(y)χa(x)=h(x).

3.1step 1.1step 2.1algebra

Expand both h and k by the preceding identity and average their product. All sums are finite, so rearrangement gives Ehk=∑a,bh^(a)k^(b)Eχaχb=∑ah^(a)k^(a). Taking k=h proves Parseval, also when either function is zero.

4.1step 1.1step 2.1step 3.1algebra∎

For a≠b, the character χa+b is one where ℓa=ℓb and minus one where they differ. Its zero mean therefore forces equal counts of agreement and disagreement. For n=0, there are no distinct indices; the sole character is one and every displayed Fourier identity is an equality of one-term sums. For n=1, the pairing interchanges the two cube points.

Depends on

Used by

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