The Final Pair from a Small Second Value

Abstract

A small second parameter value determines the last two entries.

Theorem 1.1 (The forced final pair).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateFirstScan.small_second_forces_final_pair

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaIterateFirstScan.small_second_forces_final_pair (✓ 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 r of size h at least four beginning with h and with second value between two and h minus two, if both r and b(r) avoid 132, then r ends with one, h minus one.

References

• Truth anchor: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateFirstScan.small_second_forces_final_pair
• Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateFirstEndpoint