Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-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.

Dn is a finite set

Statement

For every nN the set Dn of Dyck paths of semilength n (Dyck paths of semilength n) is finite and nonempty; more precisely Dn has at least one and at most 22n elements.

Facts & Assumptions

Given: a natural number n.

[F1]

Dn is the set of diagonal paths of length 2n from (0,0) to (2n,0) whose height function satisfies h(i)0 for every i with 0i2n (Dyck paths of semilength n).

[F2]

A diagonal path of length from (0,α) is the same datum as a function h:{0,,}Z with h(0)=α and h(i)h(i1){1,1} for 1i (Diagonal lattice paths with steps U=(1,1) and D=(1,1), and the height function).

[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, and LS(P;) is finite with LS(P;)=S (For each start point the step word is a bijection onto Sn).

[L2]

For finite sets A and B, the set AB of functions BA is finite and AB=AB (The set AB of functions BA between finite sets is finite, with AB=AB).

[L3]

A subset of a finite set is finite, and a subset S of a finite set A has SA (A subset of a finite set is finite, with BA, and equality holds if and only if B=A, clauses 1 and 2).

[L4]

A property that holds at 0 and passes from every natural number to its successor holds at every natural number: if a property P satisfies P(0) and (P(n)P(σ(n))) for all n, then P(n) holds for all nN (The principle of mathematical induction).

Proof

technique · direct
1.1

The set W((0,0);2n) of all diagonal paths of length 2n from the origin is finite with exactly 22n elements, since the step set {U,D} has two elements.

L1L2
1.2

The word w of length 2n with wj=U for even j and wj=D for odd j traces a Dyck path: its height function satisfies h(0)=0, and if h(2k)=0 with 2k<2n then h(2k+1)=1 and h(2k+2)=0, so by induction on k every even index has height 0 and every odd index height 1; hence h0 throughout and h(2n)=0.

F1F2L4construct
2.1

By [F1] the set Dn is a subset of the finite set of step 1.1, hence finite with at most 22n elements by [L3]; and it is nonempty by step 1.2, so it has at least one element.

F1L3step 1.1step 1.2

Remarks

  • What this lemma is for. It is the well-definedness obligation behind the Catalan numbers: Dn is a natural number only because Dn is finite, and the cardinality notation is defined for finite sets alone.

  • The bound 22n is not the point. It is the crude count of all words of length 2n over a two-letter alphabet, recorded because it is what makes the set finite; the exact count is the subject of the theorems below and is far smaller.

Depends on

Used by

Dependency tree · two levels

28 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