Chapter 3: Discrete Orthogonality Relations

The discrete orthogonality of roots of unity (Lemma~lem:discrete_orthogonality) has powerful consequences for sums of trigonometric functions evaluated at equally-spaced angles. We develop these consequences here.

Sums of cosines at rotated roots

The discrete orthogonality of roots of unity manifests geometrically: the projections of equally-spaced points on the circle always balance around the origin.

Lemma

For any \(N \geq 2\) and any \(\theta \in \R\),

\begin{equation}...\end{equation}

realProjectionsList_sum

(See Lemma 3.1 in \href{../paper/chebyshev_circles.pdf}{the paper})

Proof.

We use Euler's formula: \(\cos\theta = \Re(\e^{i\theta})\). Thus

\begin{equation}...\end{equation}

By Lemma~lem:discrete_orthogonality with \(m = 1\) (noting that \(N \nmid 1\) for \(N \geq 2\)), the inner sum vanishes. Hence the entire expression is zero.

Lemma

For any integers \(N \geq 1\), \(m\) with \(0 < m < N\), and any \(\theta \in \R\),

\begin{equation}...\end{equation}

(See Lemma 3.2 in \href{../paper/chebyshev_circles.pdf}{the paper})

Proof.

Using Euler's formula, \(\cos(m\theta) = \Re(\e^{im\theta})\), we have

\begin{equation}...\end{equation}

Since \(0 < m < N\), we have \(N \nmid m\), so the inner sum vanishes by Lemma~lem:discrete_orthogonality. cos_as_exp

Connection to discrete Fourier transform

The vanishing sums in Lemmas~lem:sum_cos_phi_vanishes and~lem:sum_cos_m_phi_vanishes reflect the orthogonality of the discrete Fourier basis. Define the discrete Fourier transform of a sequence \((a_0, \ldots, a_{N-1})\) as

\begin{equation}...\end{equation}

Our lemmas show that the constant sequence \(a_k = \e^{i\theta}\) (rotated unit phasor) has Fourier coefficients \(\hat{a}_m = 0\) for \(0 < m < N\) and \(\hat{a}_0 = N \e^{i\theta}\). This concentration of energy in the DC component (zero frequency) is characteristic of constant signals.

Similarly, for the sequence \(b_k = \e^{im(\theta + 2\pi k/N)}\) (complex exponential at frequency \(m\)), the projection onto the real axis (cosine) integrates to zero when summed uniformly over the roots of unity. This is the discrete analog of

\begin{equation}...\end{equation}

Chebyshev angle sums

The Chebyshev roots are located at angles \(\theta_k = (2k + 1)\pi/(2N)\). Unlike the equidistributed roots of unity, these angles carry a phase offset of \(\pi/(2N)\). Nevertheless, discrete orthogonality still forces their trigonometric sums to vanish.

Theorem 3.2.1
[blueprint]

For odd $m$ with $0 < |m| < 2N$, $\sum_{k=0}^{N-1} \cos\!\left(m \cdot \frac{(2k+1)\pi}{2N}\right) = 0$.

theorem sum_cos_chebyshev_angles_vanishes (N : ℕ) (m : ℤ) (hN : 0 < N)
    (hm : m ≠ 0) (hm_odd : Odd m) (hm_bound : |m| < 2 * N) :
    ∑ k ∈ range N, Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N)) = 0 := by
Proof ▼

