Active Letters in the First Class
Abstract
Appendable letters in the first class separate into new records, the current maximum and lower sites.
Theorem 1.1 (Structure of appendable letters).
Lean statement: D5/S3/Combinatorics/WeakAscent/WeakAscent215Sites.left_active_structure
Proof. Machine-checked in Lean as D5/S3/Combinatorics/WeakAscent/WeakAscent215Sites.left_active_structure (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. David Callan, Toufik Mansour (2025). Ascent Sequences and Weak Ascent Sequences Avoiding a Quadruple of Length-3 Patterns. DOI: 10.5281/zenodo.17144266. URL: https://math.colgate.edu/~integers/z80/z80.pdf.
Commentary.
Let w be a nonempty weak ascent sequence avoiding 100, 101, 110 and 201, with maximum M and last entry L. The bound one plus the weak ascent count is strictly greater than M. Every integer strictly above M and at most that bound is appendable and does not occur in w. The letter M is appendable exactly when L = M. Every appendable letter at most M other than M is strictly less than L.
References
- Truth anchor:
D5/S3/Combinatorics/WeakAscent/WeakAscent215Sites.left_active_structure - Dependency: D5/S3/Combinatorics/WeakAscent/WeakAscent215Left
- Dependency: D5/S3/Combinatorics/WeakAscent/WeakAscentGrowth