Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Separated Permutation Blocks

Abstract

A lower block of a separated interval permutation occupies the initial interval.

Theorem 1.1 (Initial interval of a low block).

Lean statement: D5/S3/Combinatorics/ArcherCyclicPadovanBlocks.low_block_perm_initial

Proof. Machine-checked in Lean as D5/S3/Combinatorics/ArcherCyclicPadovanBlocks.low_block_perm_initial (✓ 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.

If two consecutive blocks together permute an interval and every letter of the first block is smaller than every letter of the second, the first block permutes the initial segment of that interval.

References

  • Truth anchor: D5/S3/Combinatorics/ArcherCyclicPadovanBlocks.low_block_perm_initial