Add Hurwitz matrix foundation

LeanForControl.lean

@@ -10,7 +10,9 @@ import LeanForControl.Comparison.ComparisonFunctions
 import LeanForControl.Dini.DiniDeriv
 import LeanForControl.LinearSystems.Basic
 import LeanForControl.LinearSystems.Controllability
+import LeanForControl.LinearSystems.DefsHurwitz
 import LeanForControl.LinearSystems.Hautus
+import LeanForControl.LinearSystems.Hurwitz
 import LeanForControl.LinearSystems.MatrixLemmas
 import LeanForControl.LinearSystems.Observability
 import LeanForControl.ODEs.ComparisonLemma

LeanForControl/LinearSystems/Basic.lean

@@ -23,6 +23,5 @@ This keeps `Aᵏ` available as `A ^ (k : ℕ)` for `k : Fin n` without going
 through `Fin.val` extraction in every lemma.
 
 This file holds *only* shared imports and documentation. Definitions and proofs
-live in `LinearSystems.Controllability`, `LinearSystems.Observability`,
-and `LinearSystems.MatrixLemmas`.
+live in the sibling modules under `LeanForControl/LinearSystems`.
 -/

LeanForControl/LinearSystems/DefsHurwitz.lean

@@ -0,0 +1,55 @@
+import LeanForControl.LinearSystems.Basic
+import Mathlib.Analysis.Complex.Basic
+import Architect
+
+/-!
+# Definitions for Hurwitz matrices
+
+This file defines continuous-time Hurwitz stability for real square matrices through
+eigenpairs of their complexification. The eigenpair formulation matches the concrete
+matrix-vector equations used by the Hautus development and avoids choosing an enumeration
+of eigenvalues.
+
+The definition intentionally allows zero-dimensional matrices. In dimension zero there
+are no nonzero eigenvectors, so every matrix satisfies the predicate with every rate;
+`LinearSystems.isHurwitzWithRate_fin_zero` records this convention explicitly.
+
+Reference: standard continuous-time linear systems terminology.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {n : ℕ}
+
+/-- The entrywise complexification of a real matrix. -/
+noncomputable def complexification (A : Matrix (Fin n) (Fin n) ℝ) :
+    Matrix (Fin n) (Fin n) ℂ :=
+  A.map (algebraMap ℝ ℂ)
+
+/-- A real matrix is Hurwitz with decay rate `α` when every complex eigenvalue `μ`
+satisfies `μ.re < -α`.
+
+This is stated using nonzero eigenvectors rather than an eigenvalue enumeration so it can
+be used directly with PBH/Hautus arguments.
+
+Reference: standard continuous-time linear systems terminology. -/
+@[blueprint "def:isHurwitzWithRate"
+  (statement := /-- A real square matrix $A$ is \emph{Hurwitz with decay rate}
+    $\alpha$ when every complex eigenpair $(\mu,v)$ with $v \ne 0$ satisfies
+    $\operatorname{Re}(\mu) < -\alpha$. -/)]
+def IsHurwitzWithRate (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) : Prop :=
+  ∀ (μ : ℂ) (v : Fin n → ℂ), v ≠ 0 →
+    complexification A *ᵥ v = μ • v → μ.re < -α
+
+/-- A real matrix is Hurwitz when all of its complex eigenvalues have negative real part.
+
+Reference: standard continuous-time linear systems terminology. -/
+@[blueprint "def:isHurwitz"
+  (statement := /-- A real square matrix is \emph{Hurwitz} when every complex
+    eigenvalue has strictly negative real part. -/)]
+abbrev IsHurwitz (A : Matrix (Fin n) (Fin n) ℝ) : Prop :=
+  IsHurwitzWithRate 0 A
+
+end LinearSystems

LeanForControl/LinearSystems/Hurwitz.lean

