Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finiteness of Pure Histories

Abstract

Fixing the length and expenditure leaves only finitely many pure histories.

Theorem 1.1 (Finite length and expenditure classes).

Lean statement: D5/S3/Combinatorics/WeakAscent/WeakAscent215Finite.pure_histories_finite

Proof. Machine-checked in Lean as D5/S3/Combinatorics/WeakAscent/WeakAscent215Finite.pure_histories_finite (✓ 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.

For every pair of nonnegative integers l and s, the set of pure step lists of length l and expenditure s that run from the empty stack to some terminal stack is finite.

References