bibkey: kurkov2026a132393 authors: Mikhail Kurkov year: 2026 title: “OEIS A132393: Kurkov’s nested sum for unsigned Stirling numbers” doi: null url: https://oeis.org/A132393 claim: “Conjecture: T(n+m+1,m+1) = (n+m)! * (Product_{i=1..m} (n+i)^i) * Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(n*m + j_1 + j_2 + … + j_m) * (Product_{1 <= q < p <= m} (j_q - j_p + p - q)^2) * Product_{t=1..m} (n+t-1){j_t} / ((n-j_t+t)^(m+1) * (j_t+m-t)!) where (x){n} is the falling factorial defined as (x){n} = Product{k=0..n-1} (x-k). - Mikhail Kurkov, May 24 2026” strata_touched:

• D5/S1/Recurrence/Algebraic/KurkovNestedStirlingIdentity license: citation-only triage: anchor

Kurkov’s full nested Stirling identity

Verified locator

• URL: https://oeis.org/A132393
• Internal source: https://oeis.org/A132393/internal
• The internal entry was read on September 22, 2026. Its NAME identifies the triangle as unsigned Stirling numbers of the first kind, with row index n and column index k from zero through n.
• The exact May 24, 2026 FORMULA line is:

Conjecture: T(n+m+1,m+1) = (n+m)! * (Product_{i=1..m} (n+i)^i) * Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(n*m + j_1 + j_2 + … + j_m) * (Product_{1 <= q < p <= m} (j_q - j_p + p - q)^2) * Product_{t=1..m} (n+t-1){j_t} / ((n-j_t+t)^(m+1) * (j_t+m-t)!) where (x){n} is the falling factorial defined as (x){n} = Product{k=0..n-1} (x-k). - Mikhail Kurkov, May 24 2026

The all-parameter domain is n >= 0 and m >= 1, with integer indices. These are the natural well-defined bounds of the displayed sums; the source does not print an additional quantifier sentence. The falling factorial is descending. All denominators are positive on the summation domain.

Source status and scope

The primary entry still labels this exact line Conjecture at the checked date. Issue https://github.com/the-omega-institute/trureturing/issues/9456 preregisters the exact assertion. The source/history audit recorded introduction in revision 257, approval in 261, the falling-factorial clarification in 269, and continued Conjecture wording in approved revision 286.

The preregistration reports a bounded prior-resolution audit of the Lee JIS paper 29 (2026), Article 26.2.7; MSE 5089097; MO 488662, 423415 and 415317; Krattenthaler math/0503507v2; Deb-Sokal 2507.18959; and Jeong 2607.26613. No source-equivalent proof was found in that inspected set. The independent audit read the relevant Krattenthaler statements, not the cited original Neuwirth proofs, and inspected Deb-Sokal only at abstract/introduction level. Those limits do not certify worldwide unresolved status or priority.

Classical Lean supplier

The proof-local rectangular Cauchy-Binet proof is Alex Meiburg’s cauchyBinet from https://github.com/leanprover-community/physlib/blob/15d02258f4c017bd63c6f3ece4653aa421ea87c3/QuantumInfo/ForMathlib/Majorization.lean, lines 147-231. Copyright (c) 2026 Alex Meiburg, Apache-2.0. The full license is retained at docs/reports/inoutbalance/physlib-LICENSE.txt; its bytes equal the upstream LICENSE at that revision (SHA-256 c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4). The complete upstream tree has 1327 entries and no NOTICE file.

Upstream pins Lean v4.34.0 and Mathlib 5ed2965256430c3649e86755f9576b54eca72435; the repository pins v4.33.0 and db584cd6d46c92f209a44c0f1c829460d327499d. Their mismatch rules out direct dependency form under A17.2. The compatible port uses only Mathlib imports and preserves the supplier proof body, with local scope and fixed universe. The isolated supplier compiled under the repository pin with exactly propext, Classical.choice, and Quot.sound.

Retire the port when this repository’s own pinned Mathlib supplies an equivalent rectangular Cauchy-Binet declaration. Classical determinant, Vandermonde and Stirling identities are not claimed as new results.