@@ -0,0 +1,118 @@
+import LeanForControl.LinearSystems.DefsHurwitz
+import Architect
+
+/-!
+# Basic theorems for Hurwitz matrices
+
+This file establishes the basic reusable API for the Hurwitz predicates defined in
+`LeanForControl.LinearSystems.DefsHurwitz`.
+
+The definition intentionally allows zero-dimensional matrices. In dimension zero there
+are no nonzero eigenvectors, so every matrix is Hurwitz with every rate; the theorem
+`isHurwitzWithRate_fin_zero` records this convention explicitly.
+
+Reference: standard continuous-time spectral-shift properties; the remaining compatibility
+lemmas are original infrastructure for this library.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {n : ℕ}
+
+/-- Ordinary Hurwitz stability is exactly Hurwitz stability with rate zero.
+
+Original: this is the compatibility lemma for the rate-indexed definition. -/
+theorem isHurwitz_iff_isHurwitzWithRate_zero (A : Matrix (Fin n) (Fin n) ℝ) :
+    IsHurwitz A ↔ IsHurwitzWithRate 0 A :=
+  Iff.rfl
+
+/-- A certified Hurwitz decay rate may be weakened.
+
+Original: monotonicity of the rate-indexed predicate. -/
+theorem IsHurwitzWithRate.mono {A : Matrix (Fin n) (Fin n) ℝ} {α β : ℝ}
+    (hA : IsHurwitzWithRate α A) (hβα : β ≤ α) :
+    IsHurwitzWithRate β A := by
+  intro μ v hv hAv
+  have hμ := hA μ v hv hAv
+  linarith
+
+/-- Zero-dimensional matrices are Hurwitz with every rate, vacuously, because there is no
+nonzero eigenvector.
+
+Original: documents the chosen zero-dimensional convention. -/
+theorem isHurwitzWithRate_fin_zero (α : ℝ) (A : Matrix (Fin 0) (Fin 0) ℝ) :
+    IsHurwitzWithRate α A := by
+  intro μ v hv
+  exfalso
+  apply hv
+  funext i
+  exact i.elim0
+
+/-- Complexifying a real spectral shift and applying it to a vector adds the corresponding
+complex scalar multiple of that vector.
+
+Original: bridge used by the spectral-shift characterization. -/
+lemma complexification_add_smul_one_mulVec
+    (A : Matrix (Fin n) (Fin n) ℝ) (α : ℝ) (v : Fin n → ℂ) :
+    complexification (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) *ᵥ v =
+      complexification A *ᵥ v + (α : ℂ) • v := by
+  simp [complexification, Matrix.map_add, Matrix.map_smul', Matrix.add_mulVec,
+    Matrix.smul_mulVec]
+
+/-- A matrix has decay rate `α` exactly when shifting it by `α I` makes it Hurwitz.
+
+The sign is positive: an eigenvalue `μ` of `A` becomes `μ + α` for `A + α I`, so
+`Re μ < -α` is equivalent to `Re (μ + α) < 0`.
+
+Reference: the standard spectral-shift property for scalar multiples of the identity. -/
+@[blueprint "thm:isHurwitzWithRate-iff-spectral-shift"
+  (statement := /-- A real matrix $A$ is Hurwitz with decay rate $\alpha$ if and only if
+    the spectrally shifted matrix $A + \alpha I$ is Hurwitz. -/)
+  (proof := /-- A complex eigenvalue $\mu$ of $A$ becomes $\mu + \alpha$ after the shift,
+    and $\operatorname{Re}(\mu) < -\alpha$ is equivalent to
+    $\operatorname{Re}(\mu + \alpha) < 0$. -/)]
+theorem isHurwitzWithRate_iff_add_smul_one
+    (α : ℝ) (A : Matrix (Fin n) (Fin n) ℝ) :
+    IsHurwitzWithRate α A ↔ IsHurwitz (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) := by
+  constructor
+  · intro hA μ v hv hshift
+    have hbase : complexification A *ᵥ v = (μ - α) • v := by
+      rw [complexification_add_smul_one_mulVec] at hshift
+      rw [sub_smul]
+      exact eq_sub_of_add_eq hshift
+    have hμ := hA (μ - α) v hv hbase
+    simp only [Complex.sub_re, Complex.ofReal_re] at hμ
+    linarith
+  · intro hshift μ v hv hbase
+    have heig : complexification (A + α • (1 : Matrix (Fin n) (Fin n) ℝ)) *ᵥ v =
+        (μ + α) • v := by
+      rw [complexification_add_smul_one_mulVec, hbase]
+      simp [add_smul]
+    have hμ := hshift (μ + α) v hv heig
+    simp only [Complex.add_re, Complex.ofReal_re] at hμ
+    linarith
+
+/-- The one-by-one matrix with entry `-γ` has every decay rate strictly below `γ`.
+This is a concrete sanity check for the eigenpair definition and its sign convention.
+
+Original: direct computation included as a sanity check for the definition. -/
+theorem isHurwitzWithRate_neg_one_by_one {α γ : ℝ} (hαγ : α < γ) :
+    IsHurwitzWithRate α ((-γ) • (1 : Matrix (Fin 1) (Fin 1) ℝ)) := by
+  intro μ v hv hAv
+  have hv0 : v 0 ≠ 0 := by
+    intro hv0
+    apply hv
+    funext i
+    fin_cases i
+    exact hv0
+  have heig := congrFun hAv 0
+  have hμ : μ = (-γ : ℝ) := by
+    apply mul_right_cancel₀ hv0
+    simpa [complexification, Matrix.mulVec, dotProduct] using heig.symm
+  rw [hμ]
+  simp only [Complex.ofReal_re]
+  linarith
+
+end LinearSystems

