The Survivor Series Factorization

Abstract

Marking a terminal old entry factors the survivor series into two history series.

Theorem 1.1 (Factorization of marked survivors).

Lean statement: D5/S3/Combinatorics/WeakAscent/WeakAscent215Survivors.survivor_series

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

The bivariate series counting pure histories with a chosen terminal old entry equals the product of the pure-history series and the record-ending series. Both expenditure and length are additive in the product.

References

• Truth anchor: D5/S3/Combinatorics/WeakAscent/WeakAscent215Survivors.survivor_series
• Dependency: D5/S3/Combinatorics/WeakAscent/WeakAscent215GroupedRenewal