OreAlgebraLean verification blueprint

1 Section 2: classical Stirling identity

Theorem 1 Section 2 closed form
#

For all \(m \ge 2\) and \(n \ge 0\),

\[ F(m,n) \; =\; \sum _k (-1)^{n-k}\binom {k}{m}\, S_1(m,k+1) \; =\; \tfrac 12 (n+1)(n+2)\, S_1(m,n+2). \]

Outline: pointwise certificate \(\Rightarrow \) telescoping and range reconciliation \(\Rightarrow \) boundary identity \(\Rightarrow \) both \(F\) and the closed form satisfy the six-term recurrence ; uniqueness of recurrence solutions closes the argument.