Paper coverage: Kauers & Schneider, "Symbolic summation for q-series" (Section 2 & 3)

Lean theorem rows below are verified in Lean 4 with no sorry (Mathlib axioms aside). External audit rows are reproducible finite CAS checks tracked by the harness. Historical negative controls concern alternative conventions; they are not failed Lean proofs.

Trusted? column key:

Reproduce with:

lake build                                   # Lean: all theorems below
python3 scripts/check_all.py                 # CAS cross-checks (sympy) + OEIS + data gates
python3 scripts/check_blueprint.py          # blueprint ↔ Lean declaration links

Section 2 — classical Stirling identity

Section 3, Id. 1 — q-Stirling second kind (printed statement, valid as printed)

Section 3, Id. 2 — printed form proved under the Katriel reading, boundary layer included

The paper's printed Id. 2 reads $F(m,n) = \sum_{k} (-1)^{n-k}\cdot \binom{k}{m}\cdot S_1(n,k)\cdot q^{-k} = (-1)^{n-m}\cdot S_1(n+1,m+1)$ with a weighted first kind. Once S1 is read as the Katriel-weighted first kind $S_1^K(n,k) = q^{-\binom{n}{2}}\cdot S_1^q(n,k)$ (recursion step $S_1^K(n+1,k+1) = q^{-n}\cdot (S_1^K(n,k) - [n]_q\cdot S_1^K(n,k+1))$), the printed statement holds for q ≠ 0:

• cas/check_id2_katriel.py (exact rationals, q-grid incl. $-1$) verifies both the printed identity and the paper's printed 3-term recurrence $-(q-1)\cdot q^{n+1}\cdot F(m+1,n+1) + (q-1)\cdot F(m,n) + (q^{n+1}-1)\cdot F(m+1,n) = 0$;
• structurally, the printed summand is termwise the $q^{-n(n+1}/2)$-conjugation of the unweighted sum (the column weight depends on n only, so conjugation maps the verified $q^{n-k}$·$S_1^q$ identity to the printed $q^{-k}$·$S_1^K$ identity and transports the recurrence coefficients accordingly);
• the paper's printed certificate $(-1)^{n-k}\cdot (m-k)(q-1)q^{1-k}/(m+1)\cdot \binom{k}{m}\cdot S_1^K(n,k-1)$ is correct as printed under this weighted $S_1^K$ reading: it equals $-(q-1)\cdot t(n)$ times the corrected unweighted certificate below for $k \le n$ and passes the pointwise and boundary checks in cas/check_id2_katriel.py. (An earlier negative audit omitted the $(-1)^{n-k}$ sign and checked a different operator; the corrected certificate is what the Lean proof uses directly. Lean proves the printed pointwise identity on $k+1 \le n$; see the Katriel-transport rows below.)

Boundary layer now proved too: the weighted transport of the boundary argument is fully formalized (rows below) — bottom endpoint vanishing (id2_weighted_cert_at_m), upper sentinel shift (id2_sentinel_shift), top endpoint pointwise case (id2_weighted_pointwise_at_top), shifted-range reconciliation with the printed sentinels (id2_weighted_range_reconcile), weighted telescoping (id2_weighted_telescoping), and the printed weighted boundary identity (id2_boundary_weighted).

Historically the first audit (cas/check_id2_convention.py) searched (weighted/unweighted S1) × (summand/RHS q-powers) for a convention satisfying a clean 2-term identity-and-recurrence pair and found exactly one hit — $q^{n-k}$ summand, unweighted $S_1^q$, $q^{0}$ RHS — which is the convention the Lean proof adopts (all q : ℚ, incl. $q = 0$ where the rescaling view degenerates). That search's "printed fails" verdict applies to unweighted readings only; the Katriel reading above resolves the printed statement positively.

Section 3, Id. 3 — printed statement proved (classical-S1 reading); corrected generic-q and gemini companion analogs also proved

Re-reading the paper shows Id. 3 uses the classical signed Stirling numbers S1(n,k) (not $S_1^q$) with the printed power $q^{-k}$. Under that reading the printed statement is sound and is now fully proved in Lean (cas/check_id3_convention.py sections 1–5 remain documented negatives only for the earlier (wrong) $S_1^q$ readings; its section 6 verifies the classical-S1 reading). Three statements coexist in the blueprint:

1. thm:id3-printed — the printed statement (classical S1, printed certificate), proved for q ≠ 0 with $q^{m+1} \neq 1$; the $q = 1$ column reduces to classical identity (8).
2. thm:id3 — a corrected generic-q analog (qStirling1Tilde, $q^{n-k}$ summand), kept as an independent q-analog slice, no longer a "repair" of Id. 3.
3. thm:id3-gemini — the gemini-review companion convention (rescaled companion T̃), proved in OreAlgebraLib/Papers/KauersSchneider/Section3Id3Gemini.lean.

Printed statement (classical S1)

Corrected generic-q analog (qStirling1Tilde)

Gemini-review companion convention (T̃, rescaled)

Section 3, Id. 4 — printed statement verified under the Carlitz weight

cas/derive_id4_follow_paper.py (exact fractions.Fraction arithmetic) shows the printed Id. 4 telescoper and printed certificate hold once the first-kind q-Stirling numbers carry the Carlitz weight $Ŝ₁(n,k) := q^{-n(n-1}/2)\cdot S_1ᵠ(n,k)$; the printed Id. 4 summand is the corrected Id. 3 summand conjugated by a column weight, so the earlier "subsumed by corrected Id. 3" verdict was a historical audit stage (unweighted / Gould-weighted conventions only), superseded by this resolution.

Scope notes: the Lean-proved recurrence holds for all q ≠ 0; the printed certificate additionally needs $q^{m+1} \neq 1$ (its denominator $q^{m+1} - 1$ vanishes otherwise, e.g. at $q = -1, m = 1$). The certificate pointwise identity is verified by cas/derive_id4_follow_paper.py Parts G.2–G.3 and Lean-formalized as id4_pointwise ($m \le k \le n+1$): interior rows by conjugation (id4_op_summand_conj, id3c_pointwise, id4_cert_conj), boundaries $k = m$/$k = n$ via the Id. 3 boundary identities id3c_op_left/id3c_op_right, and the range edge $k = n+1$ via id3c_cert_at_n1 and the weight step id4T_succ.

Section 3, Item 5 — q-Worpitzky identity (Lean proof, degenerate cases covered)

Closing Remark — negative for q-Stirlings, POSITIVE for classical S1 (Milestones 13–14)

The paper's closing Remark (6-term/3-step operator) is not consistent with any S1 convention matching the printed S1_q summand (unweighted qStirling1, Gould-weighted); in those conventions the statement is a documented negative (cas/check_remark_convention.py, Milestone 13).

Status update (Milestone 14): the Remark is correct AS PRINTED for the classical signed S1 reading. With $S_1(n,k) = S_1(n-1,k-1) - (n-1)\cdot S_1(n-1,k)$ and the printed summand $k\cdot (-1)^{n-k}\cdot (k choose m)_q\cdot S_1(n,k)\cdot q^{-k}$, exact-rational CAS verification (cas/check_remark_classical.py) shows:

1. the printed 6-term recurrence holds on F for the full grid $q \in {2, 3, \tfrac12, \tfrac13, 3/2, \tfrac23, -1}$, $m \le 4$, $n \le 8$ (210 rows — a polynomial identity in q, so the certificate-free rows are all valid checks);
2. the printed certificate (inner factor $q^m$) satisfies the pointwise identity $L(f)(m,n,k) = g(m,n,k+1) - g(m,n,k)$ exactly (870 checks over 270 non-degenerate rows);
3. the lower boundary is exact: $g(m,n,m) = 0$;
4. the upper boundary closes by edge-shift cancellation: with E(m,n) the $k = n+1$ sentinel terms of the shifted columns, $g(m,n,n+1) = -E(m,n)$, and the series-form operator equals the pointwise sum plus E(m,n) — so the telescoping proof goes through unchanged.

