The sixth Fourier coefficient is the parity imbalance

For a pitch-class set A ⊆ ℤ/12, Ahat A 6 = ∑ a ∈ A, (-1) ^ a.val, the number of even minus the number of odd pitch classes in A; so Ahat A 6 = 0 iff A has as many even as odd pitch classes. The same holds at the frequency m of ℤ/(2m).

Main results

• Ahat_six_eq_sum_neg_one_pow, Ahat_six_eq_card_sub, Ahat_six_eq_zero_iff.
• dftN_half_eq_sum_neg_one_pow: the general even modulus.

References

• E. Amiot, The torii of phases, in Mathematics and Computation in Music (MCM 2013).
• J. Hoffman, On pitch-class set cartography, J. Music Theory 52 (2008).
• C. Marín, The per-voice Fourier signature: the bass is the spectrally purest voice, Zenodo (2026), doi:10.5281/zenodo.20971089.

Part 1 — the half-cycle coefficient is the even−odd parity imbalance.

theorem MusicTheory.ParityA6.Ahat_six_eq_even_sub_odd (A : Finset (ZMod 12)) : Fourier.Ahat A 6 = ∑ a ∈ A, if a ∈ Fourier.evenSet then 1 else -1

FC-K, evenSet form.  A 6 = Σ_{a∈A} (±1) with +1 on even pcs and −1 on odd pcs. Immediate from Ahat_apply and the order-2 character value stdAddChar(−(a·6)) = ±1 (Fourier.stdAddChar_neg_mul_six).

theorem MusicTheory.ParityA6.neg_one_pow_val (a : ZMod 12) : (-1) ^ a.val = if a ∈ Fourier.evenSet then 1 else -1

The ±1 sign at frequency 6 IS (−1)^a.val: even residues ↦ +1, odd residues ↦ −1. a ∈ evenSet ⟺ Even a.val is decidable over ZMod 12; then Even/Odd.neg_one_pow.

theorem MusicTheory.ParityA6.Ahat_six_eq_sum_neg_one_pow (A : Finset (ZMod 12)) : Fourier.Ahat A 6 = ∑ a ∈ A, (-1) ^ a.val

FC-K, the headline (−1)^a form.  A 6 = Σ_{a∈A} (−1)^a — the half-cycle coefficient equals the signed pitch-class count (+1 even, −1 odd).

theorem MusicTheory.ParityA6.Ahat_six_eq_card_sub (A : Finset (ZMod 12)) : Fourier.Ahat A 6 = ↑{x ∈ A | x ∈ Fourier.evenSet}.card - ↑{a ∈ A | a ∉ Fourier.evenSet}.card

FC-K, the card form.  A 6 = #(even pcs of A) − #(odd pcs of A) as a complex number. Split the ±1 sum over the parity partition.

Part 2 — a₆ vanishes iff the pc-set is parity-balanced.

theorem MusicTheory.ParityA6.Ahat_six_eq_zero_iff (A : Finset (ZMod 12)) : Fourier.Ahat A 6 = 0 ↔ {x ∈ A | x ∈ Fourier.evenSet}.card = {a ∈ A | a ∉ Fourier.evenSet}.card

FC-K characterization.  A 6 = 0 ⟺ #(even pcs) = #(odd pcs) — the half-cycle coefficient vanishes exactly when A carries equally many even and odd pitch classes (parity balance).

Witnesses.

Part 3 — the general ZMod (2*m) case: the order-2 element m reads parity.

Frequency m of ZMod (2*m) is the unique element of order 2 (2·m = 0); its character value stdAddChar(−(a·m)) = (−1)^a is the parity sign, so the m-th DFT coefficient of a pc-set over ℤ_{2m} is again the even−odd imbalance Σ_{a∈A} (−1)^a. (The ℤ₁₂ case above is m = 6.)

noncomputable def MusicTheory.ParityA6.indN {N : ℕ} (A : Finset (ZMod N)) : ZMod N → ℂ

General 0/1 indicator on ZMod N.

Equations

• MusicTheory.ParityA6.indN A j = if j ∈ A then 1 else 0

theorem MusicTheory.ParityA6.dftN_apply {N : ℕ} [NeZero N] (A : Finset (ZMod N)) (t : ZMod N) : ZMod.dft (indN A) t = ∑ a ∈ A, ZMod.stdAddChar (-(a * t))

𝓕 (indN A) t = Σ_{a∈A} stdAddChar(−(a·t)) (the indicator collapses the sum to A).

theorem MusicTheory.ParityA6.stdAddChar_half {m : ℕ} [NeZero (2 * m)] : ZMod.stdAddChar ↑m = -1

The order-2 element m has character value −1: stdAddChar (m : ZMod (2m)) = exp(πi) = −1.

theorem MusicTheory.ParityA6.neg_mul_half {m : ℕ} (a : ZMod (2 * m)) : -(a * ↑m) = a * ↑m

The order-2 element is its own negative: −(a·m) = a·m in ZMod (2m).

theorem MusicTheory.ParityA6.dftN_half_eq_sum_neg_one_pow {m : ℕ} [NeZero (2 * m)] (A : Finset (ZMod (2 * m))) : ZMod.dft (indN A) ↑m = ∑ a ∈ A, (-1) ^ a.val

FC-K, general ZMod (2m). The m-th DFT coefficient (the half-cycle / order-2 frequency) of a pc-set over ℤ_{2m} is the even−odd parity imbalance Σ_{a∈A} (−1)^a. The ℤ₁₂ headline Ahat_six_eq_sum_neg_one_pow is the case m = 6.