Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

(n+1)Cn=(2nn)

Statement

For every nN, in N,

(n+1)Cn=(2nn).

Facts & Assumptions

Given: a natural number n.

[F1]

Cn+(2nn+1)=(2nn) in N (Cn+(2nn+1)=(2nn)).

[L2]

m!0 for every mN, and σ(m)!=m!σ(m) (The factorial n! and the falling factorial nk, defined by recursion in N).

[L4]

For all x,y,kN with k0: if xk=yk then x=y (Cancellation for multiplication by a nonzero factor).

[L5]

For all x,y,kN: if x+k=y+k then x=y (Addition is cancellative).

Proof

technique · direct
1.1

First, (n+1)(2nn+1)=n(2nn) in N. For n=0 both sides are 0, since (01)=0 by [L3]. For n1 one has n+12n and 2n(n+1)=n1, so [L1] gives (2nn+1)(n+1)!(n1)!=(2n)! and (2nn)n!n!=(2n)!; writing (n+1)!=(n+1)n! and the second factor n!=n(n1)! by [L2], the two left sides read (n+1)(2nn+1)n!(n1)! and n(2nn)n!(n1)!, and cancelling the nonzero factor n!(n1)! by [L2] and [L4] gives the identity.

L1L2L3L4algebra
2.1

Multiply [F1] by n+1: (n+1)Cn+(n+1)(2nn+1)=(n+1)(2nn). By step 1.1 the second summand on the left is n(2nn), and the right-hand side is n(2nn)+(2nn), so cancelling the common summand n(2nn) by [L5] gives (n+1)Cn=(2nn). At n=0 this reads C0=(00)=1.

F1L3L5step 1.1algebra

Remarks

  • The quotient form. The identity is an identity of natural numbers. Reading each natural number as its canonical natural in R (The canonical natural ι(n)=n1F of a field) and dividing by the nonzero real n+1 turns it into the familiar Cn=1n+1(2nn). The multiplicative form is the one proved, and it is the form in which no division and no embedding is needed; it also says at once that n+1 divides the central binomial coefficient, which the quotient form presupposes.

  • What the proof actually uses. Only the reflection identity and factorial bookkeeping. The Catalan number is never manipulated as a formula: it enters as the count it was defined to be and leaves as a factor of a binomial coefficient.

Depends on

Used by

Dependency tree · two levels

37 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