Formal target: Corpus.OEIS103885.conjecture
The recurrence given below can be rewritten in the form $$(2n+1)(2n+2)P(2,n)a(n+1) - (2n-1)(2n-2)P(2,-n)a(n-1) = Q(2,n^2)a(n),$$ where the polynomial $Q(2,n) = 4(55n^2 - 34n + 3)$ and the polynomial $P(2,n) = 5n^2 - 5n + 1$ satisfies the symmetry condition $P(2,n) = P(2,1-n)$ and has real zeros.
Exact formal statement
∀ (m : Nat),
LE.le.{0} 1 m →
Exists.{1} fun P =>
Exists.{1} fun Q =>
And (Eq.{1} (Polynomial.degree.{0} P) (Nat.cast.{0} (HMul.hMul.{0, 0, 0} 2 m)))
(And (Eq.{1} (Polynomial.degree.{0} Q) (Nat.cast.{0} (HMul.hMul.{0, 0, 0} 2 m)))
(And
(∀ (n : Nat),
LE.le.{0} 1 n →
Eq.{1}
(HAdd.hAdd.{0, 0, 0}
(HMul.hMul.{0, 0, 0}
(HMul.hMul.{0, 0, 0} (Corpus.OEIS103885.prodFactorPlus m n)
(Polynomial.eval.{0} (Nat.cast.{0} n) P))
(Corpus.OEIS103885.aSubsequenceReal m (HAdd.hAdd.{0, 0, 0} n 1)))
(HMul.hMul.{0, 0, 0}
(HMul.hMul.{0, 0, 0}
(HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} (-1) m) (Corpus.OEIS103885.prodFactorMinus m n))
(Polynomial.eval.{0} (Neg.neg.{0} (Nat.cast.{0} n)) P))
(Corpus.OEIS103885.aSubsequenceReal m (HSub.hSub.{0, 0, 0} n 1))))
(HMul.hMul.{0, 0, 0} (Polynomial.eval.{0} (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2) Q)
(Corpus.OEIS103885.aSubsequenceReal m n)))
(And (∀ (x : Real), Eq.{1} (Polynomial.eval.{0} x P) (Polynomial.eval.{0} (HSub.hSub.{0, 0, 0} 1 x) P))
(And
(∀ (z : Complex),
Eq.{1} (Polynomial.eval.{0} z (Polynomial.map.{0, 0} (Algebra.algebraMap.{0, 0} Real Complex) P))
0 →
And (Eq.{1} z.im 0) (Membership.mem.{0, 0} (Set.Icc.{0} 0 1) z.re))
(∀ (z : Complex),
Eq.{1}
(Polynomial.eval.{0} (HPow.hPow.{0, 0, 0} z 2)
(Polynomial.map.{0, 0} (Algebra.algebraMap.{0, 0} Real Complex) Q))
0 →
And (Eq.{1} z.im 0) (Membership.mem.{0, 0} (Set.Icc.{0} (-1) 1) z.re))))))This target is a formal statement, not a proof of the problem.
Environment availability: available.