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

The Chung–Feller theorem: for each k with 0≤k≤n, exactly Cn of the diagonal paths from (0,0) to (2n,0) have exactly 2k steps lying above level 0

Statement

Let q be a diagonal lattice path of length ℓ with height function h (Diagonal lattice paths with steps U=(1,1) and D=(1,−1), and the height function). Its steps are the indices i with 1≤i≤ℓ, the step i passing from height h(i−1) to height h(i); it is an up step when h(i)=h(i−1)+1 and a down step when h(i)=h(i−1)−1. The step i lies above level 0 when h(i−1)≥0 and h(i)≥0, and lies below level 0 otherwise. Every step is exactly one of the two.

Let n∈N. Then every q∈W((0,0),(2n,0)) has an even number of steps above level 0, say 2k with 0≤k≤n; and for each k with 0≤k≤n the set

Fn,k:={ q∈W((0,0),(2n,0)):q has exactly 2k steps above level 0 }

is finite with

∣Fn,k∣=Cn

(The Catalan number Cn:=∣Dn∣). In particular the count does not depend on k.

Facts & Assumptions

Given: a natural number n; the set W of words of length 2n+1 over {1,−1} with exactly n entries −1, so with n+1 entries 1; the subset U⊆W of words whose entry at the position 0 is 1; and for a word w of length 2n+1 over {1,−1} the statistic κ(w):=∣{ i:0≤i≤2n, wi=1, ∑i′<iwi′≤0 }∣.

[F1]

A diagonal path of length ℓ from (0,α) is the same datum as a function h:{0,…,ℓ}→Z with h(0)=α and h(i)−h(i−1)∈{1,−1} for 1≤i≤ℓ; with μ(i) the number of up-steps among the first i its height is h(i)=α+2μ(i)−i (Diagonal lattice paths with steps U=(1,1) and D=(1,−1), and the height function).

[F2]
[F3]

∥a∥=∑i<mai; (σja)i=a(i+j) mod m; Sa(0)=0; Sa(j)−Sa(j−1)=a(j−1) mod m; Sa(j+m)=Sa(j)+∥a∥; and the finite sum satisfies ∑i<0ci=0 and ∑i<r+1ci=∑i<rci+cr (Cyclic shifts of an integer word and its periodic partial-sum function).

[L1]

If m≥1 and ∥b∥=1, then l↦∣{ r:0≤r<m, Sb(l+r)≤Sb(l) }∣ is a bijection from {0,…,m−1} onto {1,…,m} (If ∥a∥=1 then j↦#{r:0≤r<m, Sa(j+r)≤Sa(j)} is a bijection from {0,…,m−1} onto {1,…,m}).

[L2]

If gcd⁡(∥a∥,m)=1 then the stabiliser of a under the shift action of Z/m is {[0]m} and the orbit of a has exactly m elements (If gcd⁡(∥a∥,m)=1 then the shift stabiliser of a is trivial, so its orbit has exactly m elements).

[L3]

For every letter x the number of positions of σja carrying x equals the number of positions of a carrying x, and [j]m⋅a:=σja is a left action of Z/m on the words of length m (Cyclic shifting is an action of Z/m on the words of length m over a set, clauses 2 and 3).

[L4]

For a left action of G on X the relation x∼y given by y=g⋅x for some g∈G is an equivalence relation, its class at x is the orbit of x, and the distinct orbits partition X (The orbits of a group action are the equivalence classes of x∼y iff y=g⋅x for some g, and hence partition the acted-on set).

[L5]

For ∥a∥≥1, j∈Z and 0≤r≤m: ∑i<r(σja)i=Sa(j+r)−Sa(j) (σja has all partial sums positive exactly when Sa(i)>Sa(j) for every i>j, clause 1).

[L6]

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

[L7]

For a finite set A and k′∈N, [A]k′ is the set of k′-element subsets of A, and ∣[A]k′∣=(∣A∣k′) (The set [A]k of k-element subsets and the binomial coefficient (nk):=∣[n]k∣).

[L8]

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).

[L9]
[L10]

If A and B are finite and disjoint then ∣A∪B∣=∣A∣+∣B∣; and if I is finite and (Ai)i∈I are pairwise disjoint finite sets then ∣⋃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, clauses 1 and 2).

[L11]

For a constant natural number c and a finite index set S, ∑i∈Sc=∣S∣⋅c (The sum ∑i∈Sai over a finite index set, and its product form, clause (c)).

[L12]

If A is finite and f:A→B is a bijection then B is finite and ∣B∣=∣A∣; and ∣n′∣=n′ for a natural number n′ (The cardinality ∣A∣ of a finite set).

[L13]

A subset of a finite set is finite, with cardinality at most that of the set (A subset of a finite set is finite, with ∣B∣≤∣A∣, and equality holds if and only if B=A, clauses 1 and 2).

[L15]

Every nonempty subset S⊆N has a least element (The well-ordering principle).

[L16]

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 n∈N (The principle of mathematical induction).

[L17]

For all x,y,c∈N with c≠0: if x⋅c=y⋅c then x=y (Cancellation for multiplication by a nonzero factor).

[L18]

Integers x and y are coprime when gcd⁡(x,y)=1; x and 1 are coprime for every integer x, since gcd⁡(x,1)=1, and the relation is symmetric (Coprime integers: gcd⁡(a,b)=1).

Proof

technique · direct
1.1F1

A step i of a diagonal path joins the two heights h(i−1) and h(i), which differ by exactly 1; writing c for the smaller of them, the step lies above level 0 exactly when c≥0, hence below level 0 exactly when c≤−1. For an up step c=h(i−1) and for a down step c=h(i), so the steps below level 0 are the up steps starting at a height ≤−1 together with the down steps ending at a height ≤−1, and these two families are disjoint because a step cannot be both up and down.

1.2F1L7L8L9L12

Let β(q) be the number of up steps of q∈W((0,0),(2n,0)) starting at a height ≤−1. The map Δ sending w∈U to the diagonal path of length 2n from (0,0) whose step word is w1w2⋯w2n, with 1 read as an up step and −1 as a down step, is a bijection U→W((0,0),(2n,0)): the inverse prepends the entry 1, and by [F1] and [L8] a word of length 2n over the two letters with exactly n up letters is the step word of exactly one diagonal path of length 2n from (0,0), whose height at the last index is 0. Moreover κ(w)=1+β(Δ(w)): writing H(i)=∑i′<iwi′, the path q=Δ(w) has h(i)=H(i+1)−1 for 0≤i≤2n and its step i carries the letter wi, so the position i=0 always contributes to κ(w) because w0=1 and H(0)=0, while a position i≥1 with wi=1 contributes exactly when H(i)≤0, that is exactly when h(i−1)≤−1. Finally U is finite with ∣U∣=(2nn), since deleting the entry at the position 0 is a bijection from U onto the words of length 2n over {1,−1} with exactly n entries −1, and those correspond by [L7], [L9] and [L12] to the n-element subsets of a 2n-element set.

1.3F3L16

Fix a∈W and let t0<t1<⋯<tn be the positions of a carrying the entry 1, extended to all integers by tl+n+1:=tl+(2n+1). Put bl:=Sa(tl+1)−Sa(tl). Then bl+n+1=bl, because Sa(tl+2n+1)=Sa(tl)+∥a∥ by [F3], so b is determined by b0,…,bn and is a word of length n+1 of integers; its weight is ∥b∥=Sa(tn+1)−Sa(t0)=∥a∥, which is 1 because a has n+1 entries 1 and n entries −1. The one-step difference identity of [F3] for b reads Sb(l)−Sb(l−1)=bl−1, so induction on r gives Sb(l+r)−Sb(l)=Sa(tl+r)−Sa(tl) for every l∈Z and every r∈N.

2.1F1L10L12L14L15step 1.1

For q∈W((0,0),(2n,0)) the steps below level 0 number 2β(q), so the steps above level 0 number 2n−2β(q) with 0≤β(q)≤n. Send a down step i with c:=h(i)≤−1 to ψ(i):= the least index i′>i with h(i′)≥c+1, which exists by [L15] because h(2n)=0≥c+1; then h(ψ(i)−1)≤c and h(ψ(i))≥c+1 differ by 1, so h(ψ(i)−1)=c and h(ψ(i))=c+1 and ψ(i) is an up step starting at height c≤−1. The map is injective: if ψ(i1)=ψ(i2)=i′ then h(i1)=h(i′−1)=h(i2), and if moreover i1<i2 then i2−1>i1 with h(i2−1)=c+1, so ψ(i1)≤i2−1<ψ(i2), a contradiction. It is surjective: given an up step i′ with c:=h(i′−1)≤−1, the set of j≤i′−1 with h(j)≥c+1 contains 0 and is bounded above, so by [L14] it has a greatest element j0; then h(j0)=c+1 and h(j0+1)=c, so i:=j0+1 is a down step with h(i)=c≤−1, every index strictly between i and i′ has height ≤c, and ψ(i)=i′. So the two families of step 1.1 are equinumerous by [L12], and [L10] adds them; the number of up steps of q is n by [F1] since h(2n)=0, so β(q)≤n.

