Formalize both branches of Lyapunov's indirect method

[math-experiments]

Closes #9.

Summary

• Add axiom-free Hurwitz, matrix-exponential, Fréchet-remainder, quadratic-form, and arbitrary-Q Lyapunov-equation infrastructure.
• Prove that a Hurwitz Jacobian gives finite-forward local exponential stability, with compatibility corollaries for the legacy API.
• Prove that a positive-real complex eigenpair gives forward instability via a real Hermitian quadratic certificate and generic Chetaev machinery.
• Update umbrella imports, README, roadmap, and blueprint.

The primary results quantify over finite forward solution segments, avoiding finite-escape vacuity. The stable theorem does not itself package forward-complete existence.

Checks

• lake build
• lake exe runLinter --no-build
• lake exe mk_all --check
• lake build :blueprint
• leanblueprint checkdecls
• lake build LeanForControl:docs
• git diff --check

[AnandGokhale]

Superseded by #17, which has been merged. This branch predated a subsequent directory reorg on main and could not be merged as-is (conflicts in LeanForControl.lean, README.md, blueprint/src/content.tex, Stability/plan.md, plus a dependency on a complexification helper that main's independent Hurwitz rewrite had dropped). #17 relocates this work into Stability/LyapunovIndirect/, fixes the conflicts and the dependency gap, and is now on main. Closing this one.