Add a generalized-Laguerre ODE reduction for second-derivative sequences

[PerAlexandersson]

Gap

Several OEIS rows are generated by the same second-derivative recurrence

P(0) = 1,
P(n+1) = (c+X)P(n) + (m*c+2*m*X)P'(n) + m^2*X*P''(n).

For these rows, direct use of the LS4 shell proves row-wise real-rootedness but
does not produce the adjacent Interlaces/Prec certificate required by the
generated OEIS modules. The PFBidiagonal Jensen/cubic-residual wrappers are
not an alternative checked endpoint: they currently pass through the explicit
admission jensenPencilBidiagonalPreserver tracked separately by issue #355.

Reusable reduction

The family satisfies the generalized-Laguerre eigenvalue identity

m*X*P''(n) + (c+X)*P'(n) = n*P(n).

Induction proves this identity without division: use the identity at row n
to reduce the defining recurrence to

P(n+1) = (m*n+c+X)*P(n) + m*X*P'(n),

then differentiate the old identity once to prove it at row n+1. The reduced
recurrence is an immediate instance of the existing affine-X derivative
degree/nonnegativity and interlacing backend.

Proposed canonical API

Add a checked theorem, plus a small tactic frontend, along the lines of:

theorem generalizedLaguerreSecondDerivative_ode_and_reduced
    {P : Nat -> ℝ[X]} {m c : ℝ}
    (hzero : P 0 = 1)
    (hrec : forall n, P (n+1) =
      (C c + X) * P n +
      (C (m*c) + C (2*m) * X) * (P n).derivative +
      C (m^2) * X * (P n).derivative.derivative) :
    (forall n, C m * X * (P n).derivative.derivative +
      (C c + X) * (P n).derivative = C n * P n) /\
    (forall n, P (n+1) =
      (C (m*n+c) + X) * P n +
      C m * X * (P n).derivative)

The exact statement can avoid casts in the interface if m c : Nat is the
better tactic-facing choice. A companion sequence theorem should assume
0 <= m, 0 < 1 for the X*P coefficient, and the usual base certificates,
then delegate to the existing affine-X derivative backend to return adjacent
Interlaces (or Prec), not merely row-wise splitting.

Suggested tactic surface:

rr_generalized_laguerre_second_derivative_sequence using
  scale := m,
  parameter := c,
  base := ...,
  recurrence := ...

The tactic should normalize scalar casts and the expanded OEIS recurrence,
prove the ODE/reduced recurrence internally, and expose the checked interlacing
endpoint.

Current target families

• A105278: (m,c)=(1,2); locally checked by an explicit ODE reduction.
• A271703: (m,c)=(1,0).
• A286724: (m,c)=(2,2).
• A048854: (m,c)=(4,2).
• A292219: (m,c)=(4,6).
• A290596: (m,c)=(3,2).
• A290598: (m,c)=(3,4).

A105278 is locally checked. A271703, A286724, A048854, and A292219 are current
unfinished generated modules. A290596 and A290598 are also listed by the
existing LS4 coverage table and should be audited against their current
generated files before changing their proof status.

Acceptance checks

• no new sorry or admitted proposition;
• canonical smoke tests for at least (1,2), (2,2), and (4,6);
• the theorem returns or directly feeds adjacent interlacing;
• local OEIS modules no longer need to duplicate the ODE induction;
• build RealRooted.Tactic, its examples, and the affected generated modules.