An Upward Edge and a Later Intermediate Value

Abstract

The cyclic successor of an earlier value cannot cross a later value in a 312-avoider.

Theorem 1.1 (Exclusion of a crossing successor).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaCube312Edge.no_upward_edge_over_later_value

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

In a 312-avoiding permutation, there are no letters x and z such that x occurs before z and x is smaller than z while z is smaller than the cyclic successor of x in its record block.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaCube312Edge.no_upward_edge_over_later_value
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverse