Odd Chebyshev Angle 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