Fourier amplitudes of subsets of a finite cyclic group

For A ⊆ ZMod N, Ahat A k = ∑ a ∈ A, stdAddChar (-(a * k)), which equals Mathlib's ZMod.dft of the indicator (Ahat_eq_dft). This file collects the interface used by the Huddling inequality: transposition, complementation, consecutive arcs and their geometric sums, unit frequencies, and the threshold argument that reduces the inequality to a geometric selector.

Main results

• Ahat_eq_dft, Ahat_tpose, Ahat_compl, norm_Ahat_le_card.
• card_arc, Ahat_arc, Ahat_arc_geom.
• sum_le_of_threshold, sum_lt_of_strict_threshold.
• norm_Ahat_one_le_arc_of_geometric_selector, norm_Ahat_unit_le_arc_of_geometric_selector.

References

• E. Amiot, Discrete Fourier transform and Bach's good temperament, Music Theory Online 15 (2009).
• C. Marín, Huddling, diatonic and pentatonic scales in Z12: Fourier maxima and convex-energy minima formalized in Lean 4, Zenodo (2026), doi:10.5281/zenodo.23121103.

theorem MusicTheory.CyclicHuddling.exists_phase_real_eq_norm (z : ℂ) : ∃ (u : ℂ), ‖u‖ = 1 ∧ (u * z).re = ‖z‖

Every complex amplitude has a unit phase whose real projection is its norm. This turns a bound on all directional projections into a norm bound.

The exchange step in the geometric Huddling proof is independent of roots of unity.

theorem MusicTheory.CyclicHuddling.sum_le_of_threshold {α : Type u_1} [DecidableEq α] (score : α → ℝ) (A B : Finset α) (c : ℝ) (hcard : B.card = A.card) (hin : ∀ x ∈ A, c ≤ score x) (hout : ∀ x ∉ A, score x ≤ c) : ∑ x ∈ B, score x ≤ ∑ x ∈ A, score x

A set containing all scores above a threshold maximizes their sum among sets of the same cardinality. This is the finite exchange argument needed after projecting the cyclic roots onto any chosen direction.

theorem MusicTheory.CyclicHuddling.sum_lt_of_strict_threshold {α : Type u_1} [DecidableEq α] (score : α → ℝ) (A B : Finset α) (c : ℝ) (hcard : B.card = A.card) (hin : ∀ x ∈ A, c < score x) (hout : ∀ x ∉ A, score x ≤ c) (hne : B ≠ A) : ∑ x ∈ B, score x < ∑ x ∈ A, score x

Strict separation at the threshold makes the maximizer unique at its cardinality. The geometric equality analysis must account for boundary ties.

noncomputable def MusicTheory.CyclicHuddling.Ahat {N : ℕ} [NeZero N] (A : Finset (ZMod N)) (k : ZMod N) : ℂ

The unnormalized Fourier coefficient of a subset of ZMod N.

Equations

• MusicTheory.CyclicHuddling.Ahat A k = ∑ a ∈ A, ZMod.stdAddChar (-(a * k))

theorem MusicTheory.CyclicHuddling.Ahat_eq_dft {N : ℕ} [NeZero N] (A : Finset (ZMod N)) (k : ZMod N) : Ahat A k = ZMod.dft (fun (a : ZMod N) => if a ∈ A then 1 else 0) k

The set-sum convention is Mathlib's discrete Fourier transform of its zero-one indicator.

def MusicTheory.CyclicHuddling.tpose {N : ℕ} (s : ZMod N) (A : Finset (ZMod N)) : Finset (ZMod N)

Transpose a subset by one residue.

Equations

