First-Block Order

Abstract

The leading value controls the first occurrences in a four-pattern avoider.

Theorem 1.1 (Order imposed by the first letter).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourBlocks.first_block_structure

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

When an avoider begins with k, first occurrences below k increase by value and precede first occurrences above k.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourBlocks.first_block_structure
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveThree