RotationAvoidanceGaps
Abstract
Three strict inequalities distinguish circular classes with one containing cut.
Theorem 1.1 (Three strict count comparisons).
Lean statement: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceGaps.three_strict_count_gaps
Proof. Machine-checked in Lean as D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceGaps.three_strict_count_gaps (✓ 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 every size at least seven, among circular permutations rooted at one with exactly one containing rotation, the 2143 count is strictly smaller than the 1234 count, the 1234 count is strictly smaller than the 1432 count, and the 1243 count is strictly smaller than the 1342 count. Endpoint decompositions and their exact counts yield all three comparisons.
References
- Truth anchor:
D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceGaps.three_strict_count_gaps - Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceAscendingSplit
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceConsecutive
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceDescending
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceDescendingSplit
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceEndpoints
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceMarkedContraction
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceMixed
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceMixedEmptyCount
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceOneAscent
- Dependency: D5/S3/Combinatorics/RotationAvoidance/RotationAvoidanceSlices