A390883 prerequisite: shifted Jacobi interlacing and Euler-inverse pencil backend

[PerAlexandersson]

Goal

Formalize the reusable finite Jacobi-polynomial backend needed to consume the now-complete classical proof of A390883.

This is a prerequisite for #392, not a request for a conditional wrapper in the generated OEIS file. It is closely related in infrastructure to #420, but the needed theorem is different: A390883 needs parameter-gap interlacing and an Euler-inverse real pencil, rather than the Jacobi primitive theorem tracked there.

Audited proof source

The complete classical proof is commit dfe35502 on branch
proof/a390883-classical-proof-20260824 in the meta repository, file

workbench/proof-explorers/A390883-filtered-jacobi-bezoutian-continuation-2026-08-24.md.

The proof is all-rank. Bounded computations are discovery checks only.

Mathematical API required

Use shifted Jacobi polynomials

[
\mathcal P_n^{(\alpha,\beta)}(z)
= P_n^{(\alpha,\beta)}(1-2z).
]

An explicit finite coefficient definition is preferable, so the algebraic identities do not depend on analytic hypergeometric-series convergence.

The A390883 client needs the following checked statements.

1. Basic Jacobi theory. For alpha,beta > -1,
   mathcal P n alpha beta has degree n, simple roots in (0,1),
   the standard endpoint signs, derivative/ODE identities, and orthogonality
   on (0,1) against every polynomial of degree below n with weight
   z^alpha * (1-z)^beta.

2. Same-degree parameter-gap comparison. For N >= 1 and
   c in {1/2, 3/2}, if
   [
   S=\mathcal P_N^{(c-1,1)},\qquad
   J=\mathcal P_N^{(c+1/2,1)},
   ]
   and their roots are listed increasingly as s_i and xi_i, prove
   [
   s_i < \xi_i < s_{i+1}\quad(1\le i<N),\qquad
   s_N<\xi_N.
   ]
   A suitably general theorem for a Jacobi parameter increase below 2
   is welcome, but this exact gap 3/2 is the client requirement.

3. Adjacent-degree Driver--Jordaan--Mbuyi comparison. For m >= 1 and
   c in {1/2,3/2}, put
   [
   F=\mathcal P_m^{(c-1,0)},\qquad
   J=\mathcal P_{m-1}^{(c+1/2,1)}.
   ]
   With increasing roots f_i and xi_i, prove
   [
   f_i<\xi_i<f_{i+1}\qquad(1\le i<m).
   ]
   This is the specialization of Theorem 2.3 of Driver--Jordaan--Mbuyi,
   Numer. Algorithms 49 (2008), 143--152, DOI 10.1007/s11075-008-9162-2,
   with parameter increments (3/2,1).

4. Euler-inverse Jacobi pencil. Let
   [
   F(z)=\sum_{k=0}^m f_k z^k=\mathcal P_m^{(c-1,0)}(z),
   \qquad
   R_\gamma(z)=\sum_{k=0}^m f_k\frac{\gamma}{\gamma+k}z^k.
   ]
   Put A=c+m-1. For A <= gamma_1 <= gamma_2, prove the zero-aware
   real-pencil statement for R_(gamma_1),R_(gamma_2), and for strict
   inequalities orient it so the larger-gamma root set lies to the left.
   In RealRooted language the useful endpoint is an oriented Prec theorem
   (or an equivalent AllComboRealRooted theorem plus the orientation).

   The proof packet derives this from Jacobi orthogonality by
   [
   \int_0^1 z^{c-1}R_\gamma(z)p(z),dz
   =-R_\gamma(1)\int_1^\infty p(x)x^{c-\gamma-1},dx
   \quad(\deg p<m).
   ]
   For a pencil of two R_gamma polynomials, the right-hand density has at
   most one sign change. A root-count contradiction gives at least m-1
   sign-changing roots; conjugate-pair parity and the top-two coefficient
   determinant give full real-rootedness including a possible one-degree
   drop. The coefficient-of-z identity
   [
   -[z]R_\gamma=\frac{m(c+m)}c\frac{\gamma}{\gamma+1}
   ]
   fixes the interlacing orientation. The boundary gamma=A is
   (1-z) * mathcal P_(m-1)^(c-1,1).

Why this is not sequence-local

The pinned project revision has:

• the RealRooted Obreschkoff and common-interleaver consumers;
• a coefficient-level Jacobi (1,1) transport specialized to Braun--Jal;
• Mathlib ordinary hypergeometric functions as analytic series.

It does not have a general finite Jacobi polynomial, Jacobi orthogonality and simple-root API, either parameter-gap theorem above, or the Euler-inverse signed-pencil theorem. LeanSearch also finds no Mathlib Jacobi-root/interlacing theorem. Re-proving this analytic package inside ProofsOeis/A390883.lean would create substantial reusable theory in a generated sequence file.

The local algebraic Darboux identity from the proof packet has already been
probed successfully in AXLE/Lean 4.31.0; it is not the blocker.

Suggested milestones

1. Define the finite shifted Jacobi polynomial and prove coefficients, degree,
   endpoints, derivative formula, and differential equation.
2. Prove orthogonality and simple roots in (0,1).
3. Prove the same-degree gap-3/2 comparison.
4. Prove the adjacent-degree (3/2,1) comparison.
5. Formalize the signed moment identity and Euler-inverse pencil theorem,
   including degree-drop and boundary cases without a statement scaffold.
6. Axiom-audit the public endpoints and then consume them sequence-locally in
   ProofsOeis/A390883.lean.

Guardrails

• No sorry, admit, source axiom, or *Statement : Prop substitute.
• Do not encode Driver--Jordaan--Mbuyi as an assumed hypothesis.
• Keep the EHR contribution identity and agreement with the recurrence-defined
  generated family in the OEIS proof repository.
• The final OEIS client must prove A390883_splits n for every n, not
  only bounded ranks.

[PerAlexandersson]

Read-only milestone-2 audit: finite Favard is the shortest route

For every n : ℕ and real α β with hα : -1 < α and hβ : -1 < β, the useful public endpoints should be:

theorem shiftedJacobi_splits (n : ℕ) (hα : -1 < α) (hβ : -1 < β) :
    (Polynomial.shiftedJacobi n α β).Splits

theorem shiftedJacobi_hasSimpleRoots (n : ℕ) (hα : -1 < α) (hβ : -1 < β) :
    RealRooted.HasSimpleRoots (Polynomial.shiftedJacobi n α β)

theorem shiftedJacobi_root_mem_Ioo (n : ℕ) (hα : -1 < α) (hβ : -1 < β)
    {r : ℝ} (hr : (Polynomial.shiftedJacobi n α β).IsRoot r) :
    r ∈ Set.Ioo (0 : ℝ) 1

theorem shiftedJacobi_prec_succ (n : ℕ) (hα : -1 < α) (hβ : -1 < β) :
    RealRooted.Prec (Polynomial.shiftedJacobi n α β)
      (Polynomial.shiftedJacobi (n + 1) α β)

The strict ordered-root endpoint should avoid overloading weak Prec: with ss := (shiftedJacobi n α β).roots.sort (· ≤ ·) and rs := (shiftedJacobi (n+1) α β).roots.sort (· ≤ ·), prove

ss.length = n ∧ rs.length = n + 1 ∧
ss.Pairwise (· < ·) ∧ rs.Pairwise (· < ·) ∧
∀ i, i < n →
  rs.getD i 0 < ss.getD i 0 ∧ ss.getD i 0 < rs.getD (i + 1) 0

These hypotheses cover every current client pair: (-1/2,0), (1/2,0), (-1/2,1), (1/2,1), (1,1), and (2,1). The n = 0 simple/root assertions and strict-index clause are vacuous.

Lean-ready dependency chain. Put the root theory in a higher-level module importing the existing Mathlib-layer Jacobi algebra file and RealRooted.Favard; keep the Mathlib-layer file free of upward RealRooted imports.

1. Missing, Jacobi-specific algebra: let S n := shiftedJacobi n α β and Q n := C (S n).leadingCoeff⁻¹ * S n. Prove Q n monic and the Favard recurrence Q (n+1) = (X - C Aₙ) * Q n - C Bₙ * Q (n-1). With s = α+β,
   • A₀ = (α+1)/(s+2);
   • for n ≥ 1, Aₙ = (1 - (β^2-α^2)/((2*n+s)*(2*n+s+2)))/2;
   • B₁ = (1+α)*(1+β)/((s+2)^2*(s+3));
   • for n ≥ 2, Bₙ = n*(n+α)*(n+β)*(n+s)/((2*n+s)^2*(2*n+s-1)*(2*n+s+1)).
     Prove 0 < Bₙ; the separate B₁ formula removes the genuine 0/0 presentation at s = -1. These are the shifted monic form of DLMF 18.9.1 and 18.9.2_2.
2. Existing: package the recurrence as SatisfiesFavardRecurrence Q A B; favardInterlacing gives Prec (Q n) (Q (n+1)), and isRealRooted_of_favard gives splitting. Transfer back to S using Prec.C_mul_left/right and roots_C_mul.
3. Missing, small reusable strict-Favard bridge: prove adjacent no-common-roots by descending the recurrence through the nonzero Bₙ to Q 0 = 1. Combine this with existing exists_common_root_of_not_nodup and exists_common_root_of_not_nodup_g to obtain nodup root multisets, then the existing HasSimpleRoots/root-multiplicity API. Weak ListInterlaces plus no common root makes every displayed cross inequality strict. No new analytic theory is needed here.
4. Missing, Jacobi-specific localization: prove HasNonnegCoeffs ((S n).comp (-X)) directly from coeff_shiftedJacobi, and the reflection identity
   (S n α β).comp (1 - X) = C ((-1 : ℝ)^n) * S n β α.
   Existing Splits.comp_neg_X, roots_comp_neg_X, Polynomial.isRoot_comp, and the nonnegative-coefficient root-bound lemma then give 0 < r; reflection with swapped parameters gives r < 1. Endpoint nonvanishing already follows from shiftedJacobi_eval_zero/one. The reflection is DLMF Table 18.6.1.

This route is independently consistent with the classical theorem that orthogonal-polynomial zeros are simple, interior, and consecutively separating (DLMF 18.2(vi)); Jacobi admissibility and the weight are recorded in DLMF Table 18.3.1. It deliberately bypasses weighted integration for this root/interlacing endpoint. Jacobi orthogonality remains missing and must still be formalized later for the Euler-inverse moment argument; it is not a dependency of the shortest milestone-2 root proof.