OreAlgebraLean verification blueprint

4 Section 3, Id. 3: printed statement (classical \(S_1\)), proved; plus corrected generic-\(q\) analogs

Theorem 5 Id. 3, printed — classical \(S_1\) reading
#

As printed, Id. 3 uses the classical signed Stirling numbers \(S_1(n,k)\) (not \(S_1^q\)). For all \(q:\mathbb {Q}\), with \(f(m,n,k)=(-1)^{n-k}\binom {k}{m}_q S_1(n,k) q^{-k}\) and the printed certificate \(g(m,n,k)=-(-1)^{n-k}\frac{q(q^k-q^m)}{q^{m+k}(q^{m+1}-1)}\binom {k}{m}_q S_1(n,k-1)\):

\[ f\text{-operator: } \qquad F(m,n) + q(q^m+n)F(m+1,n) - qF(m+1,n+1) = 0, \]

proved pointwise via \(L(f)(m,n,k)=g(m,n,k+1)-g(m,n,k)\) for all \(k\in [m,n]\) and the sentinel balance \(g(m,n,n+1)=q\, f(m+1,n+1,n+1)\). At \(q=1\) the sum equals \((-1)^{n-m}S_1(n+1,m+1)\) (identity (8)).

Theorem 6 Id. 3, corrected generic-\(q\)
#

Let \(\tilde S_1^q\) satisfy \(\tilde S_1^q(n+1,k+1)=\tilde S_1^q(n,k)-([n]_q+q^k-1)\tilde S_1^q(n,k+1)\), \(\tilde S_1^q(n,n)=1\). For all \(q:\mathbb {Q}\):

\[ F(m,n) \; =\; \sum _k (-1)^{n-k}\binom {k}{m}_q\, S_1^q(n,k)\, q^{\, n-k} \; =\; (-1)^{n-m}\, \tilde S_1^q(n+1,m+1). \]

Note: this corrected generic-\(q\) statement is an independent q-analog slice, kept alongside the (now proved) printed classical-\(S_1\) statement above; it is no longer a "repair" of Id. 3.

At \(q=1\) this reduces to the classical identity (8): .

Remark 7 Id. 3 alternate convention
#

The printed Id. 3 of the paper states \(F(m,n) = \sum _k (-1)^{n-k}\binom {k}{m}_q S_1(n,k)\, q^{-k}\) with the classical-weighted \(S_1\) and the \(q\)-binomial \(\binom {k}{m}_q\), and the printed right-hand side \((-1)^{n-m}\tilde S_1(n+1,m+1)\) with \(\tilde S_1\) satisfying the deformed recurrence \(\tilde S_1(n+1,k+1) = \tilde S_1(n,k) - ([n]_q + q^k - 1)\tilde S_1(n,k+1)\). Under the Carlitz rescaling \(\tilde S_1(n,k) = q^{-\binom n2} S_1(n,k)\) and the index shift \(q^{-k} \mapsto q^{n-k}\), the printed summand equals the verified one up to the column weight \(q^{-\binom n2}\): the printed identity holds for the verified convention above; the printed form needs the same weight applied to \(S_1\) to be valid.

Theorem 8 Id. 3, gemini-review companion convention
#

Let \(S_1(n,k) = S_1^{(1)}(n,k)\) be the classical signed first-kind number and let \(q^{-\binom n2}T\) be the companion of the companion report (StirlingNumbers/notes/document.tex): in its polynomial normalization \(\tilde T\) satisfies \(\tilde T(0,0)=1\), \(\tilde T(n+1,k+1)=\tilde T(n,k)-(q^{k-1}+(n-1)q)\, \tilde T(n,k+1)\). For all \(q:\mathbb {Q}\) (including \(q=0\)) the rescaled sum

\[ G(m,n) \; =\; \sum _k (-1)^{n-k}\binom {k}{m}_q\, S_1^q(n,k)\, q^{\, n-k} \; =\; (-1)^{n-m}\, \tilde T(n+1,m+1). \]

For \(q \neq 0\) this is \(q^n\) times the report’s \(F(m,n) = \sum _k (-1)^{n-k}\binom {k}{m}_q S_1(n,k) q^{-k}\). The certificate \(g(k) = (-1)^{n+1-k}\binom {k}{m+1}_q S_1(n,k-1)\, q^{\, n+1-k}\) telescopes the operator \(f(m{+}1,n{+}1,\cdot ) - f(m,n,\cdot ) - (q^{m+1}+nq)\, f(m{+}1,n,\cdot )\) for all \(m+1 \le k \le n\) including the near-diagonal endpoint \(k=n\), so no separate boundary identity is needed.

The convention and the printed companion’s off-by-one defect (the coefficient \(q^k+n\) instead of \(q^{k-1}+(n-1)q\)) are verified in exact rational arithmetic by cas/check_id3_gemini_tilde.py Parts (A)–(C); the Lean development (OreAlgebraLib/Papers/KauersSchneider/Section3Id3Gemini.lean) mirrors the report’s proof idea as a formal derivation of the closed form through the rescaled step-4 recurrence.