A Stirling minor as a finite Vandermonde-square sum

Abstract

Kurkov’s three-parameter Stirling-minor Vandermonde sum.

All parameters are natural numbers. The matrix indices in the OEIS source start at one; a Fin index i represents i+1. The unsigned cycle numbers are Nat.stirlingFirst. The domain Chain is the antitone-map type of KurkovNestedStirlingIdentity, so each tuple in the nested ranges is counted exactly once. Factorials, descending factorials and exponents are natural; all divisions and Vandermonde differences are rational. Natural subtraction has Lean’s truncated meaning; the bounds on a chain make the displayed indices equal to their integer values.

Definition 1.1 (The first-kind Stirling minor).

$$\forall n\in \mathbb{N},\forall k\in \mathbb{N},\forall m\in \mathbb{N},B\left(n,k,m\right)=Matrix.det\left(\lambda i:\mathrm{Fin}\left(k\right)\mapsto \lambda j:\mathrm{Fin}\left(k\right)\mapsto (Nat.stirlingFirst\left(n+m+\mathrm{val}\left(i\right)+1,n+\mathrm{val}\left(j\right)+1\right):\mathbb{Q})\right)$$

Formalization. D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.B (✓ std3).

Citation. Mikhail Kurkov (2026). OEIS A396563: three-parameter Stirling-minor Vandermonde sum. URL: https://oeis.org/A396563/internal.

Commentary.

The source, OEIS A396563 FORMULA (unpaginated), defines the determinant in the sentence below. Conjecture: B(n, k, m) = (Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(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)^(n+k) / (j_t+m-t)!) / (Product{i=0..m-1} (n+i)!) where B(n, k, m) is the determinant of the k X k matrix with (i, j)-th entry |Stirling1(n+m+i, n+j)|, where (x){n} is the falling factorial defined as (x){n} = Product_{k=0..n-1} (x-k).

Definition 1.2 (The signed summand).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall k\in \mathbb{N},\forall j\in \mathrm{Chain}\left(n,m\right),\mathrm{sourceTerm}\left(k,j\right)=((-1:\mathbb{Q}){)}^{{\sum }_{t:\mathrm{Fin}\left(m\right)}(\mathrm{val}\left(\mathrm{val}\left(j\right)\left(t\right)\right))}\cdot \prod _{q:\mathrm{Fin}\left(m\right)}(\prod _{p\in Finset.Ioi\left(q\right)}(((\mathrm{val}\left(\mathrm{val}\left(j\right)\left(q\right)\right):\mathbb{Q})-(\mathrm{val}\left(\mathrm{val}\left(j\right)\left(p\right)\right):\mathbb{Q})+(\mathrm{val}\left(p\right):\mathbb{Q})-(\mathrm{val}\left(q\right):\mathbb{Q}){)}^2))\cdot \prod _{t:\mathrm{Fin}\left(m\right)}(\frac{(Nat.descFactorial\left(n+\mathrm{val}\left(t\right),\mathrm{val}\left(\mathrm{val}\left(j\right)\left(t\right)\right)\right):\mathbb{Q})\cdot ((n-\mathrm{val}\left(\mathrm{val}\left(j\right)\left(t\right)\right)+\mathrm{val}\left(t\right)+1:\mathbb{Q}){)}^{n+k}}{(Nat.factorial\left(\mathrm{val}\left(\mathrm{val}\left(j\right)\left(t\right)\right)+m-\left(\mathrm{val}\left(t\right)+1\right)\right):\mathbb{Q})})$$

Formalization. D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.sourceTerm (✓ std3).

Citation. Mikhail Kurkov (2026). OEIS A396563: three-parameter Stirling-minor Vandermonde sum. URL: https://oeis.org/A396563/internal.

Commentary.

The sign exponent is the sum of the chain values. Each pair of positions contributes the square of its rational difference with the position correction. The descending factorial and the power n+k lie in the numerator. Conjecture: B(n, k, m) = (Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(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)^(n+k) / (j_t+m-t)!) / (Product{i=0..m-1} (n+i)!) where B(n, k, m) is the determinant of the k X k matrix with (i, j)-th entry |Stirling1(n+m+i, n+j)|, where (x){n} is the falling factorial defined as (x){n} = Product_{k=0..n-1} (x-k).

Definition 1.3 (The normalized nested sum).

