Adding the Doubled Largest Prefix

Abstract

An increasing-order tail yields an avoider after a doubled largest prefix.

Theorem 1.1 (Constructing a large-prefix avoider).

Lean statement: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveLargeConverse.large_prefix_construct

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveLargeConverse.large_prefix_construct (✓ 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 n at least two, prefixing an increasing-order avoider of size n minus one with two copies of n gives a four-pattern avoider of size n.

References

• Truth anchor: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitiveLargeConverse.large_prefix_construct
• Dependency: D5/S3/Combinatorics/Nonnesting/NonnestingFourPrimitivePrefix