Prove oscillatory leading-principal interlacing

[PerAlexandersson]

Closes #421.

This is the complete assumption-free oscillatory-matrix endpoint. It integrates the determinant, irreducibility, and spectrum prerequisites developed in #423, #427, and #428, then adds the missing Whitney reduction and principal-section theorem.

The proof:

• performs explicit recursive Whitney elimination through adjacent nonnegative transvections;
• reduces every nonsingular totally nonnegative matrix with positive adjacent off-diagonals to an irreducible tridiagonal matrix while preserving the ambient and trailing characteristic polynomials;
• symmetrizes the tridiagonal matrix and applies checked Cauchy interlacing;
• proves consecutive principal characteristic polynomials have no common root by a formal continuant recurrence;
• transports the result to leading principal sections by simultaneous finite-index reversal.

The public APIs Matrix.IsTotallyNonneg.trailing_charpoly_strictInterlaces and Matrix.IsTotallyNonneg.leading_charpoly_strictInterlaces return polynomial interlacing, simple roots on both levels, root-disjointness, and positivity of every ambient root.

Consumer validation is complete locally at real-rooted-oeis-proofs checkpoint ba580a2: all A318107 endpoints (natDegree, nonvanishing, splitness, consecutive Interlaces, and Prec) are checked using this theorem.

Verification:

• lake-workspace build RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing — 3,461 jobs passed.
• A318107 focused integration build — 9,029 jobs passed in an isolated dependency checkout, with no manifest edit.
• #print axioms for both public APIs and all five A318107 endpoints reports only propext, Classical.choice, and Quot.sound.
• Diff, forbidden-token, and 100-column audits pass; there is no sorry, axiom, admit, or statement-only scaffold.