§4.2, side-note p. 37 — the left shift is Sᵀ, and S is orthogonal: SᵀS = SSᵀ = I

Proved

GeomDL.Grids.shift_orthogonal

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

geometric-deep-learningorthogonal-matrixp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1shift-operator

Let $n \ge 1$ , let $R$ be a commutative ring and let $S$ be the right shift on $\mathbb Z_n$ . Its transpose is the left shift,

(S^\top x)_u = x_{u+1 \bmod n} \qquad \text{for every } x \text{ and } u,

and shifting left and then right (or vice versa) is the identity:

S^\top S = S S^\top = I .

Thus $S$ is an orthogonal (permutation) matrix; this is the fact behind the orthogonality of its eigenvectors used in the derivation of the Fourier transform.

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 left shift operator is `Sᵀ`, i.e.
`(Sᵀx)_u = x_{u+1}`, and `S` is orthogonal: `SᵀS = SSᵀ = I`. -/
theorem shift_orthogonal {R : Type*} [CommRing R] {n : ℕ} [NeZero n] :
    (∀ (x : ZMod n → R) (u : ZMod n), ((shift R n)ᵀ *ᵥ x) u = x (u + 1)) ∧
      (shift R n)ᵀ * shift R n = 1 ∧ shift R n * (shift R n)ᵀ = 1 := by sorry
end GeomDL.Grids

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §4.2, side-note p. 37, "The left shift operator is given by S⊤ … S is orthogonal: S⊤S = SS⊤ = I"

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