TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$R (x) = 1 + x R (x) + x R (x)^{2}$ , and $2 x R (x) = 1 - x - (1 - 6 x + x^{2})^{1 / 2}$

Statement

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

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

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

$2 x R = 1 - x - (1 - 6 x + x^{2})^{1 / 2},$

the series $1 - x - 2 x R$ being the unique element of $1 + x Q ⟦ x ⟧$ whose square is $1 - 6 x + 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 Schröder 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]

${S c h}_{m}$ is the set of lattice paths with steps in ${U, D, L_{2}}$ , where $U = (1, 1)$ , $D = (1, - 1)$ and $L_{2} = (2, 0)$ , from $(0, 0)$ to $(2 m, 0)$ with $h (i) \geq 0$ at every index; such a path with $k$ up steps has $k$ down steps, $m - k$ level steps and $m + k$ steps in all, with $0 \leq k \leq m$ ; $R_{m} = ∣ {S c h}_{m} ∣$ is finite; $R_{0} = 1$ and $R_{1} = 2$ , the two paths of half-length $1$ having step words $L_{2}$ and $U D$ ; and $R (x) = \sum_{m \geq 0} R_{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 (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[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.1

First-return decomposition. Let $v \in {S c h}_{n + 1}$ , of length $ℓ$ , with step word $w$ and heights $h$ . Its first step is not $D$ , so it is $L_{2}$ or $U$ . If it is $L_{2}$ then translating the remaining path by $(- 2, 0)$ gives a member of ${S c h}_{n}$ , since its endpoints become $(0, 0)$ and $(2 n, 0)$ and its heights are unchanged. If it is $U$ then $h (1) = 1$ ; the set of positive indices $j \leq ℓ$ with $h (j) = 0$ contains $ℓ$ , so by [L11] it has a least element $τ \geq 2$ , and $h (τ - 1) \geq 1$ by minimality while $h (τ) = 0$ , so the step at $τ$ lowers the height and is therefore $D$ , with $h (τ - 1) = 1$ . Translating the portion of $v$ from the index $1$ to the index $τ - 1$ by $(- 1, - 1)$ gives a path from $(0, 0)$ whose heights are $h (1 + j) - 1 \geq 0$ and which returns to height $0$ ; its numbers of up and down steps are therefore equal, so its horizontal extent is even, say $2 i$ , and it lies in ${S c h}_{i}$ . Since the $D$ step at $τ$ has width $1$ , the first coordinate at $τ$ is $2 i + 2$ , so translating the portion from $τ$ to $ℓ$ by $(- 2 i - 2, 0)$ gives a member of ${S c h}_{n - i}$ , and $0 \leq i \leq n$ . Conversely, prepending $L_{2}$ to a member of ${S c h}_{n}$ , and sending $(i, P, Q)$ to the path with step word $U$ , that of $P$ , $D$ , that of $Q$ , produce members of ${S c h}_{n + 1}$ whose first-return data are the ones started from, because the heights strictly inside the first block are at least $1$ ; the two constructions are two-sided inverses, so by [L1] and [L2] the set ${S c h}_{n + 1}$ is in bijection with the disjoint union of ${S c h}_{n}$ and the sets ${i} \times {S c h}_{i} \times {S c h}_{n - i}$ for $0 \leq i \leq n$ .

F1L1L2L11

2.1

The index range is where this differs from the Motzkin case. A $U$ and its matching $D$ have width $1$ each, so together they consume two units of horizontal extent and therefore exactly one unit of half-length; the inner and outer blocks then carry half-lengths $i$ and $n - i$ with $i + (n - i) = n$ , so the convolution index runs over all of ${0, \dots, n}$ and not only over ${0, \dots, n - 1}$ . Counting the two sides of step 1.1 with [F1], [L3], [L4], [L5] and [L10] gives, in $N$ , $R_{n + 1} = R_{n} + \sum_{i = 0}^{n} R_{i} R_{n - i},$ the sum being over the finite index set ${0, \dots, n}$ . At $n = 0$ the sum has the single term $R_{0} R_{0} = 1$ , so $R_{1} = R_{0} + 1 = 2$ , matching the two paths with step words $L_{2}$ and $U D$ . At $n = 1$ it gives $R_{2} = R_{1} + R_{0} R_{1} + R_{1} R_{0} = 6$ , at $n = 2$ it gives $R_{3} = R_{2} + R_{0} R_{2} + R_{1} R_{1} + R_{2} R_{0} = 22$ , and at $n = 3$ it gives $R_{4} = R_{3} + R_{0} R_{3} + R_{1} R_{2} + R_{2} R_{1} + R_{3} R_{0} = 90$ .

F1L3L4L5L10step 1.1

3.1

Comparing coefficients gives the functional equation. At the index $0$ : $[x^{0}] (1 + x R + x R^{2}) = 1$ by [L6], and $[x^{0}] R = R_{0} = 1$ . At an index $n + 1$ : $[x^{n + 1}] (x R) = [x^{n}] R = R_{n}$ and $[x^{n + 1}] (x R^{2}) = [x^{n}] (R^{2}) = \sum_{i = 0}^{n} R_{i} R_{n - i}$ by the shift and Cauchy-product clauses of [L6], and the sum of the two is $R_{n + 1}$ by step 2.1. Extensionality in [L6] gives $R = 1 + x R + x R^{2}$ .

F1F2L6L9step 2.1

4.1

Rearranging step 3.1 in the commutative ring $Q ⟦ x ⟧$ gives $x R^{2} + (x - 1) R + 1 = 0$ , and hence $(1 - x - 2 x R)^{2} = (x - 1)^{2} + 4 x (x R^{2} + (x - 1) R) = (x - 1)^{2} - 4 x = 1 - 6 x + x^{2} .$ The series $1 - x - 2 x R$ has coefficient $1$ at the index $0$ , so it lies in $1 + x Q ⟦ x ⟧$ , and $1 - 6 x + x^{2} = 1 + u$ with $u = - 6 x + x^{2} \in x Q ⟦ x ⟧$ ; by the uniqueness clause of [L7] with $k = 2$ it is therefore $(1 - 6 x + x^{2})^{1 / 2}$ as defined in [L8], which gives $2 x R = 1 - x - (1 - 6 x + x^{2})^{1 / 2}$ . No division by $2 x$ occurs, and none is available.

L6L7L8L9step 3.1∎

Remarks

One index range, and it is the whole content. Everything else in this proof is the Motzkin argument with the level step widened. The Motzkin convolution stops at $n - 1$ because a $U$ with its $D$ costs two units of the index, and the Schröder convolution runs to $n$ because in half-length it costs one. A proof that copied the Motzkin range would give a false equation whose first wrong value is $R_{1}$ .
What the source proves and what is proved here. The statement is the source's, in the cleared form; its derivation there goes through a continued fraction, and the first-return argument above is written locally, exactly as in the Motzkin case.

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.50) (standard reference, not scraped)

R(x)=1+x R(x)+x R(x)2R(x)=1+xR(x)+xR(x)2, and 2x R(x)=1−x−(1−6x+x2)1/22xR(x)=1−x−(1−6x+x2)1/2