A176331 prerequisite: Jacobi (0,2) primitive zero-location backend

[PerAlexandersson]

Goal

Formalize the Jacobi-primitive zero-location theorem that supplies the missing
analytic endpoint in the current OEIS A176331 reduction.

For m >= 1, put

G_m(x)   = sum_(k=0)^m binom(m,k) binom(m+2,k) x^k,
q_m(s)   = s^m G_m((s-1)/(2s)),
Psi_m(s) = integral_(1)^s q_m(u) du.

Equivalently,

q_m(s) = ((1+s)/2)^m P_m^(0,2)((3s-1)/(1+s)).

The target theorem is that Psi_m has exactly m+1 simple real roots in
(0,1]: one between each pair of consecutive roots of q_m, together with
the forced root at 1.

Proof source now available

An all-rank paper proof was found in Aristotle project
0490dded-474e-4fb6-9ae1-1a1c75312e3b, task
eab53e84-0f04-4686-a819-1e59b84b8581. It proves every m >= 16 by a
Gauss--Jacobi / Markov--Stieltjes reduction followed by explicit Sturm--Bessel
comparison and an elementary integral bound; 1 <= m <= 15 are discharged by
exact rational Sturm certificates.

The proof specification and formalization boundary are recorded in
the A176331 workbench note.
This is a source for formalization, not an existing Lean proof or a published
peer-reviewed citation; its constants and analytic lemmas must be replayed
formally.

Why this belongs in RealRooted

The current A176331 branch already proves recurrence/model agreement, the
gamma-transform equivalence, and polar-rank descent. Its exact boundary is

R_m(s)  = s*q_m(s) - (m+1)*Psi_m(s),
R_m'(s) = s*q_m'(s) - m*q_m(s).

The Psi_m root theorem makes the boundary Jensen polynomial PF, after which
the existing polar descent reaches the required gamma rank and transfers
splitness back to the recurrence-defined row. Thus the missing content is a
reusable orthogonal-polynomial/Sturm backend, not another generated-file
recurrence wrapper.

RealRooted currently has a useful coefficient-level normalized Jacobi
P_n^(1,1) transport for the Braun--Jal development, but neither Mathlib nor
RealRooted has the P_n^(0,2) analytic theory, Gauss quadrature, or the
Sturm--Bessel comparison used here.

Proof skeleton

Let zeta_1 < ... < zeta_m be the roots of P_m^(0,2) and
eta_j = (1+zeta_j)/2.

1. Reduce the root count for Psi_m to alternating signs of the primitive at
   the roots of q_m.

2. Use one-sided orthogonality and Gauss--Jacobi quadrature to reduce the hard
   signs to

   A_j J_m(1-eta_j) > 2,
   A_j = (1-zeta_j^2) |(P_m^(0,2))'(zeta_j)|,
   J_m(d) = integral_0^1 (1+v)^(m+2) v^m / (v+d)^(m+1) dv.
   

3. The Jacobi contiguous relation and the Gauss-weight formula turn this into

   lambda_j < 8 eta_j (1-eta_j) J_m(1-eta_j)^2.
   

4. Apply Markov--Stieltjes:
   lambda_j < (8/3) eta_(j+1)^3.

5. Use Szego normal form and singular-endpoint Sturm comparison with J_0
   and J_2 to bound the first/last zeros and consecutive spacing.

6. Prove a log-concavity/chord lower bound for J_m; exact rational
   inequalities at m = 16 close every larger rank by monotonicity.

7. Check the first fifteen ranks with exact, kernel-checked Sturm/root-count
   certificates.

Suggested milestones

1. Define the normalized P_n^(0,2) polynomial by explicit coefficients and
   prove its recurrence, derivative/contiguous relation, and ODE.
2. Prove its roots are simple and lie in (-1,1), with an ordered root list.
3. Add the finite Gauss--Jacobi quadrature formula and the precise
   Markov--Stieltjes partial-weight inequality needed above.
4. Add a reusable singular-endpoint Sturm comparison lemma.
5. Either formalize the needed Bessel-zero bounds, or replace them by
   rational comparison functions that yield the same explicit constants.
6. Formalize the J_m lower bound and all rational constant checks.
7. Add a certificate-oriented finite Sturm/root-count frontend and discharge
   m <= 15.
8. Assemble the public Jacobi-primitive theorem, then consume it in the
   A176331 proof repository.

Milestones 1--4 should be separated into small modules and PRs; the full
analytic proof is too large for one generated-sequence patch.

Guardrails and completion criteria

• Do not introduce a JacobiPrimitiveStatement : Prop, a conditional
  *_splits_of_* wrapper presented as closure, or a finite-range substitute.
• Replace every decimal bound in the paper proof by an explicit rational
  inequality. Floating-point computation is not a theorem premise.
• Keep recurrence/model agreement in the OEIS repository separate from the
  analytic theorem here.
• No sorry, admit, source axiom, or hidden statement scaffold.
• Focused and full builds pass without new warnings; public endpoints receive
  an axiom audit and are imported from the root module.

This issue is unrelated to LGV and non-nesting rooks; those remain deferred.

[PerAlexandersson]

The exact OEIS-side client bridge is now formalized and axiom-audited in draft PR sqrt-of-2/real-rooted-oeis-proofs#114 (head 44bfc3f). It proves the shifted primitive normalization, derivative, and polar identity without introducing a conditional zero-location scaffold. The analytic Jacobi (0,2) theorem described in this issue remains the genuine blocker.