The Prefix before One in a 231-Avoider

Abstract

The part of a 231-avoider preceding one is decreasing.

Theorem 1.1 (Decreasing entries before one).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Prefix.avoid231_prefix_before_one_decreasing

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Prefix.avoid231_prefix_before_one_decreasing (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Kassie Archer, Robert P. Laudone (2024). Pattern avoidance and the fundamental bijection. DOI: 10.48550/arXiv.2407.06338. URL: https://arxiv.org/abs/2407.06338v1.

Commentary.

For a nonempty 231-avoiding permutation, any two positions before the position of one have their values in decreasing order.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Prefix.avoid231_prefix_before_one_decreasing
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse