The High Prefix before One

Abstract

A predecessor of one and the terminal value determine a decreasing prefix.

Theorem 1.1 (A forced decreasing prefix).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231ForcedPrefix.forced_high_prefix

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaCube231ForcedPrefix.forced_high_prefix (✓ 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 231-avoiding permutation of size n ending with c, if one occurs at a position t strictly between zero and n minus one and is preceded by c plus one, then its first t letters are n, n minus one, down to c plus one.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231ForcedPrefix.forced_high_prefix
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Prefix