Equation (6.1)Parity is a single character; a (k,ε)-band-limited f has squared correlation ≤ ε with χ_S for |S|>k

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Parity is a pure high-frequency character. For any nonempty $S\subseteq[n]$ , the parity function $\mathrm{PARITY}_S(x)=\chi_S(x)$ has Fourier expansion supported on a single set: $\widehat{\mathrm{PARITY}_S}(S)=1$ and $\widehat{\mathrm{PARITY}_S}(T)=0$ for $T\neq S$ . Thus its spectral “frequency” is exactly $|S|$ . More generally, if $f$ is $(k,\varepsilon)$ -spectrally band-limited and $|S|>k$ , then $\bigl|\mathbb{E}[f(x)\chi_S(x)]\bigr|^2=\hat f(S)^2\le\mathrm{Tail}_{>k}(f)\le\varepsilon.$ (6.1) This elementary inequality is the link between concentration at low degree and small correlation with a high-degree parity.

Generated from paper_jmlr.tex, lines 959–967.

2 Explain this

Parity is a pure character. The parity of the inputs in a nonempty set $S$ is exactly $\chi_S$ , so its Fourier expansion has one coefficient, $1$ at $S$ . Its frequency is $|S|$ .

The inequality. The correlation of $f$ with $\chi_S$ is the coefficient $\hat f(S)$ . If $|S|>k$ , its square is one term of the tail above $k$ , hence at most $\varepsilon$ for a band-limited $f$ . So: little high-frequency mass implies little correlation with high-degree parities.

This elementary step is fully proved; what is external is the claim that AC⁰ functions are band-limited.

3 How this is formalised

Fourier.coef_chi: the coefficient of $\chi_S$ is $1$ at $S$ and $0$ elsewhere; Fourier.chi_exactDeg: its exact degree is $|S|$ .
RealFourier.bandLimited_corr_real: over the reals, if $f$ is $(k,\varepsilon)$ -band-limited and $|S|>k$ , then $\langle f,\chi_S\rangle^2\le\varepsilon$ .

Coverage record
Paper anchor	`eq:tail-correlation` (manuscript label)
Displayed as	Equation (6.1)
Claim	Parity is a single character; a (k,ε)-band-limited f has squared correlation ≤ ε with χ_S for \|S\|>k
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 959–967; SHA-256 of the normalised block source `2a3991e3eaeca296…`
Lean declarations	`NimAudit.Fourier.coef_chi` (Fourier, lines 445–451, file `afffe6072d70…`) `NimAudit.Fourier.chi_exactDeg` (Fourier, lines 468–473, file `afffe6072d70…`) `NimAudit.RealFourier.bandLimited_corr_real` (RealFourier, lines 194–196, file `e0e69edd199d…`)
Audited correspondence rows	`eq:tail-correlation`
Explanations	`explain/eq:tail-correlation`, `formal/eq:tail-correlation`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Fourier.coef_chi`

Module Fourier (lean/phase8/Fourier.lean, lines 445–451) · file SHA-256 afffe6072d707e40… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

PARITY IS A PURE CHARACTER: the coefficient of χ_S is 1 at S and 0 elsewhere.

Statement as elaborated and printed by Lean 4.26.0

∀ {R : Type} [inst : Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Grind.OrderedRing R] {n : ℕ} {S T : List Bool},
  S ∈ NimAudit.Bridge.bitvecs n →
    T ∈ NimAudit.Bridge.bitvecs n →
      NimAudit.Fourier.coef n (NimAudit.Fourier.chi S) T = if T = S then 1 else 0

Exact source text, lines 445–451

445/-- PARITY IS A PURE CHARACTER: the coefficient of χ_S is 1 at S and 0 elsewhere. -/446theorem coef_chi {n : Nat} {S T : List Bool} (hS : S ∈ bitvecs n) (hT : T ∈ bitvecs n) :447    coef n (chi S) T = (if T = S then 1 else 0 : R) := by448  unfold coef; rw [orthonormal hS hT]449  by_cases h : S = T450  · subst h; simp451  · rw [if_neg h, if_neg (fun e => h e.symm)]

Project declarations in the statement: Bridge.bitvecs, Fourier.chi, Fourier.coef

Project declarations used by the proof or definition body

Bridge.bitvecs, Fourier.chi, Fourier.coef, Fourier.ip, Fourier.orthonormal

theorem `Fourier.chi_exactDeg`

Module Fourier (lean/phase8/Fourier.lean, lines 468–473) · file SHA-256 afffe6072d707e40… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

… and its exact degree is |S|.

Statement as elaborated and printed by Lean 4.26.0

∀ {R : Type} [inst : Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Grind.OrderedRing R] {n : ℕ} {S : List Bool},
  S ∈ NimAudit.Bridge.bitvecs n →
    NimAudit.Fourier.ExactDeg n (NimAudit.Fourier.chi S) (NimAudit.Bridge.ones S)

Exact source text, lines 468–473

468/-- … and its exact degree is |S|. -/469theorem chi_exactDeg {n : Nat} {S : List Bool} (hS : S ∈ bitvecs n) : ExactDeg n (chi (R := R) S) (ones S) := by470  refine ⟨fun T hT hk => ?_, S, hS, rfl, ?_⟩471  · rw [coef_chi hS hT, if_neg (fun e => by subst e; omega)]472  · rw [coef_chi hS hS, if_pos rfl]473    intro h; have := OrderedRing.zero_lt_one (R := R); rw [h] at this; exact Preorder.lt_irrefl _ this

Project declarations in the statement: Bridge.bitvecs, Bridge.ones, Fourier.ExactDeg, Fourier.chi

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.ones, Fourier.DegLe, Fourier.chi, Fourier.coef, Fourier.coef_chi

theorem `RealFourier.bandLimited_corr_real`

Module RealFourier (lean/phase8/RealFourier.lean, lines 194–196) · file SHA-256 e0e69edd199d8650… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

∀ {n : ℕ} {f : List Bool → ℝ} {k : ℕ} {ε : ℝ},
  NimAudit.Fourier.BandLimited n f k ε →
    ∀ {S : List Bool},
      S ∈ NimAudit.Bridge.bitvecs n →
        k < NimAudit.Bridge.ones S → NimAudit.Fourier.ip n f (NimAudit.Fourier.chi S) ^ 2 ≤ ε

Exact source text, lines 194–196

194theorem bandLimited_corr_real {n : ℕ} {f : List Bool → ℝ} {k : ℕ} {ε : ℝ} (hb : BandLimited n f k ε)195    {S : List Bool} (hS : S ∈ bitvecs n) (hk : k < ones S) : ip n f (chi S) ^ 2 ≤ ε :=196  bandLimited_corr hb hS hk

Project declarations in the statement: Bridge.bitvecs, Bridge.ones, Fourier.BandLimited, Fourier.chi, Fourier.ip

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.ones, Fourier.BandLimited, Fourier.bandLimited_corr

Definitions these statements use

def `Bridge.bitvecs`

Module BitBridge (lean/phase3/BitBridge.lean, lines 27–29) · file SHA-256 000644dc271d27f9…

Statement as elaborated and printed by Lean 4.26.0

ℕ → List (List Bool)

Exact source text, lines 27–29

27def bitvecs : Nat → List (List Bool)28  | 0 => [[]]29  | n + 1 => (bitvecs n).map (false :: ·) ++ (bitvecs n).map (true :: ·)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Fourier.chi`

Module Fourier (lean/phase8/Fourier.lean, lines 198–199) · file SHA-256 afffe6072d707e40…

The Walsh–Hadamard character χ_S(x) = (−1)^{⟨S,x⟩}.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → List Bool → List Bool → R

Exact source text, lines 198–199

198/-- The Walsh–Hadamard character χ_S(x) = (−1)^{⟨S,x⟩}. -/199def chi (S x : List Bool) : R := sg (pm S x)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.pm, Noise.sg

def `Fourier.coef`

Module Fourier (lean/phase8/Fourier.lean, lines 218–219) · file SHA-256 afffe6072d707e40…

Fourier coefficient f̂(S) = E_x[f(x) χ_S(x)].

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → List Bool → R

Exact source text, lines 218–219

218/-- Fourier coefficient f̂(S) = E_x[f(x) χ_S(x)]. -/219def coef (n : Nat) (f : List Bool → R) (S : List Bool) : R := ip n f (chi S)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Fourier.chi, Fourier.ip

def `Bridge.ones`

Module BitBridge (lean/phase3/BitBridge.lean, lines 275–276) · file SHA-256 000644dc271d27f9…

Number of ones in a bit list.

Statement as elaborated and printed by Lean 4.26.0

List Bool → ℕ

Exact source text, lines 275–276

275/-- Number of ones in a bit list. -/276def ones (l : List Bool) : Nat := (l.filter id).length

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Fourier.ExactDeg`

Module Fourier (lean/phase8/Fourier.lean, lines 390–392) · file SHA-256 afffe6072d707e40…

Exact Fourier degree d.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → ℕ → Prop

Exact source text, lines 390–392

390/-- Exact Fourier degree d. -/391def ExactDeg (n : Nat) (f : List Bool → R) (d : Nat) : Prop :=392  DegLe n f d ∧ ∃ T ∈ bitvecs n, ones T = d ∧ coef n f T ≠ 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.ones, Fourier.DegLe, Fourier.coef

def `Fourier.BandLimited`

Module Fourier (lean/phase8/Fourier.lean, lines 384–385) · file SHA-256 afffe6072d707e40…

(k, ε)-spectrally band-limited.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → [LE R] → ℕ → (List Bool → R) → ℕ → R → Prop

Exact source text, lines 384–385

384/-- (k, ε)-spectrally band-limited. -/385def BandLimited (n : Nat) (f : List Bool → R) (k : Nat) (ε : R) : Prop := tail n f k ≤ ε

Project declarations in the statement: none

Project declarations used by the proof or definition body

Fourier.tail

def `Fourier.ip`

Module Fourier (lean/phase8/Fourier.lean, lines 215–216) · file SHA-256 afffe6072d707e40…

Normalised inner product under the uniform distribution on {0,1}^n.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → ℕ → (List Bool → R) → (List Bool → R) → R

Exact source text, lines 215–216

215/-- Normalised inner product under the uniform distribution on {0,1}^n. -/216def ip (n : Nat) (f g : List Bool → R) : R := gs (bitvecs n) (fun x => f x * g x) * ((2 : R) ^ n)⁻¹

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.gs

Full modules

Module	File	Lines	Imports
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Fourier	`lean/phase8/Fourier.lean`	1379	NoiseModel
RealFourier	`lean/phase8/RealFourier.lean`	275	`Mathlib.Data.Real.Archimedean`, `Mathlib.Data.Fintype.BigOperators`, `Mathlib.Algebra.BigOperators.Fin`, `Mathlib.Tactic.Linarith`, `Mathlib.Tactic.Positivity`, `Mathlib.Tactic.FieldSimp`, `Mathlib.Tactic.NormNum`, `Mathlib.Tactic.Ring`, Fourier, RealNoise

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).

Equation (6.1)Parity is a single character; a (k,ε)-band-limited f has squared correlation ≤ ε with χ_S for |S|>k

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Fourier.coef_chi

theorem Fourier.chi_exactDeg

theorem RealFourier.bandLimited_corr_real

Definitions these statements use

def Bridge.bitvecs

def Fourier.chi

def Fourier.coef

def Bridge.ones

def Fourier.ExactDeg

def Fourier.BandLimited

def Fourier.ip

Full modules

theorem `Fourier.coef_chi`

theorem `Fourier.chi_exactDeg`

theorem `RealFourier.bandLimited_corr_real`

def `Bridge.bitvecs`

def `Fourier.chi`

def `Fourier.coef`

def `Bridge.ones`

def `Fourier.ExactDeg`

def `Fourier.BandLimited`

def `Fourier.ip`