bibkey: dement2005a113249
authors: Creighton Dement
year: 2005
title: "OEIS A113249: odd-index squares in a fourth-order recurrence family"
doi: null
url: https://oeis.org/A113249
claim: "Conjecture: a(m, 2*n+1) is a perfect square for all m, n."
strata_touched:
  - D5/S1/Recurrence/OEISA113249OddIndexSquares
license: citation-only
triage: anchor

Verified locator

Source: https://oeis.org/A113249

OEIS A113249

The unpaginated Name (%N) states: “Corresponds to m = 3 in a family of 4th-order linear recurrence sequences given by a(m,n) = m^4a(n-4) + (2m)^2a(n-3) - 4a(n-1), a(m,0) = -1, a(m,1) = 4, a(m,2) = -13 + 6*(m-1) + 3*(m-1)^2, a(m,3) = (-8+m^2)^2.”

The unpaginated Comments (%C) state: “Conjecture: a(m, 2*n+1) is a perfect square for all m, n. Disregarding signs and/or initial term, we have: m = 0 (A000302), m = 1 (A097948), m = 2 (A056450), m = 3 (a(n)), m = 4 (A113250), m = 5 (A113251), m = 6 (A113252), m = 7 (A113253), m = 8 (A113254), m = 9 (A113255), m = 10 (A113256).”

The parameter and index range over the natural numbers including zero; sequence values are integers. The formula for the third initial value uses integer subtraction, including when m is zero. A perfect square means Mathlib’s IsSquare over the integers.

The general proof identifies the odd subsequence with the squares of the auxiliary sequence b(0) = 2, b(1) = m² − 8, b(n+2) = −4b(n+1) − m²b(n). The two sequences obey the same order-three recurrence and agree at three consecutive indices. This argument uses no division and includes m = 0 and m = 2.

The related entry https://oeis.org/A113254 records a proof for m = 8 by Google DeepMind AlphaProof Nexus. Its recurrence-window pattern informs the general proof; its Lean proof term is not imported. Completeness of the external literature search is ASSUMED-UNVERIFIED.