A261318: quantify Euler-operator root separation for cycle sigma rows

[PerAlexandersson]

Scope

This tracks the genuinely new quantitative root estimate exposed by OEIS
A261318. It is not a claim that the generated family has already been proved
real-rooted.

The generated recurrence is

A_0 = 1,  A_1 = 0,  A_2 = X + X^2,
A_(n+3) = 2X A'_(n+2) + 2X A'_(n+1)
          + (X-2) A_(n+2) + (X-1) A_(n+1).

A bounded Claude Opus/max literature-and-proof consultation found a useful
first-order reduction, but no theorem in the checked literature that closes
the final estimates.

Checked algebraic reduction

Let L_a(f) = 2X f' + (X+a)f and q = X(1+X). For n >= 1, the order-two
recurrence is equivalent to

A_(n+1) = L_(-1)(A_n) + (-1)^(n-1) q.

Indeed, the original recurrence rewrites as
A_(n+1) = L_(-1)(A_n) + L_(-1)(A_(n-1)) - A_n, and the previous first-order
step supplies the alternating correction.

For n >= 2, define

Gamma_n = A_n / X + [n odd],
P_n     = (Gamma_n - 1) / X.

Then

Gamma_(n+1) = L_1(Gamma_n) - X * [n even],
P_(n+1)     = L_3(P_n) + [n odd],
A_n = X + X^2 P_n  (n even),
A_n =     X^2 P_n  (n odd).

The unperturbed parity steps follow from the standard Eulerian-operator
interlacing argument. The perturbed steps reduce to the following quantitative
invariants.

Open root-derivative invariants

1. Starting with Gamma_2 = 1+X and the recurrence above, prove that every
   Gamma_n is monic, has distinct negative roots, and satisfies

   |Gamma_n'(r)| >= 1
   

   at every root r of Gamma_n. The downstream step needs only the weaker
   threshold Gamma_n'(r) > 1/2 at roots where the derivative is positive.

2. Starting with P_2 = 1, prove that every P_n is monic, has distinct
   negative roots, and satisfies

   2 * |r| * |P_n'(r)| >= 1
   

   at every root r of P_n.

These estimates imply splitting of every A261318 row by sign changes at the
old roots. Finite high-precision checks show wide margins, but they are only
evidence.

Partial transfer lemma

A potentially reusable theorem is:

If a > 0, f is real-rooted, and theta < 0 is a root of L_a(f) with
f(theta) != 0, then (L_a(f))'(theta) has the sign of f(theta) and
|(L_a(f))'(theta)| > a * |f(theta)| / |theta|.

The proof uses f''f < (f')^2 away from the roots. This is not enough by
itself: closing the induction still needs a lower bound on the separation of
new roots of L_a(f) from the old roots of f.

Statement correction

The historical target Prec (A_n) (A_(n+1)) is false for odd n, already at
n=3, because A_3 has a double zero at 0 while A_4 has only a simple
zero there and additional negative roots to its right. Do not use that target
as an induction invariant.

References

• OEIS A261318, including the row formula and the
  Britnell--Wildon interpretation.
• Britnell--Wildon,
  Bell numbers, partition moves and the eigenvalues of the random-to-top
  shuffle in Dynkin Types A, B and D.
• Brown--Erey,
  On the roots of sigma-polynomials.
  Their real-rootedness theorem covers chromatic number at least v-3, so it
  does not give a general cycle result.
• Brown--Erey,
  On the real roots of sigma-polynomials.

Suggested formalization order

1. Prove the first-order recurrence and the Gamma/P identities.
2. Formalize the partial transfer lemma as a general RealRooted theorem.
3. Treat the two quantitative invariants as explicit sorry targets while
   investigating a root-separation estimate.
4. Derive A261318 splitting only after those targets are discharged.