The initial-values table of the classical-S1 sum matches the external (gemini-review draft) transcript. Note the draft's display of the certificate uses inner factor $q^{m+k}$; that is the mis-transcription — the paper's printed inner factor $q^m$ is the correct one. Also as printed, the certificate denominator $(1-q^{m+1})(1-q^{m+2})$ vanishes whenever $q^{m+1} = 1$ (in particular for every m at $q = -1$, and at $q = 1$); those columns are outside the certificate domain and excluded from parts 2–4, while part 1 (the recurrence) is polynomial in q and verified there too; 5. (Lean, Milestone 14 follow-up) the $q^n$-rescaled, denominator-free series form vanishes on the entire (q, m, n) grid — no hypotheses: the empty rows n < m and the diagonal $n = m$ are direct (remarkOpSeriesR_eq_zero_empty, remarkOpSeriesR_eq_zero_diag; the diagonal closes through the q-independent singleton values $-(m+2) + 2(m+1) - m = 0$), and the main rows m < n lift from 0 < q < 1 to all of ℚ by a polynomial lift in ℚ[X] (remarkOpSeriesR_eq_zero_full); 6. (Lean) the printed recurrence follows for q ≠ 0 alone — no row condition $m + 1 \le n$, no certificate hypotheses $q^{m+1} \neq 1$, $q^{m+2} \neq 1$ (remark_recurrence), matching part 1b of the audit, which covers the degenerate parameters at $q \in {0, 1}$ on the full (m, n) grid (223 checks; at $q = 0$ the rescaled operator is the object checked, since the printed $q^{-k}$ weight degenerates there); 7. (Lean, Milestone 14 closing) the printed-object transport layer is complete: the printed certificate remarkGcert (over the printed denominator $-q^{m+1} - q^{m+2} + q^{2m+3} + 1 = (1 - q^{m+1})\cdot (1 - q^{m+2})$), the printed six-term operator remarkOpPrinted, and the printed edge-shift remarkPrintedEdge are defined; the bridge remarkGp_eq proves $G_p = q^{n+2m}\cdot remarkDs\cdot g$ on the certificate domain (q ≠ 0, $q^{m+1}, q^{m+2} \neq 1$, $k \le n+1$; weight identity cert_weight_id); and from it follow the printed pointwise identity remark_pointwise ($op(k) = g(k+1) - g(k)$; certificate-domain small case remark_pointwise_small_printed at $k = 1$), the lower boundary $g(m) = 0$ (remark_certificate_lower, all q), the upper boundary $g(n+1) = -E(m,n)$ (remark_certificate_upper), the telescoping theorem remark_telescoping ($\sum_{k}=m+1}^{n} op(k) = g(n+1) - g(m+1)$), and the printed $k = m$ endpoint: the hypothesis-free rescaled column identity remark_pointwise_at_m transports through the bridge to remark_pointwise_at_m_printed ($op(m) = g(m+1) - g(m)$ for $m \le n$), giving the full-range pointwise identity remark_pointwise_full ($m \le k \le n$) and the full telescoping remark_telescoping_full ($\sum_{k}=m}^{n} op(k) = g(n+1) - g(m)$, including the lower endpoint contribution — nonzero in general: $op(1) = -1/2$ at (2,1,2) — and the diagonal rows) — closing the Remark's printed certificate proof exactly as in the CAS audit.

The natural rescaled target variant's companion-T̃ Id. 3 slice is Lean-proved (section3Id3_gemini_identity).

Companion report audit (StirlingNumbers/notes/document.tex)

The step-by-step verification report on the gemini-review branch was checked claim-by-claim with exact symbolic computation (sympy, rational arithmetic in q, $n, m \le 6$). Verdicts:

• Identity 3: sum-level recurrence $F + q(q^m + n)F(m+1,n) - qF(m+1,n+1) = 0$, initial-values table, and closed-form induction hold.
• Identity 4: sum-level recurrence under Katriel's convention and the initial values hold.
• Closing Remark: order-(2,2) recurrence and table hold.
• Two printed closed-form recurrences were off by one in the index and have been corrected (see the document):
• Id. 3 (eq:def-Stilde): coefficient $q^k + n$ → $q^{k-1} + n - 1$;
• Id. 4 (eq:def-Sbar): coefficients $q^k, q^n, q^-(n+1)$ → $q^{k-1}, q^{n-1}, q^-n$, and its first term must read the previous row $$\bar S_1^{(q)}(n,k+1)$$ (the same-row reading sbar(n+1,k) printed in the original commit is wrong).

With the corrections, the derived recurrences reproduce the sums exactly (0 mismatches for all parts (a)–(e), 330 point checks per part across $q \in {2, 1/2, 3/2, 2/3, -1}$), confirming the tables in the document.

Companion report: Lean formalization (Section3Report.lean)

The report's own restatement of Id. 3 / Id. 4 — the signed array convention $G(n,m) = (-1)^{n-m}F(m,n)$ — is also formalized in Lean, in OreAlgebraLib/Papers/KauersSchneider/Section3Report.lean (kernel-checked, no sorry), on top of the Section 3 / Section 3 Id. 4 modules:

The report's pointwise certificates remain unformalized in Lean; the exact-rational audit script cas/check_report_document_audit.py verifies all parts (a)–(e) with 0 violations, including the corrected tilde and S-bar