Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

RotationAvoidanceMarkedContraction

Abstract

Contraction of the endpoints two and three gives a binary exponential count.

Theorem 1.1 (Binary count with endpoints two and three).

Lean statement: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceMarkedContraction.binary_second_consecutive_endpoint_count

Proof. Machine-checked in Lean as D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceMarkedContraction.binary_second_consecutive_endpoint_count (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ömer Eğecioğlu, Collier Gaiser, Mei Yin (2026). Pattern avoidance in permutations and their rotations. DOI: 10.48550/arXiv.2607.20750. URL: https://arxiv.org/abs/2607.20750v1.

Commentary.

For width at least three, permutations of one through width plus two beginning with two and ending with three, and containing 1342 in exactly the uncut rotation, number 2^width minus twice width. Contraction and its increasing inverse relabelling preserve pattern containment and identify the relevant circular classes with classical avoidance classes.

References