How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
is a finite set
Statement
For every the set of Dyck paths of semilength (Dyck paths of semilength ) is finite and nonempty; more precisely has at least one and at most elements.
Facts & Assumptions
Given: a natural number .
is the set of diagonal paths of length from to whose height function satisfies for every with (Dyck paths of semilength ).
A diagonal path of length from is the same datum as a function with and for (Diagonal lattice paths with steps and , and the height function).
For a step set , a point and , the map sending a lattice path to its step word is a bijection , and is finite with (For each start point the step word is a bijection onto ).
For finite sets and , the set of functions is finite and (The set of functions between finite sets is finite, with ).
A subset of a finite set is finite, and a subset of a finite set has (A subset of a finite set is finite, with , and equality holds if and only if , clauses 1 and 2).
A property that holds at and passes from every natural number to its successor holds at every natural number: if a property satisfies and () for all , then holds for all (The principle of mathematical induction).
Proof
The set of all diagonal paths of length from the origin is finite with exactly elements, since the step set has two elements.
The word of length with for even and for odd traces a Dyck path: its height function satisfies , and if with then and , so by induction on every even index has height and every odd index height ; hence throughout and .
By [F1] the set is a subset of the finite set of step 1.1, hence finite with at most elements by [L3]; and it is nonempty by step 1.2, so it has at least one element.
Remarks
-
What this lemma is for. It is the well-definedness obligation behind the Catalan numbers: is a natural number only because is finite, and the cardinality notation is defined for finite sets alone.
-
The bound is not the point. It is the crude count of all words of length over a two-letter alphabet, recorded because it is what makes the set finite; the exact count is the subject of the theorems below and is far smaller.
Depends on
- Dyck paths of semilength $n$
- For each start point the step word is a bijection onto $S^n$
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
- The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$
- The principle of mathematical induction
- Diagonal lattice paths with steps $U=(1,1)$ and $D=(1,-1)$, and the height function
Used by
- The Catalan number Cₙ:=lvertDₙ| Definition
- Cₙ₊₁=∑ᵢ₌₀ⁿCᵢ Cₙ₋ᵢ, with C₀=1 Theorem
Dependency tree · two levels
28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- A. Postnikov (notes by A. Lin), MIT 18.212 Algebraic Combinatorics, Spring 2019 (standard reference, not scraped)