• MusicTheory.CyclicHuddling.tpose s A = Finset.map { toFun := fun (x : ZMod N) => x + s, inj' := ⋯ } A

theorem MusicTheory.CyclicHuddling.Ahat_zero {N : ℕ} [NeZero N] (A : Finset (ZMod N)) : Ahat A 0 = ↑A.card

The frequency-zero coefficient is the number of selected residues.

theorem MusicTheory.CyclicHuddling.norm_Ahat_le_card {N : ℕ} [NeZero N] (A : Finset (ZMod N)) (k : ZMod N) : ‖Ahat A k‖ ≤ ↑A.card

The elementary cardinality bound is valid at every frequency, including nonprimitive frequencies where the consecutive-arc extremal bound fails.

theorem MusicTheory.CyclicHuddling.Ahat_tpose {N : ℕ} [NeZero N] (s : ZMod N) (A : Finset (ZMod N)) (k : ZMod N) : Ahat (tpose s A) k = ZMod.stdAddChar (-(s * k)) * Ahat A k

Translation changes only Fourier phase.

theorem MusicTheory.CyclicHuddling.norm_tpose {N : ℕ} [NeZero N] (s : ZMod N) (A : Finset (ZMod N)) (k : ZMod N) : ‖Ahat (tpose s A) k‖ = ‖Ahat A k‖

Translation preserves every Fourier magnitude.

theorem MusicTheory.CyclicHuddling.Ahat_unit_frequency {N : ℕ} [NeZero N] (A : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : Ahat A k = Ahat (Finset.image (fun (x : ZMod N) => x * k) A) 1

Multiplication by a unit relabels a primitive-frequency coefficient as a frequency-one coefficient of the relabeled set.

theorem MusicTheory.CyclicHuddling.card_image_mul_unit {N : ℕ} (A : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : (Finset.image (fun (x : ZMod N) => x * k) A).card = A.card

Relabeling by a unit preserves the set size.

theorem MusicTheory.CyclicHuddling.card_tpose {N : ℕ} (s : ZMod N) (A : Finset (ZMod N)) : (tpose s A).card = A.card

Translation preserves the number of selected residues.

theorem MusicTheory.CyclicHuddling.sum_character_eq_zero {N : ℕ} [NeZero N] {k : ZMod N} (hk : k ≠ 0) : ∑ a : ZMod N, ZMod.stdAddChar (-(a * k)) = 0

The complete character sum vanishes at nonzero frequency.

theorem MusicTheory.CyclicHuddling.Ahat_compl {N : ℕ} [NeZero N] {k : ZMod N} (hk : k ≠ 0) (A : Finset (ZMod N)) : Ahat Aᶜ k = -Ahat A k

Away from zero frequency, complementation reverses the Fourier coefficient.

def MusicTheory.CyclicHuddling.arc {N : ℕ} (m : ℕ) : Finset (ZMod N)

The first m residues, viewed as a cyclic arc.

Equations

• MusicTheory.CyclicHuddling.arc m = Finset.image (fun (j : ℕ) => ↑j) (Finset.range m)

theorem MusicTheory.CyclicHuddling.card_arc {N : ℕ} (m : ℕ) (hm : m ≤ N) : (arc m).card = m

In the natural range, an arc contains exactly m residues.

theorem MusicTheory.CyclicHuddling.Ahat_arc {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (k : ZMod N) : Ahat (arc m) k = ∑ j ∈ Finset.range m, ZMod.stdAddChar (-(↑j * k))

An arc coefficient is a consecutive character sum.

theorem MusicTheory.CyclicHuddling.Ahat_arc_geom {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (k : ZMod N) : Ahat (arc m) k = ∑ j ∈ Finset.range m, ZMod.stdAddChar (-k) ^ j

The cyclic arc has a geometric-series Fourier coefficient.

theorem MusicTheory.CyclicHuddling.Ahat_arc_mul_sub {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (k : ZMod N) : Ahat (arc m) k * (ZMod.stdAddChar (-k) - 1) = ZMod.stdAddChar (-k) ^ m - 1

The geometric-series identity for an arc, without dividing by a possibly vanishing denominator at frequency zero.

theorem MusicTheory.CyclicHuddling.re_amplitude_le_of_threshold {N : ℕ} [NeZero N] (u : ℂ) (k : ZMod N) (A B : Finset (ZMod N)) (c : ℝ) (hcard : B.card = A.card) (hin : ∀ a ∈ A, c ≤ (u * ZMod.stdAddChar (-(a * k))).re) (hout : ∀ a ∉ A, (u * ZMod.stdAddChar (-(a * k))).re ≤ c) : (u * Ahat B k).re ≤ (u * Ahat A k).re

The real projection of a Fourier coefficient is controlled by the finite top-score exchange lemma. A geometric description of the top-score sets of roots of unity is the remaining analytic step in Huddling.

theorem MusicTheory.CyclicHuddling.re_amplitude_lt_of_strict_threshold {N : ℕ} [NeZero N] (u : ℂ) (k : ZMod N) (A B : Finset (ZMod N)) (c : ℝ) (hcard : B.card = A.card) (hin : ∀ a ∈ A, c < (u * ZMod.stdAddChar (-(a * k))).re) (hout : ∀ a ∉ A, (u * ZMod.stdAddChar (-(a * k))).re ≤ c) (hne : B ≠ A) : (u * Ahat B k).re < (u * Ahat A k).re

Strictly separated projected scores give strict Fourier-projection inequality unless the chosen subset is the maximizing set itself.

theorem MusicTheory.CyclicHuddling.norm_Ahat_one_le_arc_of_geometric_selector {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (B : Finset (ZMod N)) (hcard : B.card = m) (hgeom : ∀ (u : ℂ), ‖u‖ = 1 → ∃ (s : ZMod N) (c : ℝ), (∀ a ∈ tpose s (arc m), c ≤ (u * ZMod.stdAddChar (-(a * 1))).re) ∧ ∀ a ∉ tpose s (arc m), (u * ZMod.stdAddChar (-(a * 1))).re ≤ c) : ‖Ahat B 1‖ ≤ ‖Ahat (arc m) 1‖

At frequency one, the full norm bound follows once each directional projection has a translated arc above a separating threshold. Other primitive frequencies require pulling the arc back by their inverse.

theorem MusicTheory.CyclicHuddling.norm_Ahat_unit_le_arc_of_geometric_selector {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (B : Finset (ZMod N)) (hcard : B.card = m) (k : ZMod N) (hk : IsUnit k) (hgeom : ∀ (u : ℂ), ‖u‖ = 1 → ∃ (s : ZMod N) (c : ℝ), (∀ a ∈ tpose s (arc m), c ≤ (u * ZMod.stdAddChar (-(a * 1))).re) ∧ ∀ a ∉ tpose s (arc m), (u * ZMod.stdAddChar (-(a * 1))).re ≤ c) : ‖Ahat B k‖ ≤ ‖Ahat (arc m) 1‖

The same geometric selector controls every primitive frequency after relabeling the selected pitches by multiplication by that frequency.