§4.2, side-note p. 37 — the eigenvalues e^{−2πik/n}, k = 0, …, n−1, of the shift S are distinct

Proved

GeomDL.Grids.shift_eigenvalues_distinct

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

eigenvaluegeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1roots-of-unityshift-operator

Let $n \ge 1$ . The eigenvalues $\lambda_k = e^{-2\pi i k/n}$ of the right shift $S$ on the Fourier basis vectors $\varphi_k$ , $k = 0, 1, \dots, n-1$ , are pairwise distinct: for $k, l \in \{0, \dots, n-1\}$ ,

e^{-2\pi i k/n} = e^{-2\pi i l/n} \;\Longrightarrow\; k = l .

The book needs distinct eigenvalues so that the common eigenbasis of the commuting circulant matrices is determined by the shift alone; it states that the assumption "is satisfied with our choice of $S$ ".

Formalization Note $k$ and $l$ are elements of ZMod n, entering the exponent through ZMod.val. Together with the eigenvector statement for $\varphi_k$ this says that $S$ has $n$ distinct eigenvalues.

Preamble

import Mathlib
import Definitions.Def_GeomDL_Grids_Defs

open Matrix

Formal statement

namespace GeomDL.Grids
/-- Bronstein et al. §4.2, side-note p. 37: the shift `S` has distinct eigenvalues. The eigenvalues
`λ_k = e^{-2πik/n}`, `k = 0, …, n-1`, of `S` on the Fourier basis are pairwise distinct. -/
theorem shift_eigenvalues_distinct {n : ℕ} [NeZero n] (k l : ZMod n)
    (hkl : Complex.exp (-(2 * (Real.pi : ℂ) * Complex.I * (k.val : ℂ) / (n : ℂ))) =
      Complex.exp (-(2 * (Real.pi : ℂ) * Complex.I * (l.val : ℂ) / (n : ℂ)))) :
    k = l := by sorry
end GeomDL.Grids

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.2, side-note p. 37, "We must additionally assume distinct eigenvalues … This assumption is satisfied with our choice of S."

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph