Add Hurwitz matrix foundation

[raaghav-t]

Summary

• define rate-indexed Hurwitz stability for real matrices through complex eigenpairs, with ordinary Hurwitz stability as the zero-rate case
• separate reusable predicates into LinearSystems/DefsHurwitz.lean and their basic theorem API into LinearSystems/Hurwitz.lean
• prove rate weakening, explicit zero-dimensional behavior, the correctly signed spectral-shift equivalence, and a one-by-one sanity check
• expose the core vocabulary through the umbrella import and blueprint, and update the README and stability roadmap to reflect the new foundation

Design

The definition uses nonzero eigenpairs of the entrywise complexification of a real matrix. This matches the matrix-vector equations already used by the Hautus development, avoids choosing an arbitrary eigenvalue enumeration, and makes the zero-dimensional case explicitly vacuous.

This is Phase 1 prerequisite work for #9. It does not attempt the indirect method of Lyapunov, Lyapunov-equation existence, or ODE/linearization arguments.

Provenance

• Standard terminology: entrywise complexification and the continuous-time Hurwitz and rate-indexed Hurwitz predicates.
• Standard result: the spectral-shift equivalence for A + αI, with the positive shift sign checked directly from the eigenpair equations.
• Original library infrastructure: zero-rate compatibility, rate monotonicity, the explicit Fin 0 convention, the complexification/matrix-vector shift bridge, and the direct one-by-one sanity check.

Each theorem and lemma carries the corresponding Reference: or Original: note in its source docstring.

Verification

• lake build LeanForControl.LinearSystems.DefsHurwitz
• lake build LeanForControl.LinearSystems.Hurwitz
• lake exe runLinter LeanForControl.LinearSystems.DefsHurwitz LeanForControl.LinearSystems.Hurwitz
• lake build
• lake exe runLinter
• lake build :blueprint
• leanblueprint web
• leanblueprint checkdecls (all 52 blueprint declarations)
• leanblueprint pdf, followed by visual inspection of the rendered Hurwitz section
• git diff --check
• confirmed no sorry, admit, or new axiom
• #print axioms for every new public declaration reports only propext, Classical.choice, and Quot.sound

The full build retains three pre-existing long-line warnings in Dini/DiniDeriv.lean and ODEs/ODE_properties.lean. The printable blueprint also retains one pre-existing undefined reference to lem:comparison-claim-1. This change introduces no new warning.