Pair terms using the involution $k \mapsto N-1-k$. Since $\theta_k + \theta_{N-1-k} = \pi$ and $m$ is odd, $\cos(m\theta_{N-1-k}) = \cos(m(\pi - \theta_k)) = -\cos(m\theta_k)$. Each pair sums to zero, so the total sum vanishes.


  -- Define the term we're summing
  let f : ℕ → ℝ := fun k ↦ Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N))

  -- We'll show the sum vanishes by pairing terms using symmetry
  -- Key observation: θ_k + θ_{N-1-k} = (2k+1)π/(2N) + (2(N-1-k)+1)π/(2N) = π

  -- First, prove the pairing lemma: f(k) + f(N-1-k) = 0
  have pair_sum_zero : ∀ k ∈ range N, f k + f (N - 1 - k) = 0 := by
    intro k hk
    simp only [f]
    rw [mem_range] at hk
    have hk_le : k ≤ N - 1 := Nat.le_pred_of_lt hk

    -- First establish the cast identity for (N - 1 - k)
    have cast_eq : ((N - 1 - k) : ℝ) = N - 1 - k := by
      rfl

    -- The key insight: (2*(N-1-k)+1)*π/(2N) + (2*k+1)*π/(2N) = π
    -- So cos(m * first_angle) = cos(m*(π - second_angle)) = (-1)^m * cos(m*second_angle)

    -- Simplify the angle for N-1-k
    have angle_identity : (2 * (N - 1 - k : ℝ) + 1) * π /
      (2 * N) + (2 * k + 1) * π / (2 * N) = π := by
      have h2N_ne : (2 * N : ℝ) ≠ 0 := by
        have : (0 : ℝ) < N := Nat.cast_pos.mpr hN
        linarith
      rw [← add_div, ← add_mul]
      -- Show the sum of coefficients equals 2N
      have coeff_sum : 2 * (N - 1 - k : ℝ) + 1 + (2 * k + 1) = 2 * N := by
        have : (2 * (N - 1 - k) + 1 : ℕ) + (2 * k + 1) = 2 * N := by omega
        linarith
      rw [coeff_sum]
      field_simp

    -- Rewrite second angle as π minus first angle
    have second_angle : (2 * (N - 1 - k : ℝ) + 1) * π / (2 * N) =
      π - (2 * k + 1) * π / (2 * N) := by
      linarith [angle_identity]

    -- Substitute and use cosine identity
    -- Need to show the second cosine argument can be rewritten
    have key : m * (2 * ((N - 1 - k) : ℝ) + 1) * π / (2 * N) =
      m * (π - (2 * k + 1) * π / (2 * N)) := by
      calc m * (2 * (N - 1 - k : ℝ) + 1) * π / (2 * N)
          = m * ((2 * (N - 1 - k : ℝ) + 1) * π / (2 * N)) := by ring
        _ = m * (π - (2 * k + 1) * π / (2 * N)) := by rw [second_angle]

    -- Rewrite the goal to use the same casting as key
    have cast_adjust : (2 * ↑(N - 1 - k) + 1 : ℝ) = 2 * (↑N - 1 - ↑k) + 1 := by
      congr 1
      have : k ≤ N - 1 := hk_le
      rw [Nat.cast_sub this, Nat.cast_sub (Nat.one_le_of_lt hN)]
      simp
    rw [cast_adjust, key, mul_sub, Real.cos_int_mul_pi_sub]

    -- For odd m, (-1)^m = -1
    have neg_one_pow : (-1 : ℝ) ^ m = -1 := by
      obtain ⟨k, rfl⟩ := hm_odd
      rw [zpow_add₀ (by norm_num : (-1 : ℝ) ≠ 0)]
      rw [zpow_mul, zpow_ofNat]
      norm_num

    rw [neg_one_pow]
    ring_nf

  -- Apply the sum involution: terms pair up and cancel
  -- We use the fact that g(k) = N-1-k is an involution and f(k) + f(g(k)) = 0

  -- The sum equals its own negation, hence it must be zero
  suffices h : ∑ k ∈ range N, f k = -∑ k ∈ range N, f k by
    linarith [h]

  -- Reindex the sum using the involution k ↦ N - 1 - k
  rw [← Finset.sum_neg_distrib]
  refine Finset.sum_bij (fun k _ => N - 1 - k) ?_ ?_ ?_ ?_
  · -- Prove ∀ k ∈ range N, N - 1 - k ∈ range N
    intro k hk
    simp [mem_range] at hk ⊢
    omega
  · -- Prove injectivity
    intro a₁ ha₁ a₂ ha₂ heq
    simp only at heq
    have h1 : a₁ < N := by simp [mem_range] at ha₁; exact ha₁
    have h2 : a₂ < N := by simp [mem_range] at ha₂; exact ha₂
    -- N - 1 - a₁ = N - 1 - a₂ implies a₁ = a₂
    omega
  · -- Prove surjectivity
    intro b hb
    use N - 1 - b
    refine ⟨?_, ?_⟩
    · simp [mem_range] at hb ⊢
      have : b < N := hb
      omega
    · simp only
      have : b < N := by simp [mem_range] at hb; exact hb
      omega
  · -- Prove ∀ k ∈ range N, -f k = f (N - 1 - k)
    intro k hk
    have := pair_sum_zero k hk
    linarith
