[PerAlexandersson]

Closes #2513.

Theorem (RealRooted.strictInterl_of_orbitPerturbation_recurrence). Let s ≥ 1 and κ ≥ s + 4, and let Q satisfy Q 0 = 1, Q 1 = 2u + 1, Q 2 = κu² + κu + 1 and, for n ≥ 0,

(n+1) Q(n+3) = (2n+3)(2u+1) Q(n+2) + (n+1) s (u+1) θ Q(n+2)
               − (n+2)(2u+1) [(2u+1) Q(n+1) + s (u+1) θ Q(n+1)],   θ = u d/du.

Then every Q n has simple roots in (−1, 0) and StrictInterl (Q n) (Q (n+1)). This is the issue's recurrence multiplied by n − 2 and shifted by 3. Applications: A141689 (1,5), A141690 (1,8), A141696 (1,10), A141697 (1,18), A147565 (2,6).

Proof (fully checked; axioms propext, Classical.choice, Quot.sound only):

• centeredEulerOrbit_critical_values (n ≥ 5, via the inverse Bernstein inequality of The inverse Bernstein inequality for polynomials with large critical values #2522/Alternating values bound every critical value #2523) and centeredEulerOrbit_small_critical (n ≤ 4; explicit rows, drafted by a Codex worker and merged into the existing row lemmas).
• New shim lemma Polynomial.roots_of_sign_changes: a degree-n polynomial with n sign changes has exactly one simple root per interval, with the sign of the derivative there.
• strictInterl_centeredEulerStep_add_monomial / centeredEulerOrbit_add_monomial: for α ≥ 1/2 and −1 < b ≤ 1, h n = p n + b X^n has simple roots in (−1, 1) and h n ≺ h (n+1) (Ma–Wang root-sign criterion with h (n+1) = X h n + α(X² − 1) p n').
• orbitPerturbationRow_recurrence and the transfer x = 2u + 1, Q n = r p n + (1 − r) x^n, r = (κ − 4)/(2s).

Eulerian form (RealRooted.splits_C_mul_add_C_mul_one_add_X_pow_of_recurrence, new file OrbitPerturbationCayley.lean): for s ≥ 1, c ≥ 1/2, E 0 = 1 and E (n+1) = (1 + (1 + s n) X) E n + s X (1 − X) E n', every c E n + (1 − c)(1 + X)^n splits. This is the Cayley transform of the Q n (new shim lemmas cayleyTransform_X_pow, cayleyTransform_succ, cayleyTransform_succ_X_mul, cayleyTransform_X_mul_derivative); for s = 1 the E n are the Eulerian polynomials, matching the downstream models c · A173018 (n+1) − (c − 1)(1 + X)^n.

Catalog page centered-euler-orbit-perturbation (tag realrooted-original, cites Erdélyi–Hardin–Saff arXiv:1307.4056).

Local checks: focused Lake builds of the four touched modules and the catalog page, runLinter on each, root imports, module system, import architecture (budgets +4), proof status, catalog audit and tests.

🤖 Generated with Claude Code