Add finite shifted Jacobi polynomial algebra

[PerAlexandersson]

Milestone 1 of #424.

Summary

• define finite shifted Jacobi polynomials over ℝ by an explicit coefficient sum
• prove the coefficient formula, degree and leading coefficient under α, β > -1, and endpoint values at 0 and 1
• prove the derivative identity and shifted Jacobi differential equation by finite polynomial algebra
• expose the new public module through the sorted RealRooted.lean umbrella import

This deliberately does not attempt orthogonality, root location, parameter-gap interlacing, Euler-inverse pencils, or the A390883 client.

Verification

• AXLE 4.31: 8 declarations, 0 errors/lint warnings (request c5ad65d5-2b6c-4adb-8a6e-f4228a5973ac)
• lake-workspace build RealRooted.Mathlib.RingTheory.Polynomial.Jacobi: 2,969 jobs passed
• lake-workspace build RealRooted: 9,026 jobs passed
• scripts/check_root_imports.py: all 467 modules imported
• scripts/check_proof_status.py --self-test and project proof-status audit passed
• public theorem axiom audit: only propext, Classical.choice, Quot.sound
• no sorry/admit/source axioms and no lines over 100 columns