2.2F3L1L2L3L5L18step 1.3

The members of the orbit of a that lie in U are exactly the n+1 pairwise distinct words σtla with 0≤l≤n, and κ(σtla) takes each of the values 1,…,n+1 for exactly one such l. Since ∥a∥=1 and 1 is coprime to 2n+1 by [L18], [L2] makes the stabiliser trivial, so the 2n+1 words σja with 0≤j≤2n are pairwise distinct and form the orbit; the entry of σja at the position 0 is aj mod (2n+1), which is 1 exactly for j∈{t0,…,tn}. For such a j=tl, [L5] gives ∑i′<i(σtla)i′=Sa(tl+i)−Sa(tl), and the positions i with 0≤i≤2n at which σtla carries the entry 1 are exactly those with tl+i=tl+r for some r with 0≤r≤n, because tl<tl+1<⋯<tl+n<tl+2n+1 and the integers whose residue carries the entry 1 are exactly the tj. Hence κ(σtla)=∣{ r:0≤r<n+1, Sa(tl+r)≤Sa(tl) }∣, which by step 1.3 is ∣{ r:0≤r<n+1, Sb(l+r)≤Sb(l) }∣; and [L1] applied to b, of length n+1 and weight 1, says that this is a bijection from {0,…,n} onto {1,…,n+1}.

3.1L4L6L10L11L12L13L17step 1.2step 2.2

For 1≤k′≤n+1 put Ik′:={ w∈U:κ(w)=k′ }. By step 2.2, κ takes values in {1,…,n+1} on U and each orbit meets each Ik′ in exactly one word, so U is the union of the pairwise disjoint sets I1,…,In+1, and for each pair k′,k′′ the rule sending w∈Ik′ to the unique member of its orbit lying in Ik′′ is a bijection, the orbits being the classes of an equivalence relation by [L4]. Hence all n+1 sets have the same cardinality, and by [L10], [L11], [L12] and [L13] we get (n+1)∣I1∣=∣U∣=(2nn), which is (n+1)Cn by [L6]; cancelling the nonzero factor n+1 by [L17] gives ∣Ik′∣=Cn for every k′.

4.1F1F2L12step 1.2step 2.1step 3.1∎

By step 2.1 a path q∈W((0,0),(2n,0)) has 2n−2β(q) steps above level 0, an even number, and 0≤β(q)≤n, so the count is 2k for exactly one k with 0≤k≤n, namely k=n−β(q). By step 1.2 the bijection Δ carries { w∈U:κ(w)=n−k+1 } onto Fn,k, since κ(w)=1+β(Δ(w)) and β=n−k; and by step 3.1 that set has exactly Cn elements, so ∣Fn,k∣=Cn by [L12]. At n=1 the two paths from (0,0) to (2,0) have height sequences 0,1,0 and 0,−1,0, with two steps above level 0 and none respectively, so each of k=1 and k=0 is realised once, and C1=1.

Remarks

  • This is not a corollary of the cycle lemma as that lemma is stated here. The cycle lemma counts the cyclic shifts all of whose partial sums are positive, and for weight 1 that is exactly one shift; Chung–Feller needs every shift sorted by how many of its partial sums fail to rise, which is the strictly finer statement If ∥a∥=1 then j↦#{r:0≤r<m, Sa(j+r)≤Sa(j)} is a bijection from {0,…,m−1} onto {1,…,m}.

  • Where the blocking is spent. The word b records only the jumps of Sa between consecutive positions carrying the entry 1. That is what turns a statement about the n+1 shifts of a beginning with 1 into a statement about all n+1 shifts of a word of length n+1, which is the form the transversal lemma is stated in.

  • Why the steps split evenly below the axis. The pairing of step 2.1 matches each descent to level c≤−1 with the next ascent from c, and it is a bijection only because the path ends at height 0: with a free right endpoint a descent below the axis need never be undone, and the count of steps below the axis would not be even.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

89 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