Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A Cycle Forced by Two Successors

Abstract

Two specified successor edges force a single initial record block.

Theorem 1.1 (The return edge to one).

Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateShortCycle.second_to_penultimate_forces_one_block

Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaIterateShortCycle.second_to_penultimate_forces_one_block (✓ 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 132-avoiding permutation q of size h at least four, if the cyclic successors of one and two are h and h minus one and the successor of h exceeds one, then the successor of h minus one is one and q begins with h.

References