Boundary Entries of Fixed 231-Avoiders

Abstract

Indecomposable fixed 231-avoiders have prescribed entries at their boundaries.

Theorem 1.1 (The second and last entries).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Boundary.terminal_value_next_to_max

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Boundary.terminal_value_next_to_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.

A sum-indecomposable 231-avoiding permutation of size n greater than three fixed by the third inverse iterate ends with n minus one and has one in position one, with positions numbered from zero.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Boundary.terminal_value_next_to_max
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseTail
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicSumIndecomp
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231ForcedPrefix
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Middle
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Pair
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaCube231Prefix