Theorem 3.2.2
[blueprint]

For even $m$ with $0 < m < N$, $\sum_{k=0}^{N-1} \cos\!\left(m \cdot \frac{(2k+1)\pi}{2N}\right) = 0$.

theorem sum_cos_chebyshev_angles_even_vanishes (N m : ℕ)
    (hN : 0 < N) (hm : 0 < m) (hm_even : Even m) (hm_bound : m < N) :
    ∑ k ∈ range N, Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N)) = 0 := by
Proof ▼

Write $m = 2s$, convert to complex exponentials, factor out the common phase $e^{is\pi/N}$, and recognize the remaining sum as $\sum_{k=0}^{N-1} \omega^{sk}$ where $\omega = e^{2\pi i/N}$ is a primitive $N$-th root. Since $0 < s < N$, the geometric sum vanishes by discrete orthogonality.


  -- Extract s from m = 2s
  obtain ⟨s, hs⟩ := hm_even
  rw [hs]

  -- Bound on s
  have hs_pos : 0 < s := by omega
  have hs_bound : s < N := by omega

  -- First convert s + s to 2 * s
  conv_lhs => arg 2; ext k; arg 1; rw [show (s + s : ℕ) = 2 * s by omega]

  -- Push down the cast and simplify
  conv_lhs => arg 2; ext k; arg 1; rw [show ((2 * s : ℕ) : ℝ) = 2 * (s : ℝ) by norm_cast]

  -- Simplify 2s * (2k+1) * π / (2N) = s * (2k+1) * π / N
  conv_lhs => arg 2; ext k; arg 1; rw [show (2 * (s : ℝ)) * (2 * k + 1 : ℝ) * π / (2 * N) =
      (s : ℝ) * (2 * k + 1 : ℝ) * π / N by field_simp]

  -- Now prove: ∑ k, cos(s*(2k+1)*π/N) = 0 using complex exponentials
  -- First prove the complex exponential sum is zero
  have geom_sum_zero : ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) = 0 := by
    -- Let ω = exp(2πi/N), primitive N-th root
    let ω := Complex.exp (2 * π * Complex.I / N)
    have ω_prim : IsPrimitiveRoot ω N := Complex.isPrimitiveRoot_exp N (by omega)

    -- Rewrite as sum of powers of ω^s
    have h_rewrite : ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) =
        ∑ k ∈ range N, ω ^ (s * k) := by
      refine Finset.sum_congr rfl fun k _ => ?_
      rw [← Complex.exp_nat_mul]
    rw [h_rewrite]

    conv_lhs =>
      arg 2
      ext k
      rw [pow_mul]

    -- Show ω^s ≠ 1
    have ωs_ne_one : ω ^ s ≠ 1 := by
      intro h_eq
      have h_div : N ∣ s := (ω_prim.pow_eq_one_iff_dvd s).mp h_eq
      have : N ≤ s := Nat.le_of_dvd hs_pos h_div
      omega

    -- Show (ω^s)^N = 1
    have ωs_pow_N : (ω ^ s) ^ N = 1 := by
      rw [← pow_mul, mul_comm, pow_mul, ω_prim.pow_eq_one, one_pow]

    -- Geometric sum
    have h_geom : (ω ^ s - 1) * ∑ k ∈ range N, (ω ^ s) ^ k = (ω ^ s) ^ N - 1 :=
      mul_geom_sum (ω ^ s) N
    rw [ωs_pow_N] at h_geom
    have : (ω ^ s - 1) * ∑ k ∈ range N, (ω ^ s) ^ k = 0 := by
      rw [h_geom]; ring
    exact eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne ωs_ne_one) this

  have complex_sum :
      ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N)) = 0 := by
    -- Factor: s*(2k+1)*π/N = s*π/N + s*2k*π/N
    calc ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N))
        = ∑ k ∈ range N, Complex.exp (Complex.I * (s : ℝ) * π / N) *
            Complex.exp (Complex.I * ((s : ℝ) * (2 * k) * π / N)) := by
          refine Finset.sum_congr rfl fun k _ => ?_
          rw [← Complex.exp_add]
          congr 1
          push_cast
          ring
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) *
            ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k) * π / N)) := by
          rw [Finset.mul_sum]
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) *
            ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) := by
          congr 2
          funext k
          congr 1
          push_cast
          ring
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) * 0 := by rw [geom_sum_zero]
      _ = 0 := by simp

  -- Convert cosine to exponential and use complex_sum
  have cos_eq : ∀ k : ℕ, Real.cos ((s : ℝ) * (2 * k + 1) * π / N) =
      (Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N))).re := by
    intro k
    have h1 : (Complex.I * (((s : ℝ) * (2 * k + 1) * π / N) : ℂ)) =
        ((((s : ℝ) * (2 * k + 1) * π / N) : ℝ) : ℂ) * Complex.I := by
      push_cast
      ring
    rw [show (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N) : ℂ) =
        Complex.I * (((s : ℝ) * (2 * k + 1) * π / N) : ℂ) by push_cast; rfl]
    rw [h1]
    exact (Complex.exp_ofReal_mul_I_re _).symm

  simp_rw [cos_eq]
  rw [← Complex.re_sum, complex_sum]
  simp

Geometric interpretation

The vanishing of these angle sums has a simple geometric interpretation. The angles \((2k+1)\pi/(2N)\) for \(k = 0, \ldots, N-1\) correspond to equally-spaced points on the upper half of the unit circle (when \(N\) is even, they avoid the points \(\pm 1\)). Their symmetry about the imaginary axis ensures that horizontal projections cancel. This is precisely the discrete analog of the orthogonality integral \(\int_0^\pi \cos(m\theta) \, d\theta = 0\) for \(m > 0\).

3.1 Sums of cosines at rotated roots

The discrete orthogonality of roots of unity manifests geometrically: the projections of equally-spaced points on the circle always balance around the origin.

Lemma

For any \(N \geq 2\) and any \(\theta \in \R\),

\begin{equation}...\end{equation}

realProjectionsList_sum

(See Lemma 3.1 in \href{../paper/chebyshev_circles.pdf}{the paper})

Proof.

We use Euler's formula: \(\cos\theta = \Re(\e^{i\theta})\). Thus

\begin{equation}...\end{equation}

By Lemma~lem:discrete_orthogonality with \(m = 1\) (noting that \(N \nmid 1\) for \(N \geq 2\)), the inner sum vanishes. Hence the entire expression is zero.

Lemma

For any integers \(N \geq 1\), \(m\) with \(0 < m < N\), and any \(\theta \in \R\),

\begin{equation}...\end{equation}

(See Lemma 3.2 in \href{../paper/chebyshev_circles.pdf}{the paper})

Proof.

Using Euler's formula, \(\cos(m\theta) = \Re(\e^{im\theta})\), we have

\begin{equation}...\end{equation}

Since \(0 < m < N\), we have \(N \nmid m\), so the inner sum vanishes by Lemma~lem:discrete_orthogonality. cos_as_exp

Connection to discrete Fourier transform

The vanishing sums in Lemmas~lem:sum_cos_phi_vanishes and~lem:sum_cos_m_phi_vanishes reflect the orthogonality of the discrete Fourier basis. Define the discrete Fourier transform of a sequence \((a_0, \ldots, a_{N-1})\) as

\begin{equation}...\end{equation}

Our lemmas show that the constant sequence \(a_k = \e^{i\theta}\) (rotated unit phasor) has Fourier coefficients \(\hat{a}_m = 0\) for \(0 < m < N\) and \(\hat{a}_0 = N \e^{i\theta}\). This concentration of energy in the DC component (zero frequency) is characteristic of constant signals.

Similarly, for the sequence \(b_k = \e^{im(\theta + 2\pi k/N)}\) (complex exponential at frequency \(m\)), the projection onto the real axis (cosine) integrates to zero when summed uniformly over the roots of unity. This is the discrete analog of

\begin{equation}...\end{equation}

3.2 Chebyshev angle sums

The Chebyshev roots are located at angles \(\theta_k = (2k + 1)\pi/(2N)\). Unlike the equidistributed roots of unity, these angles carry a phase offset of \(\pi/(2N)\). Nevertheless, discrete orthogonality still forces their trigonometric sums to vanish.

Theorem 3.2.1
[blueprint]

For odd $m$ with $0 < |m| < 2N$, $\sum_{k=0}^{N-1} \cos\!\left(m \cdot \frac{(2k+1)\pi}{2N}\right) = 0$.

theorem sum_cos_chebyshev_angles_vanishes (N : ℕ) (m : ℤ) (hN : 0 < N)
    (hm : m ≠ 0) (hm_odd : Odd m) (hm_bound : |m| < 2 * N) :
    ∑ k ∈ range N, Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N)) = 0 := by
Proof ▼

Pair terms using the involution $k \mapsto N-1-k$. Since $\theta_k + \theta_{N-1-k} = \pi$ and $m$ is odd, $\cos(m\theta_{N-1-k}) = \cos(m(\pi - \theta_k)) = -\cos(m\theta_k)$. Each pair sums to zero, so the total sum vanishes.


  -- Define the term we're summing
  let f : ℕ → ℝ := fun k ↦ Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N))

  -- We'll show the sum vanishes by pairing terms using symmetry
  -- Key observation: θ_k + θ_{N-1-k} = (2k+1)π/(2N) + (2(N-1-k)+1)π/(2N) = π

  -- First, prove the pairing lemma: f(k) + f(N-1-k) = 0
  have pair_sum_zero : ∀ k ∈ range N, f k + f (N - 1 - k) = 0 := by
    intro k hk
    simp only [f]
    rw [mem_range] at hk
    have hk_le : k ≤ N - 1 := Nat.le_pred_of_lt hk

    -- First establish the cast identity for (N - 1 - k)
    have cast_eq : ((N - 1 - k) : ℝ) = N - 1 - k := by
      rfl

    -- The key insight: (2*(N-1-k)+1)*π/(2N) + (2*k+1)*π/(2N) = π
    -- So cos(m * first_angle) = cos(m*(π - second_angle)) = (-1)^m * cos(m*second_angle)

    -- Simplify the angle for N-1-k
    have angle_identity : (2 * (N - 1 - k : ℝ) + 1) * π /
      (2 * N) + (2 * k + 1) * π / (2 * N) = π := by
      have h2N_ne : (2 * N : ℝ) ≠ 0 := by
        have : (0 : ℝ) < N := Nat.cast_pos.mpr hN
        linarith
      rw [← add_div, ← add_mul]
      -- Show the sum of coefficients equals 2N
      have coeff_sum : 2 * (N - 1 - k : ℝ) + 1 + (2 * k + 1) = 2 * N := by
        have : (2 * (N - 1 - k) + 1 : ℕ) + (2 * k + 1) = 2 * N := by omega
        linarith
      rw [coeff_sum]
      field_simp

    -- Rewrite second angle as π minus first angle
    have second_angle : (2 * (N - 1 - k : ℝ) + 1) * π / (2 * N) =
      π - (2 * k + 1) * π / (2 * N) := by
      linarith [angle_identity]

    -- Substitute and use cosine identity
    -- Need to show the second cosine argument can be rewritten
    have key : m * (2 * ((N - 1 - k) : ℝ) + 1) * π / (2 * N) =
      m * (π - (2 * k + 1) * π / (2 * N)) := by
      calc m * (2 * (N - 1 - k : ℝ) + 1) * π / (2 * N)
          = m * ((2 * (N - 1 - k : ℝ) + 1) * π / (2 * N)) := by ring
        _ = m * (π - (2 * k + 1) * π / (2 * N)) := by rw [second_angle]

    -- Rewrite the goal to use the same casting as key
    have cast_adjust : (2 * ↑(N - 1 - k) + 1 : ℝ) = 2 * (↑N - 1 - ↑k) + 1 := by
      congr 1
      have : k ≤ N - 1 := hk_le
      rw [Nat.cast_sub this, Nat.cast_sub (Nat.one_le_of_lt hN)]
      simp
    rw [cast_adjust, key, mul_sub, Real.cos_int_mul_pi_sub]

    -- For odd m, (-1)^m = -1
    have neg_one_pow : (-1 : ℝ) ^ m = -1 := by
      obtain ⟨k, rfl⟩ := hm_odd
      rw [zpow_add₀ (by norm_num : (-1 : ℝ) ≠ 0)]
      rw [zpow_mul, zpow_ofNat]
      norm_num

    rw [neg_one_pow]
    ring_nf

  -- Apply the sum involution: terms pair up and cancel
  -- We use the fact that g(k) = N-1-k is an involution and f(k) + f(g(k)) = 0

  -- The sum equals its own negation, hence it must be zero
  suffices h : ∑ k ∈ range N, f k = -∑ k ∈ range N, f k by
    linarith [h]

  -- Reindex the sum using the involution k ↦ N - 1 - k
  rw [← Finset.sum_neg_distrib]
  refine Finset.sum_bij (fun k _ => N - 1 - k) ?_ ?_ ?_ ?_
  · -- Prove ∀ k ∈ range N, N - 1 - k ∈ range N
    intro k hk
    simp [mem_range] at hk ⊢
    omega
  · -- Prove injectivity
    intro a₁ ha₁ a₂ ha₂ heq
    simp only at heq
    have h1 : a₁ < N := by simp [mem_range] at ha₁; exact ha₁
    have h2 : a₂ < N := by simp [mem_range] at ha₂; exact ha₂
    -- N - 1 - a₁ = N - 1 - a₂ implies a₁ = a₂
    omega
  · -- Prove surjectivity
    intro b hb
    use N - 1 - b
    refine ⟨?_, ?_⟩
    · simp [mem_range] at hb ⊢
      have : b < N := hb
      omega
    · simp only
      have : b < N := by simp [mem_range] at hb; exact hb
      omega
  · -- Prove ∀ k ∈ range N, -f k = f (N - 1 - k)
    intro k hk
    have := pair_sum_zero k hk
    linarith
