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.
, and
Statement
In the Motzkin generating function (Motzkin paths, Schröder paths, the Motzkin numbers , the large Schröder numbers , and their generating functions) satisfies
and, with the formal binomial power of Formal exponential, logarithm, and binomial powers over a commutative -algebra,
the series being the unique element of whose square is (Every with has a unique th root with constant coefficient in a commutative -algebra).
Facts & Assumptions
Given: a natural number , and the Motzkin paths and numbers of Motzkin paths, Schröder paths, the Motzkin numbers , the large Schröder numbers , and their generating functions.
is the set of lattice paths of length with steps in , where , and , from to with for every ; each such path advances the first coordinate by at every step; is finite; and ; and (Motzkin paths, Schröder paths, the Motzkin numbers , the large Schröder numbers , and their generating functions).
A natural number written where a rational is expected denotes its image under an injective embedding preserving addition, multiplication and finite sums, and is a commutative -algebra (The Catalan generating function in ).
For a step set , a point and , the map sending a lattice path to its step word is a bijection (For each start point the step word is a bijection onto ).
For : is a bijection if and only if there is a function with and ( is a bijection if and only if there is a function with and ; such a is unique, equals the inverse relation , and is itself a bijection).
If and are finite and disjoint then ; and if is finite and are pairwise disjoint finite sets then (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clauses 1 and 2).
If and are finite then is finite and (The product rule: , and , clause 1).
For a finite index set and the sum is defined, and (The sum over a finite index set, and its product form, clause (c)).
; if and only if for every ; for and for ; and (Coefficient extraction is -linear, separates formal series, shifts under multiplication by , and converts products to finite convolution).
For a commutative -algebra , and , there is a unique with , namely (Every with has a unique th root with constant coefficient in a commutative -algebra).
For and the formal binomial power is (Formal exponential, logarithm, and binomial powers over a commutative -algebra).
The coefficientwise sum and Cauchy product make a commutative ring (Cauchy multiplication makes a commutative ring containing as the finitely supported subring).
If is finite and is a bijection then is finite and (The cardinality of a finite set).
Every nonempty subset has a least element (The well-ordering principle).
Proof
First-return decomposition. Let with step word and heights . Its first step is not , since would fail, so it is or . If it is then and the path of length with step word has heights , so it lies in . If it is then ; the set of positive indices with contains , so by [L11] it has a least element , and by minimality while , so the step at is and ; putting , the path of length with step word has heights ending at , so , and the path of length with step word has heights ending at , so , with because . Conversely, prepending to a member of , and sending to the path with step word , that of , , that of , produce members of whose first-return data are the ones started from; the two constructions are two-sided inverses, so by [L1] and [L2] the set is in bijection with the disjoint union of and the sets for .
Counting the two sides of step 1.1 with [F1], [L3], [L4], [L5] and [L10] gives, in , the sum being over the finite index set . At that index set is empty and the sum is , so , which is correct because a path of length beginning with cannot return to height . At it gives , at it gives , and at it gives .
Comparing coefficients gives the functional equation. At the index : by [L6], and . At an index : , while is when and when , by the shift and Cauchy-product clauses of [L6]; in both cases this matches the sum of step 2.1, so . Extensionality in [L6] gives .
Rearranging step 3.1 in the commutative ring gives , and hence The series has coefficient at the index , so it lies in , and with ; by the uniqueness clause of [L7] with it is therefore the series of [L8], which gives . No division by occurs, and none is available: that series has coefficient at the index and is not a unit.
Remarks
-
The route is the page's own, run on a third step set. No combinatorial class, no symbolic-method operator and no fixed-point theorem is used; the argument is the first-return decomposition of Every Dyck path of semilength factors uniquely as with and with a level step added, and the added case is the whole difference between the Dyck recurrence and this one. The source reaches the same equation from an infinite continued fraction, which needs machinery this page does not build, so the proof here is local while the statement is the source's.
-
Where the level step shows in the equation. It contributes the summand , and the pair of a with its matching contributes the factor : two units of length for one pair. The convolution index therefore stops at and not at , which is exactly the point at which the Schröder equation differs.
Depends on
- Motzkin paths, Schröder paths, the Motzkin numbers $M_n$, the large Schröder numbers $R_n$, and their generating functions
- The Catalan generating function $C(x)=\sum_{n\ge0}C_nx^n$ in $\mathbb{Q}\llbracket x\rrbracket$
- For each start point the step word is a bijection onto $S^n$
- $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = \Delta_A$ and $f \circ g = \Delta_B$; such a $g$ is unique, equals the inverse relation $f^{-1}$, and is itself a bijection
- The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
- The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form
- Coefficient extraction is $R$-linear, separates formal series, shifts under multiplication by $x^k$, and converts products to finite convolution
- Every $1+u$ with $u\in xR\llbracket x\rrbracket$ has a unique $k$th root with constant coefficient $1$ in a commutative $\mathbb Q$-algebra
- Formal exponential, logarithm, and binomial powers over a commutative $\mathbb Q$-algebra
- Cauchy multiplication makes $R\llbracket x\rrbracket$ a commutative ring containing $R[x]$ as the finitely supported subring
- The cardinality $\lvert A\rvert$ of a finite set
- The well-ordering principle
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
61 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.