Expose ordered spectrum from primitive compounds

[PerAlexandersson]

Partial, reusable progress toward #421; this does not close the issue.

This PR strengthens the existing primitive-compound Gantmacher--Krein API with a positive eigenvalue enumeration in nonincreasing order, while preserving the old theorem as a backward-compatible wrapper. It also proves that separability of the characteristic polynomial upgrades the enumeration to StrictAnti, making algebraic simplicity the precise remaining Perron--Frobenius input.

The audit found that the repository does not yet contain the two larger classical layers needed for the requested endpoint: (1) primitive Perron-root algebraic simplicity together with the TN+nonsingular+positive-adjacent-off-diagonal oscillatory criterion, and (2) the sign-variation theorem that yields strict interlacing for consecutive leading principal sections. No axiom, sorry, or statement scaffold is added.

Verification:

• AXLE 4.31 checked both extracted proof steps.
• lake-workspace build RealRooted.Mathlib.LinearAlgebra.Matrix.GantmacherKrein passed (3,419 jobs).
• lake-workspace build RealRooted passed (9,025 jobs).
• Direct axiom audit reports only propext, Classical.choice, and Quot.sound.
• Diff, 100-column, and forbidden-token checks passed.

Refs #421.