Add Hurwitz matrix foundation

[raaghav-t]

Summary

Add the Phase 1 Hurwitz vocabulary needed for #9: real matrices whose complex eigenpairs have strictly negative real parts, plus a strict rate-indexed variant. Definitions live in LinearSystems/Stability/DefsHurwitz.lean; basic results live in LinearSystems/Stability/Hurwitz.lean, with a local roadmap. Real matrices are embedded using Mathlib's Matrix.map directly.

The API proves zero-rate compatibility, rate weakening, explicit vacuous behavior in dimension zero, the equivalence between rate α and Hurwitz stability of A + αI, and a one-by-one sanity check. Umbrella imports, the blueprint, README, and stability roadmap are updated. The indirect method itself remains out of scope.

Reference and provenance

João P. Hespanha, Linear Systems Theory (2nd ed.), Princeton University Press, 2018: continuous-time stability and the Hurwitz eigenvalue criterion. Author's textbook page.

The strict rate predicate and rate/shift/scalar lemmas are elementary adaptations or consequences of that criterion, proved directly here; this does not claim the textbook states these exact Lean signatures. Zero-rate compatibility, the matrix-map bridge, and the empty-dimension convention are original formalization infrastructure. Source docstrings record this provenance.

Validation

• Targeted Hurwitz build, full lake build, and full lake exe runLinter pass.
• lake exe mk_all --check passes.
• lake build :blueprint, leanblueprint web, and leanblueprint checkdecls pass.
• All eight public declarations use only propext, Classical.choice, and Quot.sound.
• git diff --check passes; no new sorry, admit, or axioms; Lean toolchain and dependency revisions unchanged.

The full build retains three existing long-line warnings in unrelated Dini/ODE modules.

[AnandGokhale]

Hey,
Thanks for the PR, could you please place your results in a sub-directory called Stability or something similar, The approach of having many files under linear systems is not a scalable one.

[AnandGokhale]

Also, please add a reference from a paper or a textbook for any results you may have.

[AnandGokhale]

It feels like complexification is not really needed as a definition, you always eliminate it immediately by expanding its definition.