Add an asymmetric quadratic-derivative sequence backend

[PerAlexandersson]

Motivation

The OEIS proof backlog now has several recurrence families of the form

P(n+1) = (a(n) + b(n) X) P(n) + (u(n) X - v(n) X^2) P′(n).

The current project-local scaled_x_sub_x_sq_derivative_step_* helpers cover only the symmetric specialization u(n)=v(n). The asymmetric cases currently require long sequence-specific coefficient inductions even though the real-rootedness step is the same Ma–Wang argument.

Immediate generated targets are:

• sqrt-of-2/real-rooted-oeis A102365 after the tail shift Q(n)=P(n+1): a=1, b=n+1, u=2, v=1;
• A106800 after the same tail shift: a=1, b=n+1, u=0, v=1;
• unshifted A008278, A089231, A126351, and A144084 in the -X^2 P′ lane.

A126351 and A144084 already contain nearly duplicate hand-written coefficient/degree/root-sign inductions, so copying those proofs into the remaining modules would deepen avoidable duplication.

Proposed theorem layer

Add a reusable sequence theorem (name open to adjustment) for the recurrence above. A useful interface should accept:

• 0 ≤ a(n), 0 ≤ u(n), and 0 ≤ v(n);
• 0 ≤ b(n) - v(n) * m for m ≤ n (or the equivalent shifted coefficient condition);
• 0 < b(n) - v(n) * n for degree growth / positive leading coefficient;
• a constant nonzero base row with nonnegative coefficients;
• the normalized recurrence identity.

It should return the recurring state

(P n).natDegree = n ∧
HasPosLeadingCoeff (P n) ∧
HasNonnegCoeffs (P n)

and a companion theorem should derive adjacent Interlaces, hence Splits and nonvanishing, from small affine/quadratic base cases. A degree-offset/tail wrapper may remain in the OEIS client; it need not be part of the canonical theorem.

The coefficient update is

[X^m] P(n+1)
  = (a(n) + u(n) m) [X^m] P(n)
    + (b(n) - v(n) (m-1)) [X^(m-1)] P(n),

which gives the nonnegative-coefficient and leading-coefficient induction under the conditions above.

Real-rootedness route

For a nonpositive root r of a nonzero, splitting row with nonnegative coefficients,

u(n) r - v(n) r^2 ≤ 0.

Together with derivative_interlaces, positive leading coefficients, and the one-step degree data, the existing canonical prec_of_interlaces_evalCoeff_nonpos / Ma–Wang machinery gives the next-row Prec step. This is the same argument already expanded by hand in the OEIS A126351 and A144084 modules.

References in the current library: RealRooted.MaWang, RealRooted.Tactic.RootBounds, and the planned theorem-wrapper-first workflow in RealRooted/Tactic/PLAN.md (Phases 0–2).

Tactic frontend

After the theorem wrapper is executable, add a shallow rr_* frontend (or extend the Ma–Wang sequence frontend) that:

1. recognizes the normalized u X - v X^2 derivative multiplier;
2. asks positivity/linarith for the scalar inequalities;
3. leaves recurrence normalization and base-row certificates as explicit goals when automation cannot close them.

Tests should include the symmetric u=v regression plus u=0,v=1 and u=2,v=1, so the frontend demonstrably covers A106800 and A102365.

Remaining assumptions to settle

• whether a,u,v should vary with n in the first public theorem or begin as constants;
• the cleanest indexing of the coefficient inequality (m ≤ n versus m < n+1);
• whether the interlacing companion takes the first two/three base certificates directly or exposes only the inductive Prec step for a separate sequence finisher.