Orbits of cyclic rotation

Cyclic rotation of a nonempty finite ordinal is a single cycle through every point, including the singleton case where the rotation is the identity: its full cycle partition has the one part n, so it has one orbit and order n. Its powers that are again single cycles through every point are exactly those with exponent coprime to n. The orbit count includes fixed points. The formula is useful when a traversal permutation is identified, up to conjugacy, with cyclic rotation: it reduces the resulting orbit or component count to whether the underlying ordinal is empty.

theorem TauCeti.parts_partition_finRotate {n : ℕ} (hn : n ≠ 0) : (finRotate n).partition.parts = {n}

The full cycle partition of cyclic rotation of a nonempty finite ordinal has the single part n.

theorem TauCeti.orderOf_finRotate {n : ℕ} (hn : n ≠ 0) : orderOf (finRotate n) = n

Cyclic rotation of a nonempty finite ordinal of length n has order n.

theorem TauCeti.parts_partition_finRotate_pow {n k : ℕ} (hn : n ≠ 0) (hk : k.Coprime n) : (finRotate n ^ k).partition.parts = {n}

A power of cyclic rotation of a nonempty finite ordinal of length n, with exponent coprime to n, is again a single cycle through every point: its full cycle partition has the single part n.

@[simp]

theorem TauCeti.parts_partition_finRotate_pow_eq_singleton_iff {n k : ℕ} (hn : n ≠ 0) : (finRotate n ^ k).partition.parts = {n} ↔ k.Coprime n

A power of cyclic rotation of a nonempty finite ordinal of length n is a single cycle through every point exactly when its exponent is coprime to n.

@[simp]

theorem TauCeti.orbitCount_finRotate (n : ℕ) : orbitCount (finRotate n) = if n = 0 then 0 else 1

Cyclic rotation has one orbit when the ordinal is nonempty, and none otherwise.