Appending a Maximal Fixed Point

Abstract

The fundamental bijection commutes with appending a new maximum.

Theorem 1.1 (An unchanged maximal tail).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTail.theta_append_max

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTail.theta_append_max (✓ 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 permutation w of size h, the fundamental image of w followed by h plus one is the fundamental image of w followed by h plus one.