Forced Prefix after an Initial Two

Abstract

Primitivity fixes the positions of the first two small letters.

Theorem 1.1 (Positions of one, two, and three).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwoPrefix.primitive_two_positions

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

A primitive avoider of size at least three beginning with two has its first one at position one, first three at position two, second two at position three, and second one at position four.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwoPrefix.primitive_two_positions
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwo