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.
Statement
For every , in ,
Facts & Assumptions
Given: a natural number .
For with : in ( for ; hence , the quotient is a natural number, and ).
for every , and (The factorial and the falling factorial , defined by recursion in ).
for , and (The set of -element subsets and the binomial coefficient ).
For all with : if then (Cancellation for multiplication by a nonzero factor).
For all : if then (Addition is cancellative).
Proof
First, in . For both sides are , since by [L3]. For one has and , so [L1] gives and ; writing and the second factor by [L2], the two left sides read and , and cancelling the nonzero factor by [L2] and [L4] gives the identity.
Multiply [F1] by : . By step 1.1 the second summand on the left is , and the right-hand side is , so cancelling the common summand by [L5] gives . At this reads .
Remarks
-
The quotient form. The identity is an identity of natural numbers. Reading each natural number as its canonical natural in (The canonical natural of a field) and dividing by the nonzero real turns it into the familiar . 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 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
- $C_n+\binom{2n}{n+1}=\binom{2n}{n}$
- $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$; hence $\binom{n}{k}\,k! = n^{\underline{k}}$, the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- Cancellation for multiplication by a nonzero factor
- Addition is cancellative
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
Used by
- n+1 divides C(2n, n) for every n∈ℕ Corollary
- The Catalan numbers through C₆, from the recurrence and from the closed formula Example
- The five Dyck paths of semilength 3, with their height functions Example
- FALSE: the monotone paths from (0,0) to (n,n) staying weakly below the diagonal are exactly half of all monotone paths False statement
- FALSE: the quotient C(2n, n)/(n+1) is an integer only for small n False statement
- Why the Catalan count is proved three times, and how the three statements agree Remark
- (2n+1) Cₙ=C(2n+1, n), a second derivation of the Catalan count Theorem
- A third derivation of (n+1) Cₙ=C(2n, n), from the closed form of C(x) Theorem
- The Chung–Feller theorem: for each k with 0≤ k≤ n, exactly Cₙ of the diagonal paths from (0,0) to (2n,0) have exactly 2k steps lying above level 0 Theorem
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
- D. Guichard, An Introduction to Combinatorics and Graph Theory, §3.5 Catalan Numbers (standard reference, not scraped)
- C. Krattenthaler, "Lattice Path Enumeration", ch. 10 of the Handbook of Enumerative Combinatorics, §10.3 (standard reference, not scraped)