Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Equinumerosity of the Weak Ascent Sequence Classes in Class 215

Abstract

The two weak ascent sequence classes in Class 215 have equal cardinalities in every length.

Theorem 1.1 (The Class 215 equinumerosity).

Lean statement: D5/S3/Combinatorics/WeakAscent/WeakAscentClass215.result

Proof. Machine-checked in Lean as D5/S3/Combinatorics/WeakAscent/WeakAscentClass215.result (✓ std3). ∎

Resolves. Problems/callan-mansour-weak-ascent-class-215 (proved) by D5/S3/Combinatorics/WeakAscent/WeakAscentClass215.result.

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.

For every nonnegative integer n, the number of weak ascent sequences of length n avoiding 100, 101, 110 and 201 equals the number avoiding 021, 101, 201 and 210.

References