Theorem 3.2.2
[blueprint]

For even $m$ with $0 < m < N$, $\sum_{k=0}^{N-1} \cos\!\left(m \cdot \frac{(2k+1)\pi}{2N}\right) = 0$.

theorem sum_cos_chebyshev_angles_even_vanishes (N m : ℕ)
    (hN : 0 < N) (hm : 0 < m) (hm_even : Even m) (hm_bound : m < N) :
    ∑ k ∈ range N, Real.cos (m * (2 * k + 1 : ℝ) * π / (2 * N)) = 0 := by
Proof ▼

Write $m = 2s$, convert to complex exponentials, factor out the common phase $e^{is\pi/N}$, and recognize the remaining sum as $\sum_{k=0}^{N-1} \omega^{sk}$ where $\omega = e^{2\pi i/N}$ is a primitive $N$-th root. Since $0 < s < N$, the geometric sum vanishes by discrete orthogonality.


  -- Extract s from m = 2s
  obtain ⟨s, hs⟩ := hm_even
  rw [hs]

  -- Bound on s
  have hs_pos : 0 < s := by omega
  have hs_bound : s < N := by omega

  -- First convert s + s to 2 * s
  conv_lhs => arg 2; ext k; arg 1; rw [show (s + s : ℕ) = 2 * s by omega]

  -- Push down the cast and simplify
  conv_lhs => arg 2; ext k; arg 1; rw [show ((2 * s : ℕ) : ℝ) = 2 * (s : ℝ) by norm_cast]

  -- Simplify 2s * (2k+1) * π / (2N) = s * (2k+1) * π / N
  conv_lhs => arg 2; ext k; arg 1; rw [show (2 * (s : ℝ)) * (2 * k + 1 : ℝ) * π / (2 * N) =
      (s : ℝ) * (2 * k + 1 : ℝ) * π / N by field_simp]

  -- Now prove: ∑ k, cos(s*(2k+1)*π/N) = 0 using complex exponentials
  -- First prove the complex exponential sum is zero
  have geom_sum_zero : ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) = 0 := by
    -- Let ω = exp(2πi/N), primitive N-th root
    let ω := Complex.exp (2 * π * Complex.I / N)
    have ω_prim : IsPrimitiveRoot ω N := Complex.isPrimitiveRoot_exp N (by omega)

    -- Rewrite as sum of powers of ω^s
    have h_rewrite : ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) =
        ∑ k ∈ range N, ω ^ (s * k) := by
      refine Finset.sum_congr rfl fun k _ => ?_
      rw [← Complex.exp_nat_mul]
    rw [h_rewrite]

    conv_lhs =>
      arg 2
      ext k
      rw [pow_mul]

    -- Show ω^s ≠ 1
    have ωs_ne_one : ω ^ s ≠ 1 := by
      intro h_eq
      have h_div : N ∣ s := (ω_prim.pow_eq_one_iff_dvd s).mp h_eq
      have : N ≤ s := Nat.le_of_dvd hs_pos h_div
      omega

    -- Show (ω^s)^N = 1
    have ωs_pow_N : (ω ^ s) ^ N = 1 := by
      rw [← pow_mul, mul_comm, pow_mul, ω_prim.pow_eq_one, one_pow]

    -- Geometric sum
    have h_geom : (ω ^ s - 1) * ∑ k ∈ range N, (ω ^ s) ^ k = (ω ^ s) ^ N - 1 :=
      mul_geom_sum (ω ^ s) N
    rw [ωs_pow_N] at h_geom
    have : (ω ^ s - 1) * ∑ k ∈ range N, (ω ^ s) ^ k = 0 := by
      rw [h_geom]; ring
    exact eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne ωs_ne_one) this

  have complex_sum :
      ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N)) = 0 := by
    -- Factor: s*(2k+1)*π/N = s*π/N + s*2k*π/N
    calc ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N))
        = ∑ k ∈ range N, Complex.exp (Complex.I * (s : ℝ) * π / N) *
            Complex.exp (Complex.I * ((s : ℝ) * (2 * k) * π / N)) := by
          refine Finset.sum_congr rfl fun k _ => ?_
          rw [← Complex.exp_add]
          congr 1
          push_cast
          ring
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) *
            ∑ k ∈ range N, Complex.exp (Complex.I * ((s : ℝ) * (2 * k) * π / N)) := by
          rw [Finset.mul_sum]
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) *
            ∑ k ∈ range N, Complex.exp ((s * k : ℕ) * (2 * π * Complex.I / N)) := by
          congr 2
          funext k
          congr 1
          push_cast
          ring
      _ = Complex.exp (Complex.I * (s : ℝ) * π / N) * 0 := by rw [geom_sum_zero]
      _ = 0 := by simp

  -- Convert cosine to exponential and use complex_sum
  have cos_eq : ∀ k : ℕ, Real.cos ((s : ℝ) * (2 * k + 1) * π / N) =
      (Complex.exp (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N))).re := by
    intro k
    have h1 : (Complex.I * (((s : ℝ) * (2 * k + 1) * π / N) : ℂ)) =
        ((((s : ℝ) * (2 * k + 1) * π / N) : ℝ) : ℂ) * Complex.I := by
      push_cast
      ring
    rw [show (Complex.I * ((s : ℝ) * (2 * k + 1) * π / N) : ℂ) =
        Complex.I * (((s : ℝ) * (2 * k + 1) * π / N) : ℂ) by push_cast; rfl]
    rw [h1]
    exact (Complex.exp_ofReal_mul_I_re _).symm

  simp_rw [cos_eq]
  rw [← Complex.re_sum, complex_sum]
  simp

Geometric interpretation

The vanishing of these angle sums has a simple geometric interpretation. The angles \((2k+1)\pi/(2N)\) for \(k = 0, \ldots, N-1\) correspond to equally-spaced points on the upper half of the unit circle (when \(N\) is even, they avoid the points \(\pm 1\)). Their symmetry about the imaginary axis ensures that horizontal projections cancel. This is precisely the discrete analog of the orthogonality integral \(\int_0^\pi \cos(m\theta) \, d\theta = 0\) for \(m > 0\).