Continuants for Bounded Dyck Path Series
Abstract
Weighted Dyck path series in a finite strip are quotients of continuants whose denominators are invertible power series.
Definition 1.1 (The continuant recurrence).
Lean statement: D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.cont
Formalization. D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.cont (✓ std3).
Source. Repository-derived.
Acknowledgement. Johann Cigler (2026). Some sequences and number triangles which are related to Narayana polynomials and to q-Narayana polynomials for q=-1. DOI: 10.48550/arXiv.2608.03363. URL: https://arxiv.org/abs/2608.03363v2.
Commentary.
Given a sequence a_n in a commutative ring and initial values r_0 and r_1, the continuant sequence starts with K_0 = r_0 and K_1 = r_1 and satisfies K_{n+2} = K_{n+1} - a_n K_n for every nonnegative integer n. The initial values zero and one give the numerator sequence, while the initial values one and one give the denominator sequence.
Theorem 1.2 (A unit denominator and the strip series).
Lean statement: D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.continuant_representation
Proof. Machine-checked in Lean as D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.continuant_representation (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Johann Cigler (2026). Some sequences and number triangles which are related to Narayana polynomials and to q-Narayana polynomials for q=-1. DOI: 10.48550/arXiv.2608.03363. URL: https://arxiv.org/abs/2608.03363v2.
Commentary.
Let w_k be any sequence of polynomials with integer coefficients, and assume the weighted strip sums obey the first-return convolution for every weight sequence, bound b and semilength n + 1: the sum at height b + 1 is w_0 times the sum over i from zero through n of the height-b sum of semilength i with weights shifted by one times the height-(b + 1) sum of semilength n - i with the original weights. Set a_k = w_k z, and let P and Q be the continuant sequences with initial values (0, 1) and (1, 1), respectively. For every nonnegative height h, Q_{h+1} is an invertible formal power series and Q_{h+1} times the weighted strip series of height h equals P_{h+1}.
References
- Truth anchor:
D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.cont - Truth anchor:
D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants.continuant_representation - Dependency: D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductDefs