Crossing after an Initial Two

Abstract

A primitive word beginning with two must cross the next letter.

Theorem 1.1 (First three before the second two).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwo.primitive_two_crossing

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

In a primitive avoider beginning with two, with later first occurrences increasing, the first three precedes the second two.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwo.primitive_two_crossing
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveBlocks