TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$M (x) = 1 + x M (x) + x^{2} M (x)^{2}$ , and $2 x^{2} M (x) = 1 - x - (1 - 2 x - 3 x^{2})^{1 / 2}$

Statement

In $Q ⟦ x ⟧$ the Motzkin generating function (Motzkin paths, Schröder paths, the Motzkin numbers $M_{n}$ , the large Schröder numbers $R_{n}$ , and their generating functions) satisfies

$M = 1 + x M + x^{2} M^{2},$

and, with $(1 - 2 x - 3 x^{2})^{1 / 2}$ the formal binomial power of Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra,

$2 x^{2} M = 1 - x - (1 - 2 x - 3 x^{2})^{1 / 2},$

the series $1 - x - 2 x^{2} M$ being the unique element of $1 + x Q ⟦ x ⟧$ whose square is $1 - 2 x - 3 x^{2}$ (Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra).

Facts & Assumptions

Given: a natural number $n$ , and the Motzkin paths and numbers of Motzkin paths, Schröder paths, the Motzkin numbers $M_{n}$ , the large Schröder numbers $R_{n}$ , and their generating functions.

[F1]

${M o t}_{m}$ is the set of lattice paths of length $m$ with steps in ${U, D, L}$ , where $U = (1, 1)$ , $D = (1, - 1)$ and $L = (1, 0)$ , from $(0, 0)$ to $(m, 0)$ with $h (i) \geq 0$ for every $i \leq m$ ; each such path advances the first coordinate by $1$ at every step; $M_{m} = ∣ {M o t}_{m} ∣$ is finite; $M_{0} = 1$ and $M_{1} = 1$ ; and $M (x) = \sum_{m \geq 0} M_{m} x^{m}$ (Motzkin paths, Schröder paths, the Motzkin numbers $M_{n}$ , the large Schröder numbers $R_{n}$ , and their generating functions).

[F2]

A natural number written where a rational is expected denotes its image under an injective embedding preserving addition, multiplication and finite sums, and $Q ⟦ x ⟧$ is a commutative $Q$ -algebra (The Catalan generating function $C (x) = \sum_{n \geq 0} C_{n} x^{n}$ in $Q ⟦ x ⟧$ ).

[L1]

For a step set $S$ , a point $P$ and $ℓ \in N$ , the map sending a lattice path to its step word is a bijection $L_{S} (P; ℓ) \to S^{ℓ}$ (For each start point the step word is a bijection onto $S^{n}$ ).

[L2]

For $f : A \to B$ : $f$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ( $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

[L3]

If $A$ and $B$ are finite and disjoint then $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ ; and if $I$ is finite and $(A_{i})_{i \in I}$ are pairwise disjoint finite sets then $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clauses 1 and 2).

[L4]

If $A$ and $B$ are finite then $A \times B$ is finite and $∣ A \times B ∣ = ∣ A ∣ \cdot ∣ B ∣$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , clause 1).

[L5]

For a finite index set $S$ and $a : S \to N$ the sum $\sum_{i \in S} a_{i}$ is defined, and $\sum_{i \in \emptyset} a_{i} = 0$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, clause (c)).

[L6]

$[x^{m}] (f + g) = [x^{m}] f + [x^{m}] g$ ; $f = g$ if and only if $[x^{m}] f = [x^{m}] g$ for every $m$ ; $[x^{m}] (x^{k} f) = [x^{m - k}] f$ for $k \leq m$ and $0$ for $k > m$ ; and $[x^{m}] (f g) = \sum_{i = 0}^{m} [x^{i}] f [x^{m - i}] g$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[L7]

For a commutative $Q$ -algebra $R$ , $u \in x R ⟦ x ⟧$ and $k \geq 1$ , there is a unique $v \in 1 + x R ⟦ x ⟧$ with $v^{k} = 1 + u$ , namely $v = (1 + u)^{1 / k}$ (Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra).

[L8]

For $u \in x R ⟦ x ⟧$ and $c \in R$ the formal binomial power is $(1 + u)^{c} : = \exp (c \log (1 + u))$ (Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra).

[L9]

The coefficientwise sum and Cauchy product make $Q ⟦ x ⟧$ a commutative ring (Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ as the finitely supported subring).

[L10]

If $A$ is finite and $f : A \to B$ is a bijection then $B$ is finite and $∣ B ∣ = ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set).

[L11]

Every nonempty subset $S \subseteq N$ has a least element (The well-ordering principle).

Proof

technique · direct

1.1F1L1L2L11

First-return decomposition. Let $v \in {M o t}_{n + 1}$ with step word $w$ and heights $h$ . Its first step is not $D$ , since $h (1) \geq 0$ would fail, so it is $L$ or $U$ . If it is $L$ then $h (1) = 0$ and the path of length $n$ with step word $w_{1} \dots w_{n}$ has heights $h (1 + j)$ , so it lies in ${M o t}_{n}$ . If it is $U$ then $h (1) = 1$ ; the set of positive indices $j \leq n + 1$ with $h (j) = 0$ contains $n + 1$ , so by [L11] it has a least element $τ \geq 2$ , and $h (τ - 1) \geq 1$ by minimality while $h (τ) = 0$ , so the step at $τ$ is $D$ and $h (τ - 1) = 1$ ; putting $i : = τ - 2$ , the path $P$ of length $i$ with step word $w_{1} \dots w_{i}$ has heights $h (1 + j) - 1 \geq 0$ ending at $h (τ - 1) - 1 = 0$ , so $P \in {M o t}_{i}$ , and the path $Q$ of length $n - 1 - i$ with step word $w_{τ} \dots w_{n}$ has heights $h (τ + j) \geq 0$ ending at $0$ , so $Q \in {M o t}_{n - 1 - i}$ , with $0 \leq i \leq n - 1$ because $τ \leq n + 1$ . Conversely, prepending $L$ to a member of ${M o t}_{n}$ , and sending $(i, P, Q)$ to the path with step word $U$ , that of $P$ , $D$ , that of $Q$ , produce members of ${M o t}_{n + 1}$ whose first-return data are the ones started from; the two constructions are two-sided inverses, so by [L1] and [L2] the set ${M o t}_{n + 1}$ is in bijection with the disjoint union of ${M o t}_{n}$ and the sets ${i} \times {M o t}_{i} \times {M o t}_{n - 1 - i}$ for $0 \leq i \leq n - 1$ .

2.1F1L3L4L5L10step 1.1

Counting the two sides of step 1.1 with [F1], [L3], [L4], [L5] and [L10] gives, in $N$ , $M_{n + 1} = M_{n} + \sum_{i = 0}^{n - 1} M_{i} M_{n - 1 - i},$ the sum being over the finite index set ${0, \dots, n - 1}$ . At $n = 0$ that index set is empty and the sum is $0$ , so $M_{1} = M_{0} = 1$ , which is correct because a path of length $1$ beginning with $U$ cannot return to height $0$ . At $n = 1$ it gives $M_{2} = M_{1} + M_{0} M_{0} = 2$ , at $n = 2$ it gives $M_{3} = M_{2} + M_{0} M_{1} + M_{1} M_{0} = 4$ , and at $n = 3$ it gives $M_{4} = M_{3} + M_{0} M_{2} + M_{1} M_{1} + M_{2} M_{0} = 9$ .

3.1F1F2L6L9step 2.1

Comparing coefficients gives the functional equation. At the index $0$ : $[x^{0}] (1 + x M + x^{2} M^{2}) = 1$ by [L6], and $[x^{0}] M = M_{0} = 1$ . At an index $n + 1$ : $[x^{n + 1}] (x M) = [x^{n}] M = M_{n}$ , while $[x^{n + 1}] (x^{2} M^{2})$ is $[x^{n - 1}] (M^{2}) = \sum_{i = 0}^{n - 1} M_{i} M_{n - 1 - i}$ when $n \geq 1$ and $0$ when $n = 0$ , by the shift and Cauchy-product clauses of [L6]; in both cases this matches the sum of step 2.1, so $[x^{n + 1}] (1 + x M + x^{2} M^{2}) = M_{n + 1} = [x^{n + 1}] M$ . Extensionality in [L6] gives $M = 1 + x M + x^{2} M^{2}$ .

4.1L6L7L8L9step 3.1∎

Rearranging step 3.1 in the commutative ring $Q ⟦ x ⟧$ gives $x^{2} M^{2} + (x - 1) M + 1 = 0$ , and hence $(1 - x - 2 x^{2} M)^{2} = (x - 1)^{2} + 4 x^{2} (x^{2} M^{2} + (x - 1) M) = (x - 1)^{2} - 4 x^{2} = 1 - 2 x - 3 x^{2} .$ The series $1 - x - 2 x^{2} M$ has coefficient $1$ at the index $0$ , so it lies in $1 + x Q ⟦ x ⟧$ , and $1 - 2 x - 3 x^{2} = 1 + u$ with $u = - 2 x - 3 x^{2} \in x Q ⟦ x ⟧$ ; by the uniqueness clause of [L7] with $k = 2$ it is therefore the series $(1 - 2 x - 3 x^{2})^{1 / 2}$ of [L8], which gives $2 x^{2} M = 1 - x - (1 - 2 x - 3 x^{2})^{1 / 2}$ . No division by $2 x^{2}$ occurs, and none is available: that series has coefficient $0$ at the index $0$ 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 $n + 1$ factors uniquely as $U P D Q$ with $P \in D_{i}$ and $Q \in D_{n - i}$ 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 $x M$ , and the pair of a $U$ with its matching $D$ contributes the factor $x^{2}$ : two units of length for one pair. The convolution index therefore stops at $n - 1$ and not at $n$ , which is exactly the point at which the Schröder equation differs.

Depends on

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.

Sources

C. Krattenthaler, "Lattice Path Enumeration", ch. 10 of the Handbook of Enumerative Combinatorics, §10.9, Theorem 10.9.2, equation (10.49) (standard reference, not scraped)

M(x)=1+x M(x)+x2M(x)2M(x)=1+xM(x)+x2M(x)2, and 2x2M(x)=1−x−(1−2x−3x2)1/22x2M(x)=1−x−(1−2x−3x2)1/2