Separated Prefixes

Abstract

A value-separated prefix of a permutation consists of small letters.

Theorem 1.1 (The range of a separated prefix).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicSum.separated_prefix_cut

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaBasicSum.separated_prefix_cut (✓ 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.

If every letter in a prefix of length k is smaller than every letter in the remaining suffix, then every letter in the prefix is at most k.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicSum.separated_prefix_cut
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseGeneral