Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

slug: oeis-a054096-stephan-triangle-second-column bibkey: kimberling2004a054096 doi: null url: https://oeis.org/A054096 triage: theorem motivation_gids:

  • D5/S1/Recurrence/StephanTriangleSecondColumn.result
  • D5/S1/Recurrence/StephanTriangleSecondColumn.rowSum_succ

Stephan’s A054096 second-column conjecture

Problem

OEIS A054096, NAME (%N, verbatim):

T(n,2), array T as in A054090.

Ralf Stephan’s target COMMENT (%C, verbatim):

Conjecture: sequence is A006183 shifted right. - Ralf Stephan, Jan 15 2004

OEIS A054090, NAME (%N, verbatim):

Triangular array generated by its row sums: T(n,0) = 1 for n >= 0, T(n,1) = r(n-1), T(n,k) = T(n,k-1) - (-1)^k * r(n-k) for k = 2, 3, …, n, n >= 2, r(h) = sum of the numbers in row h of T.

OEIS A054090, FORMULA (%F, verbatim):

T(n, k) = T(n, k-1) - (-1)^k * Sum_{j=0..n-k} T(n-k, j), with T(n, 0) = 1, and T(n, 1) = Sum_{j=0..n-1} T(n-1, j).

OEIS A006183, NAME (%N, verbatim):

a(n) = (n+1)*a(n-1) + (2-n)*a(n-2).

The literal proved statement is

forall T B, IsA054090Triangle T -> IsShiftedA006183 B -> forall n, 2 <= n -> T n 2 = B (n - 1).

A054096 has offset 2 and A006183 has offset 1, and their %S and %T data lines are term-for-term identical. Thus “shifted right” means A054096(n) = A006183(n-1) for n >= 2. Writing B(j) = a(j-1) turns A006183’s recurrence into B(j) = j*B(j-1) + (3-j)*B(j-2), exactly the recurrence encoded by IsShiftedA006183.

Not claimed here are other columns of A054090; the row-sum sequence A054091; the generating-function form of A006183, including Gladkovskii’s 2013 continued fraction %F, or its equivalence to the recurrence; or any particular term of A054096.

Motivation

Ralf Stephan stated the conjecture in January 2004. It had remained unsettled for 22 years when this proof was checked in 2026. The result identifies the complete second column from the defining row-sum equations, while the row-sum invariant is reusable for the triangle’s other columns and for later work on A054091.

Gap

The mandatory first lead was checked and refuted on two independent grounds: Tian-Xiao He and Louis W. Shapiro, Row sums and alternating sums of Riordan arrays, Linear Algebra and its Applications 507 (2016), 77–95, DOI 10.1016/j.laa.2016.05.035 — its OpenAlex-indexed full text has zero exact hits for A054096, A054090, A054091, A006183, Kimberling, Stephan, 1753618, the prefix “1,2,6,22,98,522”, or “generated by its row sums”, and its reference list carries only a generic OEIS citation; and, independently of any search, A054090 is not an ordinary Riordan array — columns 0 and 1 would force the row-3 column-2 value to be 3, whereas A054090 has 2, so the triangle is not in that paper’s object class at all. Also checked: Paul Barry, arXiv:1804.06801 (full PDF; its covered-sequence list omits all three entries); OpenAlex global full-text for the three A-numbers, the exact %N phrase and the numeric prefix (all 0, with one unrelated biology false positive for A006183); the recurrence’s combinatorial interpretations and A006183’s references. No source proving the identity was found; the finding is bounded, not a claim of exhaustive search.

Route

The cross-row induction proves that an entry in one row is the difference between the first column and the next column of the following row. Summing these identities across a row telescopes and yields the public invariant rowSum(T,n+1) = n*rowSum(T,n) + 2.

The second-column defining equation identifies T(n,2) with the difference of two successive row sums. A strong induction then shows that these differences satisfy the shifted A006183 initial values and recurrence. The two identities combine to give T(n,2) = B(n-1) for every n >= 2.

Falsifier

A pair of integer-valued functions T and B satisfying the two stated predicates, together with a natural n >= 2 for which T(n,2) != B(n-1), would contradict result. A triangle satisfying IsA054090Triangle and an index n whose row sums violate rowSum(T,n+1) = n*rowSum(T,n) + 2 would contradict the reusable lemma.

Evidence

  • Lean module: D5/S1/Recurrence/StephanTriangleSecondColumn.lean.
  • Public definition rowSum: std3 axiom closure [propext, Classical.choice, Quot.sound].
  • Public definition IsA054090Triangle: std3 axiom closure [propext, Classical.choice, Quot.sound].
  • Public definition IsShiftedA006183: empty axiom closure.
  • Public theorem rowSum_succ: std3 axiom closure [propext, Classical.choice, Quot.sound].
  • Public theorem result: std3 axiom closure [propext, Classical.choice, Quot.sound].
  • Kernel profile on this worktree: wall time 3.25 seconds, type checking 163 milliseconds, and maximum resident set size 1,486,766,080 bytes.
  • Deleting Mathlib.Algebra.BigOperators.Group.Finset.Basic makes the module fail to compile with exit 1; deleting Mathlib.Tactic.Ring independently also makes it fail with exit 1.
  • The orchestrator independently recomputed the triangle with exact integers through n = 59 and found zero mismatches with shifted A006183.
  • The finite recomputation carries no proof of the universal statement.

Triage

theorem. Stephan’s second-column conjecture is proved for every integer triangle and sequence satisfying the two source predicates; the resolution is proved, not refuted.

ASSUMED-UNVERIFIED

Literature completeness outside the bounded scan of the named Riordan paper, Barry’s arXiv paper, the OpenAlex full-text queries, A006183’s references and combinatorial interpretations, the repository, and pinned Mathlib is unverified. No exhaustive literature or priority claim is made. The finite exact-integer recomputation through n = 59 does not establish the universal statement.