LeanForControl/Stability/plan.md

@@ -140,12 +140,13 @@ Let f : ℝⁿ → ℝⁿ be C¹ with f(x_eq) = 0. Let A = fderiv ℝ f x_eq (th
 
 This theorem needs substantial external infrastructure:
 
-- **Hurwitz matrices**: `IsHurwitz A ↔ ∀ λ ∈ A.eigenvalues ℂ, λ.re < 0`
-  (partially developed in `Lyapunov_old/LinearSystems.lean`)
+- **Hurwitz matrices (Phase 1 foundation)**: ✅ `LinearSystems/DefsHurwitz.lean` defines
+  `IsHurwitzWithRate` through complex eigenpairs; `LinearSystems/Hurwitz.lean` provides
+  rate weakening, spectral shifting, and explicit zero-dimensional behavior.
 
 - **Lyapunov equation for Hurwitz matrices**: If A is Hurwitz, then for any Q ≻ 0 there exists
   a unique P ≻ 0 satisfying PA + AᵀP = -Q. Use Q = I for simplicity.
-  (sketched in `Lyapunov_old/LinearSystems.lean`, all sorry)
+  This is not yet implemented.
 
 - **Linearization error bound**: f(x) = Ax + g(x) where ‖g(x)‖/‖x‖ → 0 as x → x_eq.
   Lean path: Taylor's theorem / `HasFDerivAt` remainder bound.
@@ -166,8 +167,8 @@ Given P satisfying PA + AᵀP = -I:
 ### Priority assessment
 
 Linearization is low priority for immediate Lean work because:
-- It requires substantial eigenvalue/Hurwitz infrastructure not yet in the library.
-- The LinearSystems files have this sketched but all sorry.
+- It still requires Lyapunov-equation and linearization-remainder infrastructure.
+- Positive-definite matrix Lyapunov-equation existence is not yet formalized.
 - Proving the Lyapunov equation existence (Sylvester-type) is a significant standalone project.
 
 Suggested order: prove Chetaev's theorem first, then revisit linearization.
@@ -185,7 +186,7 @@ Suggested order: prove Chetaev's theorem first, then revisit linearization.
 3. ~~**Barbashin/Krasovskii corollaries**~~ — ✅ done in `LaSalle.lean`.
 
 4. **Linearization (indirect method)** — new file `Stability/Linearization.lean`.
-   Blocked on eigenvalue / Lyapunov equation infrastructure.
+   Blocked on Lyapunov-equation, linearization-remainder, and unstable-branch infrastructure.
    Estimated effort: 4+ sessions after unblocking.
 
 ---

README.md

@@ -73,7 +73,7 @@ LeanForControl/                          ← Lean source
 ├── ODEs/                                ← comparison lemma, Gronwall–Bellman, ODE existence
 ├── Dini/                                ← Dini derivatives (used by the comparison lemma)
 ├── Analysis/                            ← supporting real-analysis lemmas
-└── LinearSystems/                       ← matrices, observability, controllability, Hautus
+└── LinearSystems/                       ← matrices, observability, controllability, Hautus, Hurwitz
 blueprint/src/                           ← .tex sources (run leanblueprint web to render)
 docbuild/                                ← nested project for doc-gen4
 home_page/                               ← Jekyll scaffold for the project's home page

blueprint/src/content.tex

@@ -74,6 +74,18 @@ \subsection{Hautus controllability}
 
 \inputleannode{thm:isControllable-iff-hautus}
 
+\section{Hurwitz stability}
+
+For a real square matrix $A$, Hurwitz stability is expressed through the complex eigenpairs
+of its entrywise complexification. The rate-indexed predicate records a strict spectral
+margin, and ordinary Hurwitz stability is the zero-rate case.
+
+\inputleannode{def:isHurwitzWithRate}
+
+\inputleannode{def:isHurwitz}
+
+\inputleannode{thm:isHurwitzWithRate-iff-spectral-shift}
+
 \chapter{Ordinary differential equations}
 
 \section{Dini derivatives}