Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unique Primitive Increasing Word

Abstract

Exactly one increasing-order word is primitive at each positive size.

Theorem 1.1 (Existence at each positive size).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveIncUnique.primitive_increasing_exists

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveIncUnique.primitive_increasing_exists (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Sergi Elizalde, Amya Luo (2024). Pattern avoidance in nonnesting permutations. DOI: 10.48550/arXiv.2412.00336. URL: https://arxiv.org/abs/2412.00336v6.

Commentary.

For every positive n, at least one increasing-order avoider of size n is primitive.

Theorem 1.2 (Uniqueness at each positive size).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveIncUnique.primitive_increasing_unique

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveIncUnique.primitive_increasing_unique (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Sergi Elizalde, Amya Luo (2024). Pattern avoidance in nonnesting permutations. DOI: 10.48550/arXiv.2412.00336. URL: https://arxiv.org/abs/2412.00336v6.

Commentary.

Any two primitive increasing-order avoiders of the same positive size are equal.

References