Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finiteness of Full Histories

Abstract

A fixed initial state has finitely many full histories of any prescribed length.

Theorem 1.1 (Finite full-history classes).

Lean statement: D5/S3/Combinatorics/WeakAscent/WeakAscent215HistoryFinite.full_histories_finite

Proof. Machine-checked in Lean as D5/S3/Combinatorics/WeakAscent/WeakAscent215HistoryFinite.full_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 nonnegative length d, Boolean stack, nonnegative budget and Boolean mode, the set of full step lists of length d that run from this initial state is finite.

References