Tritone symmetry is a phase fact

A pitch-class set A ⊆ ℤ/12 is fixed by the tritone transposition T₆ iff its discrete Fourier transform Â vanishes at every odd frequency. The engine is  (T₆ A) t = (-1)ᵗ ·  A t (Fourier.Ahat_tpose at k = 6) together with injectivity of Â (Fourier.Ahat_injective).

Main results

• stdAddChar_neg_six_mul_of_odd, stdAddChar_neg_six_mul_of_not_odd: the tritone character t ↦ exp(-2πi·6t/12) is -1 at odd t and 1 at even t.
• tpose_six_eq_iff: T₆ A = A ↔ ∀ t, Odd t.val → Â A t = 0.

References

• C. Marín, The phase taxonomy of pitch-class set invariants, Zenodo (2026), doi:10.5281/zenodo.20826773, §7 (P4).

theorem MusicTheory.TritoneFixedFourier.neg_six_mul_cases (t : ZMod 12) : (¬Odd t.val → -(6 * t) = 0) ∧ (Odd t.val → -(6 * t) = 6)

6t reduces to 0 at even t and to 6 at odd t (finite check in ZMod 12).

theorem MusicTheory.TritoneFixedFourier.stdAddChar_six : ZMod.stdAddChar 6 = -1

The value of the standard character at the tritone is -1.

theorem MusicTheory.TritoneFixedFourier.stdAddChar_neg_six_mul_of_odd {t : ZMod 12} (ht : Odd t.val) : ZMod.stdAddChar (-(6 * t)) = -1

The tritone character: exp(-2πi·6t/12) = (-1)ᵗ.

theorem MusicTheory.TritoneFixedFourier.stdAddChar_neg_six_mul_of_not_odd {t : ZMod 12} (ht : ¬Odd t.val) : ZMod.stdAddChar (-(6 * t)) = 1

The tritone character is 1 at even frequencies.

theorem MusicTheory.TritoneFixedFourier.tpose_six_eq_iff (A : Finset (ZMod 12)) : Fourier.tpose 6 A = A ↔ ∀ (t : ZMod 12), Odd t.val → Fourier.Ahat A t = 0

Tritone symmetry is a phase fact. T₆ A = A iff  A vanishes at every odd frequency.