Replaying source construction, interlacing, coefficient positivity, determinant and Routh checks.
Positive physical equilibria: 5 ; Routh unstable counts: [0, 1, 0, 1, 0]
Paper substrate window: certified_at_least_5 ; wider attempted window: not_certified
Source checks: 3239 ; exact Routh census n <= 6
The all-n equilibrium count is a paper theorem. Even-index stability beyond the finite census is not proved here. Numerical trajectories are not basin or robustness certificates; Lean not rerun.
