Counting Avoiders with a Maximal Tail
Abstract
Removing a final maximum preserves every 132-avoidance layer.
Theorem 1.1 (The count after removing a final maximum).
Lean statement: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTailCount.final_tail_count
Proof. Machine-checked in Lean as D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTailCount.final_tail_count (✓ 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 every size n and depth k, the number of depth-k 132-avoiders of size n plus one ending with n plus one equals the number of depth-k 132-avoiders of size n.
References
- Truth anchor:
D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTailCount.final_tail_count - Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseBlocks
- Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaBasicInverseGeneral
- Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateDefs
- Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateScan
- Dependency: D5/S3/Combinatorics/FundamentalBijection/ThetaIterateTail