Classification of Primitive Avoiders

Abstract

Primitive words fall into three explicit structural families.

Theorem 1.1 (Three primitive families).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveClassify.primitive_classification

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveClassify.primitive_classification (✓ 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 size at least three, a primitive four-pattern avoider is a doubled largest-letter prefix with an increasing-order tail, a primitive increasing-order word, or a specified 21321 prefix with a shifted primitive increasing-order tail.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveClassify.primitive_classification
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveLarge
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveTwoConstruct