6 Section 3, companion report: the signed array form

The module OreAlgebraLib/Papers/KauersSchneider/Section3Report.lean provides signed-array wrappers \(G(n,m)=(-1)^{n-m}F(m,n)\) for the corrected \(q\)-Stirling Id. 3 sum and the Carlitz-weighted Id. 4 sum. Its Id. 3 sum is different from the report’s classical-\(S_1\) sum; the latter companion is treated in Section3Id3Gemini.lean.

Theorem 12 Report Id. 3: signed array closed form

With \(G(n,m) = (-1)^{n-m} F(m,n)\) and \(F\) the corrected Id. 3 sum,

\[ G(n,m) = \tilde S_1^q(n+1,m+1), \]

i.e. the signed-array closed form of the corrected sum equals its Id. 3 companion (Theorem 6); and the corrected sum satisfies the F-level step \(F(m{+}1,n{+}1) = F(m,n) + ([n{+}1]_q + q^{m+1} - 1)\, F(m{+}1,n)\).

Theorem 13 Report Id. 4: printed recurrence and closed form

For the Carlitz-weighted sum \(\hat F\) (Theorem 9), the printed Id. 4 sum-level recurrence

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

holds for all \(q \neq 0\), and the signed array satisfies \(\hat G(n,m) = q^{-n(n+1)/2}\, \tilde S_1^q(n+1,m+1)\) (the report’s column-weighted closed form, Theorem 9 in signed-array form).

The report’s pointwise certificates (the \(g(m,n,k)\) of the report’s Steps 2, Id. 3 boundary estimate, and closing Remark) involve denominators \(q^{m+1}-1\) that vanish on the degenerate columns; their Lean formalization is future work (the accompanying exact-rational audit script cas/check_report_document_audit.py reports zero mismatches on corrected parts (b’), (d’) and (e); only the historical companion formulas remain negative controls). (Milestone 14 formalizes the closing Remark’s classical reading; see below.)