The Huddling inequality for every cyclic group

For every N ≠ 0 and B ⊆ ZMod N, ‖Ahat B 1‖ ≤ ‖Ahat (arc #B) 1‖, where arc m = {0, …, m - 1}, with equality exactly for the translates of arc #B. The proof cuts the circle at the boundary of an arc selected by the phase of Ahat B 1, and uses the monotonicity of the cosine. Both statements transfer to every unit frequency.

Main results

• geometric_selector.
• norm_Ahat_one_le_arc, norm_Ahat_unit_le_arc.
• norm_Ahat_one_eq_arc_iff, norm_Ahat_unit_eq_arc_iff, maximizer_unit_iff.

References

• E. Amiot, Discrete Fourier transform and Bach's good temperament, Music Theory Online 15 (2009), Lemma 2.
• 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.threshold_eq_on_diff {α : 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) (hsum : ∑ x ∈ B, score x = ∑ x ∈ A, score x) : (∀ x ∈ A \ B, score x = c) ∧ ∀ x ∈ B \ A, score x = c

theorem MusicTheory.CyclicHuddling.eq_or_swap_of_diff_subset {α : Type u_1} [DecidableEq α] (A B : Finset α) (a b : α) (hcard : B.card = A.card) (ha : A \ B ⊆ {a}) (hb : B \ A ⊆ {b}) : B = A ∨ B = insert b (A.erase a)

theorem MusicTheory.CyclicHuddling.cos_ge_of_between {x t : ℝ} (ht : t ≤ Real.pi) (hx₁ : -t ≤ x) (hx₂ : x ≤ t) : Real.cos t ≤ Real.cos x

theorem MusicTheory.CyclicHuddling.cos_gt_of_between {x t : ℝ} (ht : t ≤ Real.pi) (hx₁ : -t < x) (hx₂ : x < t) : Real.cos t < Real.cos x

theorem MusicTheory.CyclicHuddling.cos_le_of_between {x t : ℝ} (ht₀ : 0 ≤ t) (hx₁ : t ≤ x) (hx₂ : x ≤ 2 * Real.pi - t) : Real.cos x ≤ Real.cos t

theorem MusicTheory.CyclicHuddling.cos_lt_of_between {x t : ℝ} (ht₀ : 0 ≤ t) (hx₁ : t < x) (hx₂ : x < 2 * Real.pi - t) : Real.cos x < Real.cos t

theorem MusicTheory.CyclicHuddling.exists_grid_cut_strict (θ t h : ℝ) (hh : 0 < h) : ∃ (s : ℤ), t - h < θ - h * ↑s ∧ θ - h * ↑s ≤ t

A rotated grid always has a cut with residual angle in a prescribed cell.

theorem MusicTheory.CyclicHuddling.exists_grid_cut (θ t h : ℝ) (hh : 0 < h) : ∃ (s : ℤ), t - h ≤ θ - h * ↑s ∧ θ - h * ↑s ≤ t

theorem MusicTheory.CyclicHuddling.grid_projection_inside (N m j : ℕ) (hm : m ≤ N) (hj : j < m) (h β : ℝ) (hh : 0 < h) (hperiod : h * ↑N = 2 * Real.pi) (hβ₁ : h * ↑m / 2 - h ≤ β) (hβ₂ : β ≤ h * ↑m / 2) : Real.cos (h * ↑m / 2) ≤ Real.cos (β - h * ↑j)

theorem MusicTheory.CyclicHuddling.grid_projection_outside (N m j : ℕ) (hj₁ : m ≤ j) (hj₂ : j < N) (h β : ℝ) (hh : 0 < h) (hperiod : h * ↑N = 2 * Real.pi) (hβ₁ : h * ↑m / 2 - h ≤ β) (hβ₂ : β ≤ h * ↑m / 2) : Real.cos (β - h * ↑j) ≤ Real.cos (h * ↑m / 2)

theorem MusicTheory.CyclicHuddling.grid_projection_inside_strict (N m j : ℕ) (hm : m ≤ N) (hj₀ : 0 < j) (hj : j < m) (h β : ℝ) (hh : 0 < h) (hperiod : h * ↑N = 2 * Real.pi) (hβ₁ : h * ↑m / 2 - h < β) (hβ₂ : β ≤ h * ↑m / 2) : Real.cos (h * ↑m / 2) < Real.cos (β - h * ↑j)

theorem MusicTheory.CyclicHuddling.grid_projection_outside_strict (N m j : ℕ) (hj₁ : m < j) (hj₂ : j < N) (h β : ℝ) (hh : 0 < h) (hperiod : h * ↑N = 2 * Real.pi) (hβ₁ : h * ↑m / 2 - h < β) (hβ₂ : β ≤ h * ↑m / 2) : Real.cos (β - h * ↑j) < Real.cos (h * ↑m / 2)

theorem MusicTheory.CyclicHuddling.re_exp_mul_character {N : ℕ} [NeZero N] (θ : ℝ) (j : ℤ) : (Complex.exp (↑θ * Complex.I) * ZMod.stdAddChar (-↑j)).re = Real.cos (θ - 2 * Real.pi / ↑N * ↑j)

theorem MusicTheory.CyclicHuddling.mem_tpose_arc_iff {N : ℕ} (s a : ZMod N) (m : ℕ) : a ∈ tpose s (arc m) ↔ ∃ j < m, ↑j + s = a

theorem MusicTheory.CyclicHuddling.arc_swap_endpoint {N : ℕ} (s : ZMod N) (m : ℕ) (hm₀ : 0 < m) (hmN : m < N) : insert (↑m + s) ((tpose s (arc m)).erase s) = tpose (s + 1) (arc m)

theorem MusicTheory.CyclicHuddling.geometric_selector_with_boundary {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (u : ℂ) (hu : ‖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) ∧ (∀ a ∈ tpose s (arc m), a ≠ s → c < (u * ZMod.stdAddChar (-(a * 1))).re) ∧ ∀ a ∉ tpose s (arc m), a ≠ ↑m + s → (u * ZMod.stdAddChar (-(a * 1))).re < c

In any direction the regular polygon has a consecutive block of m vertices separated from the others by a projection threshold.

theorem MusicTheory.CyclicHuddling.geometric_selector {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) (u : ℂ) (hu : ‖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

theorem MusicTheory.CyclicHuddling.norm_Ahat_one_le_arc {N : ℕ} [NeZero N] (B : Finset (ZMod N)) : ‖Ahat B 1‖ ≤ ‖Ahat (arc B.card) 1‖

The Huddling inequality for an arbitrary nonzero cyclic order.

theorem MusicTheory.CyclicHuddling.norm_Ahat_unit_le_arc {N : ℕ} [NeZero N] (B : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : ‖Ahat B k‖ ≤ ‖Ahat (arc B.card) 1‖

Huddling at any primitive frequency, with the same frequency-one bound.

theorem MusicTheory.CyclicHuddling.eq_tpose_arc_of_norm_eq {N : ℕ} [NeZero N] (B : Finset (ZMod N)) (hm₀ : 0 < B.card) (hmN : B.card < N) (heq : ‖Ahat B 1‖ = ‖Ahat (arc B.card) 1‖) : ∃ (s : ZMod N), B = tpose s (arc B.card)

theorem MusicTheory.CyclicHuddling.norm_Ahat_one_eq_arc_iff {N : ℕ} [NeZero N] (B : Finset (ZMod N)) : ‖Ahat B 1‖ = ‖Ahat (arc B.card) 1‖ ↔ ∃ (s : ZMod N), B = tpose s (arc B.card)

Equality in Huddling holds exactly for a consecutive arc, including the empty and full sets. Boundary ties allow the adjacent arc and no other set.

theorem MusicTheory.CyclicHuddling.norm_Ahat_unit_eq_arc_iff {N : ℕ} [NeZero N] (B : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : ‖Ahat B k‖ = ‖Ahat (arc B.card) 1‖ ↔ ∃ (s : ZMod N), Finset.image (fun (x : ZMod N) => x * k) B = tpose s (arc B.card)

At a primitive frequency, equality holds precisely when multiplication by that frequency sends the pitch set to a consecutive arc.

theorem MusicTheory.CyclicHuddling.maximizer_unit_iff {N : ℕ} [NeZero N] (B : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : (∀ (C : Finset (ZMod N)), C.card = B.card → ‖Ahat C k‖ ≤ ‖Ahat B k‖) ↔ ∃ (s : ZMod N), Finset.image (fun (x : ZMod N) => x * k) B = tpose s (arc B.card)

The extremal formulation: a set maximizes the primitive Fourier magnitude among sets of its cardinality exactly when its frequency image is an arc.