Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A Large Initial Letter

Abstract

A large initial value repeats immediately and determines a value cut.

Theorem 1.1 (Immediate repetition of a large first letter).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourLargeFirst.large_first_double

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

An avoider beginning with k at least three has a second k immediately after the first.

Theorem 1.2 (Cut after a large initial block).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourLargeFirst.large_first_cut

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

If an avoider begins with k at least three and below n, it has a value cut at k.

References