5 Section 3, Id. 4: fully deformed variant (Carlitz-weighted resolution)

Theorem 9 Id. 4, printed statement valid under the Carlitz weight

Let \(\hat S_1(n,k) := q^{-\binom n2} S_1^q(n,k)\) (Carlitz weight; equivalently the Katriel signed \(S_1^{(q)}(n,k)=q^{1-n}S_1(n{-}1,k{-}1)-q^{1-n}[n{-}1]_q\, S_1(n{-}1,k)\)). For all \(q : \mathbb {Q}\) with \(q \neq 0\), \(F(m,n)=\sum _k (-1)^{n-k}\binom {k}{m}_q \hat S_1(n,k)\, q^{-k}\) satisfies the printed recurrence

\[ -(q-1)q^{n+1}F(m{+}1,n{+}1) + q(-q^m+q^{m+1}+q^n-1)F(m{+}1,n) + (q-1)F(m,n) = 0. \]

Moreover, for \(q\) with \(q \neq 0\) and \(q^{m+1} \neq 1\), the recurrence is telescoped by the printed certificate

\[ g(m,n,k)=-\frac{(-1)^{n-k}(q-1)q(q^k-q^m)}{q^{m+k}(q^{m+1}-1)}\binom {k}{m}_q \hat S_1(n,k-1), \]

i.e. \(L(f)(m,n,k) = g(m,n,k{+}1) - g(m,n,k)\) pointwise, where \(f\) is the Id. 4 summand and \(L\) the printed operator. This certificate identity is verified in exact rational arithmetic by cas/derive_id4_follow_paper.py Parts G.2–G.3 and is formalized in Lean as (interior rows by the conjugation of the corrected Id. 3 pointwise certificate ; boundary rows \(k = m\) and \(k = n\) by the Id. 3 boundary identities and ; the range edge \(k = n+1\) by and the weight step ; the lower-support zero ).

The condition \(q^{m+1} \neq 1\) on the certificate is forced by its \(q^{m+1}-1\) denominator. For example, at \((q,m,n,k) = (-1,1,3,2)\) one has \((-1)^{m+1}-1 = 0\) and the pointwise identity \(L(f)(m,n,k) = 2\) cannot equal the right-hand side, which involves \(1/0\) under the exact-arithmetic reading of the display (the sum-level recurrence of Theorem 9 is unaffected: it holds at \(q=-1\) too). The hypothesis \(q \neq 0\) in the theorem is forced by the printed \(q^{m+k}\) denominators of the recurrence coefficients; the certificate needs the further condition \(q^{m+1} \neq 1\). Under the total-function reading of \((q^k)^{-1}\) the statement in fact fails at \(m = n = 0\) when \(q = 0\).

Resolution summary (exact verification, cas/derive_id4_follow_paper.py): the Id. 4 summand is the corrected Id. 3 summand conjugated by the column weight \(W(n)=q^{-\binom n2}q^{-n}\); conjugating the corrected Id. 3 telescoper and certificate by \(W\) reproduces the printed Id. 4 operator and certificate exactly (sum-level, and pointwise on the non-degenerate part of the CAS grid, exact rational arithmetic). The printed pair therefore does hold — the paper’s display merely omits the Carlitz weight on \(S_1\). The sum-level identity is proved in Lean (Theorem 9) and the pointwise certificate identity (G.2–G.3) is proved in Lean as , see the paragraph following Theorem 9.

Remark 10 History of the audit

The earlier negative verdict (cas/check_id4_convention.py, cas/search_id4_qanalog.py) searched only the unweighted and Gould-weighted conventions, where the printed pair fails; the Carlitz weight resolves both the recurrence and the certificate. The independent report StirlingNumbers/notes/document.tex reaches the same resolution via the Katriel signed first kind.

Remark 11 Two Id. 4 normalizations

cas/derive_id4_follow_paper.py proves the printed pair for the Carlitz-weighted sum \(\hat S_1(n,k)\, q^{-k}\) above; the merged report StirlingNumbers/notes/document.tex states the same operator/certificate for the Katriel signed \(S_1^{(q)}\) — the same numbers, since \(S_1^{(q),\text{Katriel}}=\hat S_1\).