Recovering a Cyclic Permutation

Abstract

The orbit word of a cyclic permutation recovers its one-line form.

Theorem 1.1 (Recover the one-line permutation).

Lean statement: D5/S3/Combinatorics/ArcherCyclicPadovanCycleWords.oneLine_orbitWord

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ArcherCyclicPadovanCycleWords.oneLine_orbitWord (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kassie Archer, Ethan Borsh, Jensen Bridges, Christina Graves, Millie Jeske (2024). Pattern-restricted cyclic permutations with a pattern-restricted cycle form. DOI: 10.48550/arXiv.2408.15000. URL: https://arxiv.org/abs/2408.15000v1.

Commentary.

For a cyclic permutation of the integers from one through its length, the successor permutation of its orbit word is the original permutation.

References

• Truth anchor: D5/S3/Combinatorics/ArcherCyclicPadovanCycleWords.oneLine_orbitWord
• Dependency: D5/S3/Combinatorics/ArcherCyclicTetranacciCycleWords