TheoremStatement: Literature-sourcedProof: 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.

Worpitzky's identity for $n \geq 1$

Statement

For every $n, m \in N$ with $n \geq 1$ ,

$m^{n} = \sum_{k = 0}^{n - 1} A (n, k) (\binom{m + k}{n}) .$

Facts & Assumptions

Given: Naturals $n$ and $m$ .

[L1]

The Eulerian numbers satisfy $A (n, k) = (k + 1) A (n - 1, k) + (n - k) A (n - 1, k - 1)$ (The Eulerian numbers satisfy $A (n, k) = (k + 1) A (n - 1, k) + (n - k) A (n - 1, k - 1)$ ).

[L2]

Binomial coefficients satisfy $(\binom{N}{r}) = 0$ for $r > N$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ), Pascal's rule $(\binom{N + 1}{r}) = (\binom{N}{r}) + (\binom{N}{r - 1})$ (Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ ), and for $r \leq N$ the closed formula rearranges to $r (\binom{N}{r}) = (N - r + 1) (\binom{N}{r - 1})$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq 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})$ ).

[L3]

$A (1, 0) = 1$ by the definition of Eulerian numbers (Eulerian numbers and Eulerian polynomials).

Proof

technique · induction

1.1

For $n = 1$ , [L3] makes the right-hand side $(\binom{m}{1}) = m = m^{1}$ .

baseL3given

1.2

Assume the identity at $n - 1$ , where $n \geq 2$ , and write $W_{n} (m) : = \sum_{k = 0}^{n - 1} A (n, k) (\binom{m + k}{n})$ .

2.1

Using [L1] and shifting the second sum, $W_{n} (m) = \sum_{k = 0}^{n - 2} A (n - 1, k) ((k + 1) (\binom{m + k}{n}) + (n - k - 1) (\binom{m + k + 1}{n}))$ .

step 1.2L1algebra

3.1

Fix $k$ from step 2.1 and put $M : = m + k$ . If $n > M + 1$ , then [L2] gives $(\binom{M}{n}) = (\binom{M + 1}{n}) = (\binom{M}{n - 1}) = 0$ , so the bracket in step 2.1 is $0 = m (\binom{M}{n - 1})$ . If $n = M + 1$ , then $(\binom{M}{n}) = 0$ , $(\binom{M + 1}{n}) = 1$ , and $(\binom{M}{n - 1}) = 1$ , so the same bracket is $(n - k - 1) = m = m (\binom{M}{n - 1})$ . Finally, if $n \leq M$ , then Pascal's rule from [L2] gives $(n - k - 1) (\binom{M + 1}{n}) = (n - k - 1) (\binom{M}{n}) + (n - k - 1) (\binom{M}{n - 1})$ , and the closed-form identity from [L2] gives $n (\binom{M}{n}) = (M + 1 - n) (\binom{M}{n - 1}) = (m + k + 1 - n) (\binom{M}{n - 1})$ . Substituting into the bracket of step 2.1 yields $m (\binom{M}{n - 1})$ . So in every case that bracket simplifies to $m (\binom{m + k}{n - 1})$ .

step 2.1L2algebra

4.1

Steps 2.1 and 3.1 give $W_{n} (m) = m \sum_{k = 0}^{n - 2} A (n - 1, k) (\binom{m + k}{n - 1})$ , and the inductive hypothesis of step 1.2 makes this $m \cdot m^{n - 1} = m^{n}$ .

step 1.2step 2.1step 3.1

5.1

This is the required identity.

step 4.1discharge-induction∎

Depends on

Used by

A(4,2)=11 by the recurrence, by Worpitzky's identity and by excedances Example

Dependency tree · two levels

30 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

Richard P. Stanley, Enumerative Combinatorics, Volume 1, second edition (standard reference, not scraped)
Felix Gotti, MIT 18.211 Combinatorial Analysis, Lecture 13 (standard reference, not scraped)

Worpitzky's identity for n≥1n≥1