Chapter 4: Power Sum Invariance

We now prove that the power sums of the rotated projections $r_k(\theta) = \cos(\theta + 2\pi k/N)$ are independent of $\theta$. This remarkable invariance is the heart of our main theorem: it shows that rotating the configuration does not change the polynomial (except for the constant term).

Strategy via binomial expansion

The key technique is to expand $\cos^j(\theta + 2\pi k/N)$ using Euler's formula:

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

Raising to the $j$-th power and expanding binomially yields

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

Summing over $k = 0, \ldots, N-1$ with $\theta = \theta + 2\pi k/N$, each term with $j - 2\ell \not\equiv 0 \pmod{N}$ contributes zero by discrete orthogonality (Lemma~lem:sum_cos_m_phi_vanishes). Only the term with $j - 2\ell \equiv 0 \pmod{N}$ survives, and this term is independent of $\theta$.

Computational examples

Before proving the general case, we illustrate the invariance with explicit calculations for small values.

Example: $N = 3$, $j = 2$

For $N = 3$ and $j = 2$, the power sum is

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

Using $\cos^2\theta = (1 + \cos(2\theta))/2$:

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

The sum vanishes by Lemma~lem:sum_cos_m_phi_vanishes (with $m = 2 < N = 3$), giving $S_2(\theta) = 3/2$ for all $\theta$.

Example: $N = 4$, $j = 3$

For $N = 4$ and $j = 3$:

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

Using the identity $\cos^3\theta = \frac{3\cos\theta + \cos(3\theta)}{4}$: cos_cube_formula

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

Both sums vanish (first sum by Lemma~lem:sum_cos_phi_vanishes, second sum by Lemma~lem:sum_cos_m_phi_vanishes with $m = 3 < N = 4$), giving $S_3(\theta) = 0$ for all $\theta$.

Example: $N = 5$, $j = 2$

For $N = 5$ and $j = 2$:

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

The trigonometric sum vanishes since $m = 2 < N = 5$.

General power sum invariance

We now prove that the power sums of the rotated projections $r_k(\theta) = \cos(\theta + 2\pi k/N)$ are independent of $\theta$. This remarkable invariance is the heart of our main theorem: it shows that rotating the configuration does not change the polynomial (except for the constant term).

Theorem 4.3.1

[blueprint]

For any integers $N \ge 1$, $j$ with $1 \le j < N$, and any $\theta \in \mathbb{R}$, $\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta + \frac{2\pi k}{N}\bigr)$ is independent of $\theta$.

theorem powerSumCos_invariant (N : ℕ) (j : ℕ) (θ₁ θ₂ : ℝ)
    (hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
    ∑ k ∈ Finset.range N, (Real.cos (θ₁ + 2 * π * k / N)) ^ j =
    ∑ k ∈ Finset.range N, (Real.cos (θ₂ + 2 * π * k / N)) ^ j := by

Proof ▼

For $j = 1$ this is the vanishing cosine sum. For $j \ge 2$, apply the binomial expansion strategy: expand $\cos^j$ via Euler's formula, sum over the roots of unity, and observe that discrete orthogonality kills every $\theta$-dependent term.


  match j with
  | 0 => omega  -- Contradicts hj
  | 1 =>
    -- j = 1: sum of cosines at N equally spaced angles = 0
    simp only [pow_one]
    have hN2 : 2 ≤ N := by omega
    rw [sum_cos_roots_of_unity N θ₁ hN2, sum_cos_roots_of_unity N θ₂ hN2]
  | j' + 2 =>
    -- j ≥ 2: use the general binomial expansion theorem
    exact sum_cos_pow_theta_independent N (j' + 2) θ₁ θ₂ hN (by omega) hj'

The formalization establishes this for small values of $j$ explicitly ($j = 2, 3, 4, 5, 6$) and then proves the general case using the binomial argument above.

The formalization establishes this for small values of $j$ explicitly ($j = 2, 3, 4, 5, 6$) and then proves the general case using the binomial argument above. sum_pow_primitive_root_mul, sum_primitive_root_pow_mul

4.1 Strategy via binomial expansion

The key technique is to expand $\cos^j(\theta + 2\pi k/N)$ using Euler's formula:

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

Raising to the $j$-th power and expanding binomially yields

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

4.2 Computational examples

Before proving the general case, we illustrate the invariance with explicit calculations for small values.

Example: $N = 3$, $j = 2$

For $N = 3$ and $j = 2$, the power sum is

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

Using $\cos^2\theta = (1 + \cos(2\theta))/2$:

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

The sum vanishes by Lemma~lem:sum_cos_m_phi_vanishes (with $m = 2 < N = 3$), giving $S_2(\theta) = 3/2$ for all $\theta$.

Example: $N = 4$, $j = 3$

For $N = 4$ and $j = 3$:

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

Using the identity $\cos^3\theta = \frac{3\cos\theta + \cos(3\theta)}{4}$: cos_cube_formula

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

Both sums vanish (first sum by Lemma~lem:sum_cos_phi_vanishes, second sum by Lemma~lem:sum_cos_m_phi_vanishes with $m = 3 < N = 4$), giving $S_3(\theta) = 0$ for all $\theta$.

Example: $N = 5$, $j = 2$

For $N = 5$ and $j = 2$:

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

The trigonometric sum vanishes since $m = 2 < N = 5$.

4.3 General power sum invariance

Theorem 4.3.1

[blueprint]

For any integers $N \ge 1$, $j$ with $1 \le j < N$, and any $\theta \in \mathbb{R}$, $\sum_{k=0}^{N-1} \cos^j\!\bigl(\theta + \frac{2\pi k}{N}\bigr)$ is independent of $\theta$.

theorem powerSumCos_invariant (N : ℕ) (j : ℕ) (θ₁ θ₂ : ℝ)
    (hN : 0 < N) (hj : 0 < j) (hj' : j < N) :
    ∑ k ∈ Finset.range N, (Real.cos (θ₁ + 2 * π * k / N)) ^ j =
    ∑ k ∈ Finset.range N, (Real.cos (θ₂ + 2 * π * k / N)) ^ j := by

Proof ▼


  match j with
  | 0 => omega  -- Contradicts hj
  | 1 =>
    -- j = 1: sum of cosines at N equally spaced angles = 0
    simp only [pow_one]
    have hN2 : 2 ≤ N := by omega
    rw [sum_cos_roots_of_unity N θ₁ hN2, sum_cos_roots_of_unity N θ₂ hN2]
  | j' + 2 =>
    -- j ≥ 2: use the general binomial expansion theorem
    exact sum_cos_pow_theta_independent N (j' + 2) θ₁ θ₂ hN (by omega) hj'

The formalization establishes this for small values of $j$ explicitly ($j = 2, 3, 4, 5, 6$) and then proves the general case using the binomial argument above.