$$\forall n\in \mathbb{N},\forall k\in \mathbb{N},\forall m\in \mathbb{N},\mathrm{sourceRHS}\left(n,k,m\right)=\frac{{\sum }_{j:\mathrm{Chain}\left(n,m\right)}(\mathrm{sourceTerm}\left(k,j\right))}{{\prod }_{i:\mathrm{Fin}\left(m\right)}((Nat.factorial\left(n+\mathrm{val}\left(i\right)\right):\mathbb{Q}))}$$

Formalization. D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.sourceRHS (✓ std3).

Citation. Mikhail Kurkov (2026). OEIS A396563: three-parameter Stirling-minor Vandermonde sum. URL: https://oeis.org/A396563/internal.

Commentary.

The complete chain sum is divided by the product of (n+i)! for 0<=i<m. Empty products and determinants have value one. Conjecture: B(n, k, m) = (Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(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)^(n+k) / (j_t+m-t)!) / (Product{i=0..m-1} (n+i)!) where B(n, k, m) is the determinant of the k X k matrix with (i, j)-th entry |Stirling1(n+m+i, n+j)|, where (x){n} is the falling factorial defined as (x){n} = Product_{k=0..n-1} (x-k).

Definition 1.4 (Kurkov’s three-parameter assertion).

$$claim=(\forall n\in \mathbb{N},\forall k\in \mathbb{N},\forall m\in \mathbb{N},(1\le m)\Rightarrow (B\left(n,k,m\right)=\mathrm{sourceRHS}\left(n,k,m\right)))$$

Formalization. D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.claim (✓ std3).

Citation. Mikhail Kurkov (2026). OEIS A396563: three-parameter Stirling-minor Vandermonde sum. URL: https://oeis.org/A396563/internal.

Commentary.

OEIS A396563 FORMULA, approved revision 15, is unpaginated. Conjecture: B(n, k, m) = (Sum_{j_1=0..n} Sum_{j_2=0..j_1} … Sum_{j_m=0..j_{m-1}} (-1)^(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)^(n+k) / (j_t+m-t)!) / (Product{i=0..m-1} (n+i)!) where B(n, k, m) is the determinant of the k X k matrix with (i, j)-th entry |Stirling1(n+m+i, n+j)|, where (x){n} is the falling factorial defined as (x){n} = Product_{k=0..n-1} (x-k). The assertion quantifies over all n,k>=0 and m>=1. The source examples and programs include n=0 and k=0.

Theorem 1.5 (The full identity).

$$\forall n\in \mathbb{N},\forall k\in \mathbb{N},\forall m\in \mathbb{N},(1\le m)\Rightarrow (B\left(n,k,m\right)=\mathrm{sourceRHS}\left(n,k,m\right))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.result (✓ std3). ∎

Resolves. Problems/kurk396563 (proved) by D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.result.

Source. Repository-derived.

Acknowledgement. Mikhail Kurkov (2026). OEIS A396563: three-parameter Stirling-minor Vandermonde sum. URL: https://oeis.org/A396563/internal.

Commentary.

The coefficient identity for rising factorials converts the first-kind minor into an elementary-coefficient corner. Determinant-one inverse Toeplitz matrices identify that corner with the complete-coefficient corner of a different size. The map sending j at position t to n-j+t identifies the nested tuples with increasing subsets. Factorial normalization and Cauchy–Binet give a signed moment determinant. Stirling inclusion–exclusion evaluates its entries; column reversal cancels its sign. This proves the displayed identity also when n=0 or k=0.

References

• Truth anchor: D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.B
• Truth anchor: D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.claim
• Truth anchor: D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.result
• Truth anchor: D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.sourceRHS
• Truth anchor: D5/S3/Combinatorics/BinomialBases/KurkovStirlingMinorVandermondeSum.sourceTerm
• Dependency: D5/S1/Recurrence/Algebraic/KoutschanKrattenthalerSchlosserShiftedG
• Dependency: D5/S1/Recurrence/Algebraic/KurkovNestedStirlingIdentity
• Dependency: D5/S1/Recurrence/Interpolation/CullinanYoungKrawtchouk
• Dependency: D5/S1/Recurrence/Parity/StirlingPowerFactorialPrimePeriod
• Dependency: D5/S3/Analytic/GoldenTomography/FinitePronyHankelReconstruction
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/Duality
• Dependency: D5/S3/Quantum/Schatten/CompoundMatrices