Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: barry-2013-riordan-pascal-kernel-determinant bibkey: barry2013riordanpascal doi: null url: https://cs.uwaterloo.ca/journals/JIS/VOL16/Barry2/barry231.pdf triage: theorem motivation_gids:

  • D5/S1/Recurrence/Algebraic/BarryRiordanPascalKernelDeterminant.result

Barry’s Riordan-Pascal kernel determinant

Problem

Barry defines the generalized Pascal matrix on printed page 1:

In this note, we investigate some properties of the two-parameter generalized Pascal triangle M^{(m)}(a, b) given by the Riordan array M^{(m)}(a, b) = ( 1/(1 − ax) , x(1 + bx)/(1 − ax)^m ).

The row polynomials are defined on printed page 19:

We can regard the matrix M^{(m)}(a, b) as the coefficient array of a family of polynomials P_n(x; m, a, b). We have P_n(x; m, a, b) = Σ_{k=0}^{n} T^{(m)}_{n,k}(a, b) x^k.

The comparison that introduces the kernel appears later on printed page 19:

It is interesting to compare the matrices defined by the quotient above with those defined by Σ_{j=0}^{n} P_j(x; m, a, b)P_j(y; m, a, b). In the case of monic orthogonal polynomials, such expressions lead to the same matrices. However, M^{(m)}(a, b) is not in general the coefficient array of a family of monic orthogonal polynomials, and hence the two family of matrices will in general differ. In the case m = 2, a = b = 1, we can conjecture the following.

Conjecture 32 is stated on printed page 20:

Conjecture 32. The matrix D̃_n(2, 1, 1) with generating function Σ_{k=0}^{n} P_j(x; 2, 1, 1)P_j(y; 2, 1, 1) is given by M_n^{(2)}(a, b)^t M_n^{(2)}(a, b). We then have |D̃_n(2, 1, 1)| = 1 for n ≥ 0. In the above the notation M_n denotes the matrix formed from the first (n + 1) rows and columns of M.

The page-20 lower summation index is printed as k=0, while its summand uses P_j. The unambiguous comparison display on page 19 uses j=0,...,n, so the formal sum uses that index. The right side is read at (a,b)=(1,1), as fixed by the sentence immediately preceding the conjecture and by its left side. The generic reading fails already at n=1: Dtilde_1 = [[2,1],[1,1]], while M_1(a,b)^t M_1(a,b) = [[1+a^2,a],[a,1]].

The phrase “with generating function” uses the coefficient-array convention from the same section: entry (i,k) is the coefficient of x^i y^k. Section 2 defines a Riordan array entry by T_{n,k} = [x^n] g f^k, with columns indexed from zero. Thus the quantified claim is, for every natural n, Dtilde_n = M_n^t M_n and det Dtilde_n = 1.

Motivation

Conjecture 32 asks for both an exact matrix identity and its determinant consequence for every truncation size. The frozen theorem settles both clauses uniformly, including n=0, rather than checking a bounded collection of matrices.

Gap

Issue #9215 preregisters the named first-tier open problem and its bounded literature check. OpenAlex lists five citing works. Three have arXiv full texts; each contains zero Christoffel hits. The two citing works without arXiv full text were checked only through available metadata and remain ASSUMED-UNVERIFIED.

OEIS A114188 cites Barry’s article but contains no settlement of the determinant or Gram-matrix assertion. Four MathDB searches, for Riordan, Barry, Pascal matrix determinant, and Christoffel-Darboux determinant, returned no entry. Semantic Scholar returned HTTP 429 and remains ASSUMED-UNVERIFIED.

These checked surfaces do not establish exhaustive worldwide literature coverage, publication priority, or the absence of an independent proof.

Route

(A) Coefficient extraction from Sum_{j=0}^{n} P_j(x)P_j(y) gives Sum_j T_{j,i}T_{j,k} in entry (i,k), exactly the corresponding entry of M_n^t M_n.

(B) The factor defining column k contains X^k; therefore entries strictly above the diagonal vanish, and the remaining factor has constant coefficient one. Hence M_n is lower unitriangular and det M_n = 1. Multiplicativity and transpose invariance then give det Dtilde_n = 1.

Under CLAUDE.md section 3.2, result is bind-only. The strict-upper-zero and diagonal-one facts are direct power-series coefficient normalizations, and the determinant step directly instantiates pinned Mathlib’s triangular determinant, multiplicativity, and transpose lemmas. There is no escape witness. Admission is open-problem-resolution: the settlement of the preregistered named conjecture is the new content, not the proof steps.

Falsifier

A natural n for which the coefficient matrix differs from M_n^t M_n, or for which its determinant differs from one, would refute the theorem. A generic (a,b) reading, the Christoffel-Darboux quotient matrix of Conjecture 31, or a different interpretation of the misprinted summation index is a different claim.

Evidence

The source and printed-page locators are recorded in Library/Recurrence/barry2013riordanpascal.md. Exact symbolic enumeration for n=0,...,8 gives Dtilde_n = M_n^t M_n and determinant one in every case. The first six rows of M are [1], [1,1], [1,4,1], [1,9,7,1], [1,16,26,10,1], and [1,25,70,52,13,1], matching the rows printed on page 2.

The frozen declaration is D5/S1/Recurrence/Algebraic/BarryRiordanPascalKernelDeterminant.result, with statement ID sha256:47340acd13b0514d3a4d25748e921f2f60bbbf1dc42e97c472de5eedf1bf52c8. Its freeze event is sha256:c10c0b78783c62d4772cd2e78d54a6e83d83dcb83eada6bc668da20af50e0418. The axiom closure is exactly propext, Classical.choice, and Quot.sound; the freeze event has no prerequisite frozen project nodes.

Triage

First tier: a conjecture printed in Barry, Journal of Integer Sequences 16 (2013), Article 13.5.4, preregistered in issue #9215. Resolution: proved. Conjecture 31 is not asserted or settled by this module.

Declarationproof_shapedirect frozen dependenciesescape_witnessadmission_basis
resultbind-onlynonenoneopen-problem-resolution

The public surface is exactly riordan, P, M, Dtilde, claim, and result. The module proves a symbolic theorem for every n; it is not bounded enumeration, checker infrastructure, numeric reduction, or a certified finite instance, so utility: none applies.

ASSUMED-UNVERIFIED

The two OpenAlex citing works without arXiv full text are ASSUMED-UNVERIFIED beyond their available metadata. Semantic Scholar is ASSUMED-UNVERIFIED because the request returned HTTP 429. The bounded literature checks do not establish exhaustive worldwide novelty, priority, or the absence of an independent proof. The Lean kernel does not authenticate the external PDF, its pagination, or its publication history.