Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Cn+1=∑i=0nCi Cn−i, with C0=1

Statement

C0=1, and for every n∈N, in N,

Cn+1=∑i=0nCi Cn−i,

the sum being over the finite index set {0,1,…,n} (The sum ∑i∈Sai over a finite index set, and its product form) and Cm=∣Dm∣ the Catalan number (The Catalan number Cn:=∣Dn∣).

Facts & Assumptions

Given: a natural number n, and the set Zn of triples (i,P,Q) with i≤n, P∈Di and Q∈Dn−i.

[F1]

Cm=∣Dm∣, and C0=1 (The Catalan number Cn:=∣Dn∣).

[L1]

The map Θ sending (i,P,Q)∈Zn to the diagonal path whose step word is U, the step word of P, D, the step word of Q, is a bijection Zn→Dn+1 (Every Dyck path of semilength n+1 factors uniquely as U P D Q with P∈Di and Q∈Dn−i).

[L2]

Dm is finite and nonempty for every m∈N (Dn is a finite set).

[L3]

If I is finite and (Ai)i∈I are pairwise disjoint finite sets, then ⋃i∈IAi is finite with ∣⋃i∈IAi∣=∑i∈I∣Ai∣ (The sum rule: a finite disjoint union is finite with ∣A∪B∣=∣A∣+∣B∣ and ∣⋃i∈IAi∣=∑i∈I∣Ai∣, and a sum over a finite index set splits along a partition, clause 2).

[L4]

If A and B are finite then A×B is finite and ∣A×B∣=∣A∣⋅∣B∣ (The product rule: ∣A×B∣=∣A∣ ∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣, clause 1).

[L5]

For a finite index set S and a:S→N, ∑i∈Sai is defined and equals ∑k<n′aφ(k) for any bijection φ:n′→S with n′=∣S∣; taking S=n′ and the identity gives ∑i∈n′ai=∑k<n′ak (The sum ∑i∈Sai over a finite index set, and its product form, clause (a)).

[L6]

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

Proof

technique · direct
1.1F1L2L4L6

For each i with 0≤i≤n put Zn(i):={i}×Di×Dn−i. These sets are pairwise disjoint, since their members differ in the first coordinate, and their union is Zn. Each is finite with ∣Zn(i)∣=CiCn−i: the sets Di and Dn−i are finite by [L2], so [L4] makes the product finite of cardinality CiCn−i by [F1], and pairing with the single element i is a bijection onto Zn(i), which [L6] makes cardinality preserving.

2.1L3L5step 1.1

The index set {0,…,n} is finite, so [L3] applies and gives that Zn is finite with ∣Zn∣=∑i=0nCiCn−i, the sum being the natural-number sum of [L5] over that index set.

3.1F1L1L6step 2.1∎

By [L1] and [L6], Cn+1=∣Dn+1∣=∣Zn∣, which with step 2.1 is the stated identity; and C0=1 by [F1]. At n=0 the identity reads C1=C0C0=1, and at n=1 it reads C2=C0C1+C1C0=2.

Remarks

  • The recurrence determines the sequence, and the definition does not need it. Every value is computable from C0=1 by the displayed convolution, but Cn was defined as a count, so the recurrence is a theorem about that count rather than the object's definition. That is what makes the three closed forms on this page statements rather than restatements.

  • Where the first-return decomposition is spent. Only in the bijection: the sum has one summand for each possible length of the inner block, and the disjointness of the summands is the uniqueness half of that decomposition.

Depends on

Used by

Dependency tree · two levels

34 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