The Huddling constant in closed form

From Euler's formula and the chord length ‖exp (I * x) - 1‖ = ‖2 sin (x / 2)‖, the arc of m consecutive classes in ZMod N, 1 < N, has ‖Ahat (arc m) 1‖ = sin (π m / N) / sin (π / N). This gives the sharp bound for every unit frequency, its equality case, and the symmetry m ↔ N - m.

Main results

• norm_Ahat_arc_sine_ratio.
• norm_Ahat_unit_le_sine_ratio, norm_Ahat_unit_eq_sine_ratio_iff.
• sine_ratio_complement.

References

• 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.character_neg_nat_exp {N : ℕ} [NeZero N] (m : ℕ) : ZMod.stdAddChar (-↑m) = Complex.exp (Complex.I * ↑(-(2 * Real.pi * ↑m / ↑N)))

A cyclic character value is Euler's exponential at its negative angle.

theorem MusicTheory.CyclicHuddling.norm_character_neg_nat_sub_one {N : ℕ} [NeZero N] (m : ℕ) : ‖ZMod.stdAddChar (-↑m) - 1‖ = 2 * |Real.sin (Real.pi * ↑m / ↑N)|

Euler's chord-length formula at an Nth root of unity.

theorem MusicTheory.CyclicHuddling.norm_Ahat_arc_sine_ratio {N : ℕ} [NeZero N] (hN : 1 < N) (m : ℕ) (hm : m ≤ N) : ‖Ahat (arc m) 1‖ = Real.sin (Real.pi * ↑m / ↑N) / Real.sin (Real.pi / ↑N)

The exact Fourier magnitude of a consecutive cyclic arc.

theorem MusicTheory.CyclicHuddling.norm_Ahat_unit_le_sine_ratio {N : ℕ} [NeZero N] (hN : 1 < N) (B : Finset (ZMod N)) (k : ZMod N) (hk : IsUnit k) : ‖Ahat B k‖ ≤ Real.sin (Real.pi * ↑B.card / ↑N) / Real.sin (Real.pi / ↑N)

Huddling with its explicit sine-ratio constant at every primitive frequency.

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

Equality in the sine-ratio bound is exactly the frequency-image arc condition.

theorem MusicTheory.CyclicHuddling.sine_ratio_complement {N : ℕ} [NeZero N] (m : ℕ) (hm : m ≤ N) : Real.sin (Real.pi * ↑(N - m) / ↑N) / Real.sin (Real.pi / ↑N) = Real.sin (Real.pi * ↑m / ↑N) / Real.sin (Real.pi / ↑N)

Complementary cardinalities have the same sine-ratio bound.