Alphabeta Math
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.

M(x)=1+xM(x)+x2M(x)2, and 2x2M(x)=1x(12x3x2)1/2

Statement

In Qx the Motzkin generating function (Motzkin paths, Schröder paths, the Motzkin numbers Mn, the large Schröder numbers Rn, and their generating functions) satisfies

M=1+xM+x2M2,

and, with (12x3x2)1/2 the formal binomial power of Formal exponential, logarithm, and binomial powers over a commutative Q-algebra,

2x2M=1x(12x3x2)1/2,

the series 1x2x2M being the unique element of 1+xQx whose square is 12x3x2 (Every 1+u with uxRx has a unique kth root with constant coefficient 1 in a commutative Q-algebra).

Facts & Assumptions

[F1]

Motm 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)0 for every im; each such path advances the first coordinate by 1 at every step; Mm=Motm is finite; M0=1 and M1=1; and M(x)=m0Mmxm (Motzkin paths, Schröder paths, the Motzkin numbers Mn, the large Schröder numbers Rn, 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 Qx is a commutative Q-algebra (The Catalan generating function C(x)=n0Cnxn in Qx).

[L1]

For a step set S, a point P and N, the map sending a lattice path to its step word is a bijection LS(P;)S (For each start point the step word is a bijection onto Sn).

[L2]
[L3]

If A and B are finite and disjoint then AB=A+B; and if I is finite and (Ai)iI are pairwise disjoint finite sets then iIAi=iIAi (The sum rule: a finite disjoint union is finite with AB=A+B and iIAi=iIAi, 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×B is finite and A×B=AB (The product rule: A×B=AB, and i<mAi=i<mAi, clause 1).

[L5]

For a finite index set S and a:SN the sum iSai is defined, and iai=0 (The sum iSai over a finite index set, and its product form, clause (c)).

[L6]

[xm](f+g)=[xm]f+[xm]g; f=g if and only if [xm]f=[xm]g for every m; [xm](xkf)=[xmk]f for km and 0 for k>m; and [xm](fg)=i=0m[xi]f[xmi]g (Coefficient extraction is R-linear, separates formal series, shifts under multiplication by xk, and converts products to finite convolution).

[L7]

For a commutative Q-algebra R, uxRx and k1, there is a unique v1+xRx with vk=1+u, namely v=(1+u)1/k (Every 1+u with uxRx has a unique kth root with constant coefficient 1 in a commutative Q-algebra).

[L8]

For uxRx and cR the formal binomial power is (1+u)c:=exp(clog(1+u)) (Formal exponential, logarithm, and binomial powers over a commutative Q-algebra).

[L9]

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

[L10]

If A is finite and f:AB is a bijection then B is finite and B=A (The cardinality A of a finite set).

[L11]

Every nonempty subset SN has a least element (The well-ordering principle).

Proof

technique · direct
1.1

First-return decomposition. Let vMotn+1 with step word w and heights h. Its first step is not D, since h(1)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 w1wn has heights h(1+j), so it lies in Motn. If it is U then h(1)=1; the set of positive indices jn+1 with h(j)=0 contains n+1, so by [L11] it has a least element τ2, and h(τ1)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 w1wi has heights h(1+j)10 ending at h(τ1)1=0, so PMoti, and the path Q of length n1i with step word wτwn has heights h(τ+j)0 ending at 0, so QMotn1i, with 0in1 because τn+1. Conversely, prepending L to a member of Motn, and sending (i,P,Q) to the path with step word U, that of P, D, that of Q, produce members of Motn+1 whose first-return data are the ones started from; the two constructions are two-sided inverses, so by [L1] and [L2] the set Motn+1 is in bijection with the disjoint union of Motn and the sets {i}×Moti×Motn1i for 0in1.

F1L1L2L11
2.1

Counting the two sides of step 1.1 with [F1], [L3], [L4], [L5] and [L10] gives, in N, Mn+1=Mn+i=0n1MiMn1i, the sum being over the finite index set {0,,n1}. At n=0 that index set is empty and the sum is 0, so M1=M0=1, which is correct because a path of length 1 beginning with U cannot return to height 0. At n=1 it gives M2=M1+M0M0=2, at n=2 it gives M3=M2+M0M1+M1M0=4, and at n=3 it gives M4=M3+M0M2+M1M1+M2M0=9.

F1L3L4L5L10step 1.1
3.1

Comparing coefficients gives the functional equation. At the index 0: [x0](1+xM+x2M2)=1 by [L6], and [x0]M=M0=1. At an index n+1: [xn+1](xM)=[xn]M=Mn, while [xn+1](x2M2) is [xn1](M2)=i=0n1MiMn1i when n1 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 [xn+1](1+xM+x2M2)=Mn+1=[xn+1]M. Extensionality in [L6] gives M=1+xM+x2M2.

F1F2L6L9step 2.1
4.1

Rearranging step 3.1 in the commutative ring Qx gives x2M2+(x1)M+1=0, and hence (1x2x2M)2=(x1)2+4x2(x2M2+(x1)M)=(x1)24x2=12x3x2. The series 1x2x2M has coefficient 1 at the index 0, so it lies in 1+xQx, and 12x3x2=1+u with u=2x3x2xQx; by the uniqueness clause of [L7] with k=2 it is therefore the series (12x3x2)1/2 of [L8], which gives 2x2M=1x(12x3x2)1/2. No division by 2x2 occurs, and none is available: that series has coefficient 0 at the index 0 and is not a unit.

L6L7L8L9step 3.1

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 UPDQ with PDi and QDni 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 xM, and the pair of a U with its matching D contributes the factor x2: two units of length for one pair. The convolution index therefore stops at n1 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