diff --git a/LeanForControl.lean b/LeanForControl.lean
index 2e8bf0c..77e616e 100644
--- a/LeanForControl.lean
+++ b/LeanForControl.lean
@@ -19,14 +19,18 @@ import LeanForControl.Comparison.DecaySystem
 import LeanForControl.Comparison.PositiveDefiniteBounds
 import LeanForControl.LinearSystems.Continuous
 import LeanForControl.LinearSystems.Controllability.Controllability
+import LeanForControl.LinearSystems.Controllability.Decomposition
 import LeanForControl.LinearSystems.Controllability.Defs
+import LeanForControl.LinearSystems.Controllability.DefsDecomposition
 import LeanForControl.LinearSystems.Controllability.Hautus
 import LeanForControl.LinearSystems.Controllability.Reachability
 import LeanForControl.LinearSystems.Discrete
 import LeanForControl.LinearSystems.KalmanDecomposition.Decomposition
 import LeanForControl.LinearSystems.KalmanDecomposition.DecompositionExamples
 import LeanForControl.LinearSystems.KalmanDecomposition.Defs
+import LeanForControl.LinearSystems.Observability.Decomposition
 import LeanForControl.LinearSystems.Observability.Defs
+import LeanForControl.LinearSystems.Observability.DefsDecomposition
 import LeanForControl.LinearSystems.Observability.Hautus
 import LeanForControl.LinearSystems.Observability.Observability
 import LeanForControl.LinearSystems.Solutions.CtsLTI
diff --git a/LeanForControl/LinearSystems/Controllability/Decomposition.lean b/LeanForControl/LinearSystems/Controllability/Decomposition.lean
new file mode 100644
index 0000000..5b819bc
--- /dev/null
+++ b/LeanForControl/LinearSystems/Controllability/Decomposition.lean
@@ -0,0 +1,110 @@
+import LeanForControl.LinearSystems.Controllability.DefsDecomposition
+
+/-!
+# Controllability of the controllable component
+
+The state and input maps restricted to the reachable subspace give a
+controllable matrix pair. This is the controllable-component conclusion
+of Hespanha's controllable decomposition (Theorem 13.2), without choosing a
+complement in the original state space.
+
+`IsControllable` uses finite input responses from the origin. The argument
+is algebraic over a field and does not require the state matrix to be invertible.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 13.2(2).
+This proves the component conclusion in any supplied basis.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {𝕜 : Type*} [Field 𝕜] {n m : ℕ}
+
+/-- An invariant subspace of the restricted state space containing the
+restricted input range is the whole space. -/
+private theorem reachable_invariant_eq_top
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
+    ∀ S : Submodule 𝕜 (reachableSubspace A B),
+      LinearMap.range (reachableInputMap A B) ≤ S →
+      S ∈ Module.End.invtSubmodule (reachableStateMap A B) → S = ⊤ := by
+  intro S hB hA
+  let T := S.map (reachableSubspace A B).subtype
+  have hTA : T ∈ Module.End.invtSubmodule A.mulVecLin := by
+    rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem] at hA ⊢
+    rintro x ⟨y, hy, rfl⟩
+    exact ⟨reachableStateMap A B y, hA _ hy, rfl⟩
+  have hTB : LinearMap.range B.mulVecLin ≤ T := by
+    rintro x ⟨u, rfl⟩
+    exact ⟨reachableInputMap A B u, hB ⟨u, rfl⟩, rfl⟩
+  have hR := reachableSubspace_le_of_invariant_of_range_le A B T hTA hTB
+  rw [eq_top_iff]
+  intro x _
+  obtain ⟨y, hy, hxy⟩ := hR x.property
+  have hyx : y = x := Subtype.ext hxy
+  simpa only [hyx] using hy
+
+/-- The restricted state matrix acts on basis coordinates exactly as the
+restricted state map. -/
+private lemma reachableStateMatrix_mulVec_coordinates
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    {r : ℕ} (b : Module.Basis (Fin r) 𝕜 (reachableSubspace A B))
+    (x : reachableSubspace A B) :
+    reachableStateMatrix A B b *ᵥ b.equivFun x =
+      b.equivFun (reachableStateMap A B x) := by
+  simpa [reachableStateMatrix, Module.Basis.equivFun_apply] using
+    LinearMap.toMatrix_mulVec_repr b
+      b (reachableStateMap A B) x
+
+/-- The restricted input matrix acts on standard input coordinates exactly
+as the restricted input map. -/
+private lemma reachableInputMatrix_mulVec_coordinates
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    {r : ℕ} (b : Module.Basis (Fin r) 𝕜 (reachableSubspace A B))
+    (u : Fin m → 𝕜) :
+    reachableInputMatrix A B b *ᵥ u =
+      b.equivFun (reachableInputMap A B u) := by
+  simpa [reachableInputMatrix, Module.Basis.equivFun_apply] using
+    LinearMap.toMatrix_mulVec_repr (Pi.basisFun 𝕜 (Fin m))
+      b (reachableInputMap A B) u
+
+/-- The matrices of the controllable component form a controllable pair.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 13.2(2).
+This proves the component conclusion in any supplied basis.
+The component conclusion holds in any supplied basis indexed by `Fin r`. -/
+@[blueprint "thm:reachable-matrices-controllable"
+  (statement := /-- Let $A_c,B_c$ be the matrices of the restricted maps
+    (\cref{def:reachable-state-matrix} and \cref{def:reachable-input-matrix}) in any
+    supplied basis of $\mathcal R(A,B)$ indexed by $\operatorname{Fin}(r)$.
+    Then $(A_c,B_c)$ is controllable
+    in the sense of \cref{def:isControllable}. -/)]
+theorem reachableMatrices_isControllable
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    {r : ℕ} (b : Module.Basis (Fin r) 𝕜 (reachableSubspace A B)) :
+    IsControllable (reachableStateMatrix A B b) (reachableInputMatrix A B b) := by
+  rw [← reachableSubspace_eq_top_iff_isControllable]
+  let S := reachableSubspace (reachableStateMatrix A B b) (reachableInputMatrix A B b)
+  let T := S.comap b.equivFun.toLinearMap
+  have hB : LinearMap.range (reachableInputMap A B) ≤ T := by
+    rintro x ⟨u, rfl⟩
+    change b.equivFun (reachableInputMap A B u) ∈ S
+    rw [← reachableInputMatrix_mulVec_coordinates]
+    exact range_B_le_reachableSubspace _ _ ⟨u, rfl⟩
+  have hA : T ∈ Module.End.invtSubmodule (reachableStateMap A B) := by
+    rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem]
+    intro x hx
+    change b.equivFun (reachableStateMap A B x) ∈ S
+    rw [← reachableStateMatrix_mulVec_coordinates]
+    exact reachableSubspace_invariant _ _ hx
+  have hT : T = ⊤ := reachable_invariant_eq_top A B T hB hA
+  rw [eq_top_iff]
+  intro z hz
+  let x := b.equivFun.symm z
+  have hx : x ∈ T := by rw [hT]; trivial
+  change b.equivFun x ∈ S at hx
+  change b.equivFun
+      (b.equivFun.symm z) ∈ S at hx
+  simpa only [LinearEquiv.apply_symm_apply] using hx
+
+end LinearSystems
diff --git a/LeanForControl/LinearSystems/Controllability/DefsDecomposition.lean b/LeanForControl/LinearSystems/Controllability/DefsDecomposition.lean
new file mode 100644
index 0000000..0d3d5e2
--- /dev/null
+++ b/LeanForControl/LinearSystems/Controllability/DefsDecomposition.lean
@@ -0,0 +1,73 @@
+import LeanForControl.LinearSystems.Controllability.Reachability
+import Mathlib.LinearAlgebra.Basis.Defs
+import Architect
+
+/-!
+# The controllable component
+
+Restrict the state and input maps to the reachable subspace. Their matrices
+represent the controllable component in a supplied finite basis, as in the
+controllable decomposition in Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 13.2.
+These restriction maps give a coordinate-free formulation of its component.
+The matrix definitions take the state basis as an explicit argument.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {𝕜 : Type*} [Field 𝕜] {n m : ℕ}
+
+/-- The restriction of `A` to the reachable subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 13.2;
+coordinate-free construction of the controllable component. -/
+@[blueprint "def:reachable-state-map"
+  (statement := /-- Let $\mathcal R(A,B)$ be the reachable subspace
+    (\cref{def:reachableSubspace}). Its invariance under $A$ defines the
+    restricted state map $A_c:\mathcal R(A,B)\to\mathcal R(A,B)$,
+    $A_c x=Ax$. -/)]
+noncomputable def reachableStateMap
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
+    Module.End 𝕜 (reachableSubspace A B) :=
+  A.mulVecLin.restrict (fun _ hx => reachableSubspace_invariant A B hx)
+
+/-- The input map `B` with values in the reachable subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 13.2;
+coordinate-free construction of the controllable component. -/
+@[blueprint "def:reachable-input-map"
+  (statement := /-- Since $\operatorname{im}B\subseteq\mathcal R(A,B)$,
+    the input map takes values in the reachable subspace:
+    $B_c:\mathbb F^m\to\mathcal R(A,B)$, $B_c u=Bu$. -/)]
+noncomputable def reachableInputMap
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
+    (Fin m → 𝕜) →ₗ[𝕜] reachableSubspace A B :=
+  B.mulVecLin.codRestrict (reachableSubspace A B) fun u =>
+    range_B_le_reachableSubspace A B ⟨u, rfl⟩
+
+/-- The matrix of the restricted state map in the supplied basis. -/
+@[blueprint "def:reachable-state-matrix"
+  (statement := /-- Given a basis $b$ of $\mathcal R(A,B)$ indexed by
+    $\operatorname{Fin}(r)$, let $A_c$ be the matrix of the restricted state
+    map (\cref{def:reachable-state-map}) in $b$. -/)]
+noncomputable def reachableStateMatrix
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    {r : ℕ} (b : Module.Basis (Fin r) 𝕜 (reachableSubspace A B)) :
+    Matrix (Fin r) (Fin r) 𝕜 :=
+  LinearMap.toMatrix b b (reachableStateMap A B)
+
+/-- The matrix of the restricted input map in the supplied state basis,
+with standard input coordinates. -/
+@[blueprint "def:reachable-input-matrix"
+  (statement := /-- Given the same basis $b$ as in
+    \cref{def:reachable-state-matrix}, let $B_c$ be the matrix of the
+    restricted input map (\cref{def:reachable-input-map}) in $b$ and the
+    standard input basis. -/)]
+noncomputable def reachableInputMatrix
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    {r : ℕ} (b : Module.Basis (Fin r) 𝕜 (reachableSubspace A B)) :
+    Matrix (Fin r) (Fin m) 𝕜 :=
+  LinearMap.toMatrix (Pi.basisFun 𝕜 (Fin m)) b (reachableInputMap A B)
+
+end LinearSystems
diff --git a/LeanForControl/LinearSystems/Controllability/Reachability.lean b/LeanForControl/LinearSystems/Controllability/Reachability.lean
index 7e287a5..79f78b0 100644
--- a/LeanForControl/LinearSystems/Controllability/Reachability.lean
+++ b/LeanForControl/LinearSystems/Controllability/Reachability.lean
@@ -14,7 +14,7 @@ controllability matrix and proves its invariance under the state matrix. The
 `A ^ n` boundary term in the invariance proof is closed by Cayley--Hamilton.
 
 References:
-* João P. Hespanha, *Linear Systems Theory*.
+* João P. Hespanha, *Linear Systems Theory* (2nd ed.), Theorems 11.5, 11.7, and 12.1.
 * R. E. Kalman, “Mathematical Description of Linear Dynamical Systems,”
   *Journal of the Society for Industrial and Applied Mathematics, Series A:
   Control* 1(2), 152–192, 1963. DOI: 10.1137/0301010.
@@ -32,7 +32,8 @@ variable {n m : ℕ}
 the product of `controllabilityMatrix A B` with a vector indexed by
 `Fin n × Fin m`.
 
-Original: formalization infrastructure for LeanForControl. -/
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived. -/
 @[blueprint "lem:mem-reachableSubspace-iff"
   (title := "Membership in the reachable subspace")
   (latexEnv := "lemma")
@@ -58,8 +59,9 @@ lemma mem_reachableSubspace_iff
 /-- Every individual finite-horizon input response belongs to the reachable
 subspace.
 
-Original: formalization infrastructure for LeanForControl. -/
-lemma finiteHorizonResponse_mem_reachableSubspace
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived. -/
+private lemma finiteHorizonResponse_mem_reachableSubspace
     (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
     (k : Fin n) (u : Fin m → 𝕜) :
     (A ^ (k : ℕ) * B) *ᵥ u ∈ reachableSubspace A B := by
@@ -77,7 +79,11 @@ lemma finiteHorizonResponse_mem_reachableSubspace
 /-- The reachable subspace is exactly the supremum of the ranges of the
 finite-horizon maps `A^k B`.
 
-Original: formalization infrastructure for LeanForControl. -/
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived. -/
+@[blueprint "thm:reachableSubspace-eq-sum-range"
+  (statement := /-- The reachable subspace is the sum of the finite-horizon
+    input ranges: $\mathcal R(A,B)=\sum_{k=0}^{n-1}\operatorname{im}(A^kB)$. -/)]
 theorem reachableSubspace_eq_iSup_range
     (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
     reachableSubspace A B =
@@ -94,9 +100,30 @@ theorem reachableSubspace_eq_iSup_range
     rintro x ⟨u, rfl⟩
     exact finiteHorizonResponse_mem_reachableSubspace A B k u
 
+/-- The dimension of the reachable subspace is the rank of the
+controllability matrix.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 12.1 (matrix test),
+using Theorem 11.5 for the reachable-subspace characterization. -/
+@[blueprint "thm:reachableSubspace-finrank"
+  (statement := /-- The dimension of the reachable subspace equals the rank
+    of the controllability matrix:
+    \[
+      \dim \mathcal R(A,B)=\operatorname{rank}\mathcal C(A,B).
+    \] -/)]
+theorem finrank_reachableSubspace_eq_rank_controllabilityMatrix
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
+    Module.finrank 𝕜 (reachableSubspace A B) =
+      Matrix.rank (controllabilityMatrix A B) := by
+  rfl
+
 /-- The image of the input matrix is contained in the reachable subspace.
 
-Reference: Hespanha, *Linear Systems Theory*. -/
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived. -/
+@[blueprint "thm:range-B-le-reachableSubspace"
+  (statement := /-- The input range is contained in the reachable subspace:
+    $\operatorname{im}B\subseteq\mathcal R(A,B)$. -/)]
 theorem range_B_le_reachableSubspace
     (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜) :
     LinearMap.range B.mulVecLin ≤ reachableSubspace A B := by
@@ -116,7 +143,8 @@ theorem range_B_le_reachableSubspace
 /-- The system is controllable exactly when its reachable subspace is the
 whole state space.
 
-Reference: Hespanha, *Linear Systems Theory*. -/
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 12.1 (matrix test),
+using Theorem 11.5 for the reachable-subspace characterization. -/
 @[blueprint "thm:reachableSubspace-eq-top-iff-controllable"
   (title := "Controllability via the reachable subspace")
   (statement := /-- A pair $(A,B)$ is controllable if and only if its
@@ -158,7 +186,8 @@ private lemma cayleyHamilton_boundary_mem_reachableSubspace
 /-- The finite-horizon reachable subspace is invariant under the state
 matrix.  The highest-power case is discharged by Cayley--Hamilton.
 
-Reference: Hespanha, *Linear Systems Theory*. -/
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived. -/
 @[blueprint "lem:reachableSubspace-invariant"
   (title := "$A$-invariance of the reachable subspace")
   (latexEnv := "lemma")
@@ -185,4 +214,38 @@ theorem reachableSubspace_invariant
     rw [heq]
     exact cayleyHamilton_boundary_mem_reachableSubspace A B (fun j => u (k, j))
 
+/-- Every `A`-invariant subspace containing the input range contains the
+reachable subspace. Together with `range_B_le_reachableSubspace` and
+`reachableSubspace_invariant`, this characterizes it as the smallest such subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 11.5 (controllability-matrix image);
+this finite-dimensional algebraic form is derived.
+This is a derived invariant-subspace characterization. -/
+@[blueprint "thm:reachableSubspace-least-invariant"
+  (statement := /-- If $S$ is $A$-invariant and contains $\operatorname{im}B$,
+    then $\mathcal R(A,B)\subseteq S$. Together with
+    \cref{lem:reachableSubspace-invariant} and
+    $\operatorname{im}B\subseteq\mathcal R(A,B)$, this says that the reachable
+    subspace is the smallest $A$-invariant subspace containing the input range. -/)]
+theorem reachableSubspace_le_of_invariant_of_range_le
+    (A : Matrix (Fin n) (Fin n) 𝕜) (B : Matrix (Fin n) (Fin m) 𝕜)
+    (S : Submodule 𝕜 (Fin n → 𝕜))
+    (hA : S ∈ Module.End.invtSubmodule A.mulVecLin)
+    (hB : LinearMap.range B.mulVecLin ≤ S) :
+    reachableSubspace A B ≤ S := by
+  rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem] at hA
+  have hpow : ∀ k : ℕ, ∀ u : Fin m → 𝕜, A ^ k *ᵥ (B *ᵥ u) ∈ S := by
+    intro k u
+    induction k with
+    | zero => simpa using hB ⟨u, rfl⟩
+    | succ k ih =>
+        rw [pow_succ', ← Matrix.mulVec_mulVec]
+        exact hA _ ih
+  rintro x hx
+  obtain ⟨u, rfl⟩ := (mem_reachableSubspace_iff x).mp hx
+  rw [controllabilityMatrix_mulVec_eq_sum]
+  exact S.sum_mem fun k _ => by
+    rw [← Matrix.mulVec_mulVec]
+    exact hpow k _
+
 end LinearSystems
diff --git a/LeanForControl/LinearSystems/Observability/Decomposition.lean b/LeanForControl/LinearSystems/Observability/Decomposition.lean
new file mode 100644
index 0000000..d1e500a
--- /dev/null
+++ b/LeanForControl/LinearSystems/Observability/Decomposition.lean
@@ -0,0 +1,123 @@
+import LeanForControl.LinearSystems.Observability.DefsDecomposition
+
+/-!
+# Observability of the observable component
+
+The state and output maps induced on the quotient by the unobservable
+subspace give an observable matrix pair. This is a quotient-space
+construction corresponding to the observable component.
+
+The scalar field is `ℂ` because the upstream `unobservableSubspace` and
+its invariance theorem are currently defined over `ℂ`.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 16.2(2).
+The quotient formulation proves the observable-component conclusion.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {n p : ℕ}
+
+/-- An invariant subspace of the quotient contained in the induced
+output kernel is zero. -/
+private theorem observable_invariant_eq_bot
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    ∀ S : Submodule ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C),
+      S ∈ Module.End.invtSubmodule (observableStateMap A C) →
+      S ≤ LinearMap.ker (observableOutputMap A C) → S = ⊥ := by
+  intro S hA hC
+  let T := S.comap (unobservableSubspace A C).mkQ
+  have hTA : T ∈ Module.End.invtSubmodule A.mulVecLin := by
+    rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem] at hA ⊢
+    intro x hx
+    change observableStateMap A C ((unobservableSubspace A C).mkQ x) ∈ S
+    exact hA _ hx
+  have hTC : T ≤ LinearMap.ker C.mulVecLin := by
+    intro x hx
+    rw [LinearMap.mem_ker]
+    have hout := hC hx
+    rw [LinearMap.mem_ker] at hout
+    simpa [observableOutputMap, Submodule.liftQ_apply] using hout
+  have hT := le_unobservableSubspace_of_invariant_of_le_ker A C T hTA hTC
+  rw [eq_bot_iff]
+  intro q hq
+  obtain ⟨x, rfl⟩ := (unobservableSubspace A C).mkQ_surjective q
+  have hxT : x ∈ T := hq
+  have hxN := hT hxT
+  exact (Submodule.Quotient.mk_eq_zero _).mpr hxN
+
+/-- The observable quotient state matrix acts on basis coordinates exactly
+as the induced quotient state map. -/
+private lemma observableStateMatrix_mulVec_coordinates
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    {r : ℕ} (b : Module.Basis (Fin r) ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C))
+    (x : (Fin n → ℂ) ⧸ unobservableSubspace A C) :
+    observableStateMatrix A C b *ᵥ
+        b.equivFun x =
+      b.equivFun
+        (observableStateMap A C x) := by
+  simpa [observableStateMatrix, Module.Basis.equivFun_apply] using
+    LinearMap.toMatrix_mulVec_repr b
+      b (observableStateMap A C) x
+
+/-- The observable quotient output matrix acts on basis coordinates exactly
+as the induced quotient output map. -/
+private lemma observableOutputMatrix_mulVec_coordinates
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    {r : ℕ} (b : Module.Basis (Fin r) ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C))
+    (x : (Fin n → ℂ) ⧸ unobservableSubspace A C) :
+    observableOutputMatrix A C b *ᵥ
+        b.equivFun x =
+      observableOutputMap A C x := by
+  simpa [observableOutputMatrix, Module.Basis.equivFun_apply] using
+    LinearMap.toMatrix_mulVec_repr b
+      (Pi.basisFun ℂ (Fin p)) (observableOutputMap A C) x
+
+/-- The matrices of the observable component form an observable pair.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 16.2(2).
+The quotient formulation proves the observable-component conclusion.
+The induced quotient pair is observable in any supplied basis indexed by `Fin r`. -/
+@[blueprint "thm:observable-matrices-observable"
+  (statement := /-- Let $A_o,C_o$ be the matrices of the induced maps
+    (\cref{def:observable-state-matrix} and \cref{def:observable-output-matrix}) in any
+    supplied basis of $\mathbb C^n/\mathcal N(A,C)$ indexed by $\operatorname{Fin}(r)$.
+    Then $(A_o,C_o)$ is observable
+    in the sense of \cref{def:isObservable}. -/)]
+theorem observableMatrices_isObservable
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    {r : ℕ} (b : Module.Basis (Fin r) ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C)) :
+    IsObservable (observableStateMatrix A C b) (observableOutputMatrix A C b) := by
+  rw [← unobservableSubspace_eq_bot_iff_isObservable]
+  let U := unobservableSubspace (observableStateMatrix A C b) (observableOutputMatrix A C b)
+  let S := U.comap b.equivFun.toLinearMap
+  have hA : S ∈ Module.End.invtSubmodule (observableStateMap A C) := by
+    rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem]
+    intro x hx
+    change b.equivFun (observableStateMap A C x) ∈ U
+    rw [← observableStateMatrix_mulVec_coordinates]
+    exact A_mulVec_mem_unobservableSubspace_of_mem hx
+  have hC : S ≤ LinearMap.ker (observableOutputMap A C) := by
+    intro x hx
+    rw [LinearMap.mem_ker]
+    rw [← observableOutputMatrix_mulVec_coordinates]
+    exact unobservableSubspace_le_ker_C _ _ hx
+  have hS : S = ⊥ := observable_invariant_eq_bot A C S hA hC
+  rw [eq_bot_iff]
+  intro z hz
+  let x := b.equivFun.symm z
+  have hx : x ∈ S := by
+    change b.equivFun x ∈ U
+    change b.equivFun
+      (b.equivFun.symm z) ∈ U
+    simpa only [LinearEquiv.apply_symm_apply] using hz
+  rw [hS] at hx
+  have hx0 : x = 0 := hx
+  calc
+    z = b.equivFun x := by
+      exact (b.equivFun.apply_symm_apply z).symm
+    _ = 0 := by rw [hx0, map_zero]
+
+end LinearSystems
diff --git a/LeanForControl/LinearSystems/Observability/DefsDecomposition.lean b/LeanForControl/LinearSystems/Observability/DefsDecomposition.lean
new file mode 100644
index 0000000..7b16641
--- /dev/null
+++ b/LeanForControl/LinearSystems/Observability/DefsDecomposition.lean
@@ -0,0 +1,75 @@
+import LeanForControl.LinearSystems.Observability.Observability
+import Mathlib.LinearAlgebra.Basis.Defs
+import Architect
+
+/-!
+# The observable component
+
+The state and output maps descend to the quotient by the unobservable
+subspace. This quotient-space construction corresponds to the observable
+component. The matrix definitions take the quotient basis as an explicit argument.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 16.2;
+coordinate-free quotient construction corresponding to its observable component.
+-/
+
+namespace LinearSystems
+
+open Matrix
+
+variable {n p : ℕ}
+
+/-- The state map induced on the quotient by the unobservable subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 16.2;
+coordinate-free quotient construction corresponding to its observable component.
+This is the quotient-space construction corresponding to the observable component. -/
+@[blueprint "def:observable-state-map"
+  (statement := /-- The invariance of $\mathcal N(A,C)$
+    (\cref{lem:unobservableSubspace-invariant}) defines a state map on
+    $\mathbb C^n/\mathcal N(A,C)$ by $A_o[x]=[Ax]$. -/)]
+noncomputable def observableStateMap
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    Module.End ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C) :=
+  (unobservableSubspace A C).mapQ (unobservableSubspace A C) A.mulVecLin
+    (by intro x hx; exact A_mulVec_mem_unobservableSubspace_of_mem hx)
+
+/-- The output map induced on the quotient by the unobservable subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 16.2;
+coordinate-free quotient construction corresponding to its observable component.
+This is the quotient-space construction corresponding to the observable component. -/
+@[blueprint "def:observable-output-map"
+  (statement := /-- Since $\mathcal N(A,C)\subseteq\ker C$
+    (\cref{lem:unobservableSubspace-le-ker-C}), the output map
+    descends to $\mathbb C^n/\mathcal N(A,C)$: $C_o[x]=Cx$. -/)]
+noncomputable def observableOutputMap
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    ((Fin n → ℂ) ⧸ unobservableSubspace A C) →ₗ[ℂ] (Fin p → ℂ) :=
+  (unobservableSubspace A C).liftQ C.mulVecLin (unobservableSubspace_le_ker_C A C)
+
+/-- The matrix of the induced state map in the supplied quotient basis. -/
+@[blueprint "def:observable-state-matrix"
+  (statement := /-- Given a basis $b$ of $\mathbb C^n/\mathcal N(A,C)$
+    indexed by $\operatorname{Fin}(r)$, let $A_o$ be the matrix of the
+    induced state map (\cref{def:observable-state-map}) in $b$. -/)]
+noncomputable def observableStateMatrix
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    {r : ℕ} (b : Module.Basis (Fin r) ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C)) :
+    Matrix (Fin r) (Fin r) ℂ :=
+  LinearMap.toMatrix b b (observableStateMap A C)
+
+/-- The matrix of the induced output map in the supplied quotient basis,
+with standard output coordinates. -/
+@[blueprint "def:observable-output-matrix"
+  (statement := /-- Given the same basis $b$ as in
+    \cref{def:observable-state-matrix}, let $C_o$ be the matrix of the
+    induced output map (\cref{def:observable-output-map}) in $b$ and the
+    standard output basis. -/)]
+noncomputable def observableOutputMatrix
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    {r : ℕ} (b : Module.Basis (Fin r) ℂ ((Fin n → ℂ) ⧸ unobservableSubspace A C)) :
+    Matrix (Fin p) (Fin r) ℂ :=
+  LinearMap.toMatrix b (Pi.basisFun ℂ (Fin p)) (observableOutputMap A C)
+
+end LinearSystems
diff --git a/LeanForControl/LinearSystems/Observability/Hautus.lean b/LeanForControl/LinearSystems/Observability/Hautus.lean
index ca50c43..5f360a9 100644
--- a/LeanForControl/LinearSystems/Observability/Hautus.lean
+++ b/LeanForControl/LinearSystems/Observability/Hautus.lean
@@ -3,7 +3,6 @@ import LeanForControl.LinearSystems.Observability.Observability
 import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.Data.Matrix.ColumnRowPartitioned
 import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
-import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
 import Architect
 
 /-!
@@ -22,12 +21,8 @@ The unobservable subspace `unobservableSubspace A C` and the block-row matrix
 `hautusObservabilityMatrix A C μ = [μI - A; C]` are defined in
 `LinearSystems.Observability.Defs`. This file develops:
 
-* `mem_unobservableSubspace_iff` and the bridge
-  `unobservableSubspace A C = ⊥ ↔ IsObservable A C`.
-* Cayley-Hamilton helper: vectors in `unobservableSubspace` are killed by
-  `C * A^n` too, not just `C * A^k` for `k < n`
-  (via `MatrixAlgebra.pow_card_eq_neg_sum_charpoly_coeff`).
-* `A`-invariance of `unobservableSubspace`.
+* Foundational unobservable-subspace facts are imported from `Observability`.
+* `hautusObservabilityMatrix A C μ` — the block-row matrix `[μI - A; C]`.
 * Failure direction: `¬ IsObservable A C → ∃ μ, witness vector` via
   eigenvector extraction on `unobservableSubspace`.
 * Converse: a Hautus-failure witness violates observability directly.
@@ -36,6 +31,8 @@ The unobservable subspace `unobservableSubspace A C` and the block-row matrix
 The dual controllability Hautus lemma lives in
 `LinearSystems.Controllability.Hautus`, which imports this file and routes
 through the transpose rather than repeating the eigenvector argument.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.9 (PBH observability test).
 -/
 
 namespace LinearSystems
@@ -44,84 +41,6 @@ open Matrix
 
 variable {n p : ℕ}
 
-lemma mem_unobservableSubspace_iff
-    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
-    (v : Fin n → ℂ) :
-    v ∈ unobservableSubspace A C
-      ↔ ∀ k : Fin n, (C * A ^ (k : ℕ)) *ᵥ v = 0 := by
-  simp [unobservableSubspace, Submodule.mem_iInf, LinearMap.mem_ker]
-
-/-- The unobservable subspace is trivial exactly when the system is observable
-in the textbook sense `IsObservable`. -/
-@[blueprint "thm:unobservable-eq-bot-iff-observable"
-  (title := "Observability via the unobservable subspace")
-  (statement := /-- A finite-dimensional system $(A, C)$ is observable in the
-    sense of \cref{def:isObservable} if and only if its unobservable subspace
-    is trivial:
-    \[
-      \mathcal{N}(A, C) = \{0\} \iff \mathrm{IsObservable}(A, C).
-    \] -/)
-  (proof := /-- Both directions are membership unfoldings of
-    \cref{def:unobservableSubspace} against \cref{def:isObservable}. -/)]
-theorem unobservableSubspace_eq_bot_iff_isObservable
-    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
-    unobservableSubspace A C = ⊥ ↔ IsObservable A C := by
-  rw [Submodule.eq_bot_iff]
-  unfold IsObservable
-  refine ⟨fun h v hv => ?_, fun h v hv => ?_⟩
-  · exact h v ((mem_unobservableSubspace_iff v).mpr hv)
-  · exact h v ((mem_unobservableSubspace_iff v).mp hv)
-
-/-- Cayley-Hamilton consequence: a vector in the unobservable subspace is
-also annihilated by `C * A^n`, not just by `C * A^k` for `k < n`. The single
-extra power closes the gap that `A`-invariance needs. -/
-private lemma mulVec_aPowN_eq_zero_of_mem_unobservableSubspace
-    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
-    {v : Fin n → ℂ} (hv : v ∈ unobservableSubspace A C) :
-    (C * A ^ n) *ᵥ v = 0 := by
-  -- By Cayley--Hamilton `Aⁿ` is a combination of the lower powers `A⁰, …, Aⁿ⁻¹`, and each
-  -- `(C Aⁱ) v` with `i < n` vanishes because `v` is unobservable.
-  rw [mem_unobservableSubspace_iff] at hv
-  have hCH : A ^ n = -∑ i ∈ Finset.range n, A.charpoly.coeff i • A ^ i := by
-    have h := MatrixAlgebra.pow_card_eq_neg_sum_charpoly_coeff A
-    rwa [Fintype.card_fin] at h
-  have hlower : ∀ i ∈ Finset.range n, (C * A.charpoly.coeff i • A ^ i) *ᵥ v = 0 := by
-    intro i hi
-    rw [Finset.mem_range] at hi
-    rw [Matrix.mul_smul, Matrix.smul_mulVec, hv ⟨i, hi⟩, smul_zero]
-  rw [hCH, Matrix.mul_neg, Matrix.neg_mulVec, Matrix.mul_sum, Matrix.sum_mulVec,
-    Finset.sum_eq_zero hlower, neg_zero]
-
-/-- The unobservable subspace is `A`-invariant: applying `A` to any
-unobservable state keeps it unobservable. The proof for the boundary case
-`k = n - 1` uses Cayley-Hamilton through
-`mulVec_aPowN_eq_zero_of_mem_unobservableSubspace`. -/
-@[blueprint "lem:unobservableSubspace-invariant"
-  (title := "$A$-invariance of the unobservable subspace")
-  (latexEnv := "lemma")
-  (statement := /-- The unobservable subspace is closed under the action of
-    $A$: for every $v \in \mathcal{N}(A, C)$, also $A\, v \in \mathcal{N}(A, C)$. -/)
-  (proof := /-- For $k = 0, \dots, n-2$ this is direct from the definition.
-    For $k = n - 1$ we land at $C\, A^{n}\, v$, which Cayley-Hamilton
-    rewrites as a $\mathbb{C}$-linear combination of $C\, A^{i}\, v$ for
-    $i < n$. Each of those is zero, so the combination is zero. -/)]
-lemma A_mulVec_mem_unobservableSubspace_of_mem
-    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
-    {v : Fin n → ℂ} (hv : v ∈ unobservableSubspace A C) :
-    A *ᵥ v ∈ unobservableSubspace A C := by
-  rw [mem_unobservableSubspace_iff]
-  intro k
-  -- Bridge `(C * A^k.val) *ᵥ (A *ᵥ v) = (C * A^(k.val + 1)) *ᵥ v`.
-  rw [Matrix.mulVec_mulVec, Matrix.mul_assoc, ← pow_succ]
-  by_cases hk : k.val + 1 < n
-  · exact (mem_unobservableSubspace_iff v).mp hv ⟨k.val + 1, hk⟩
-  · -- `k.val + 1 = n`, so use the Cayley-Hamilton helper.
-    push Not at hk
-    have hk_lt : k.val < n := k.isLt
-    have heq : k.val + 1 = n := by omega
-    rw [heq]
-    exact mulVec_aPowN_eq_zero_of_mem_unobservableSubspace hv
-
 /-- If the unobservable subspace is non-trivial, it contains a nonzero
 eigenvector of `A` (over `ℂ`). The eigenvector lifts to the ambient space
 `Fin n → ℂ` and is automatically annihilated by `C` (membership at `k = 0`). -/
diff --git a/LeanForControl/LinearSystems/Observability/Observability.lean b/LeanForControl/LinearSystems/Observability/Observability.lean
index e8698ad..fd580ed 100644
--- a/LeanForControl/LinearSystems/Observability/Observability.lean
+++ b/LeanForControl/LinearSystems/Observability/Observability.lean
@@ -1,5 +1,8 @@
 import LeanForControl.LinearSystems.Observability.Defs
 import LeanForControl.MatrixAlgebra.Rank
+import Mathlib.Algebra.Module.Submodule.Invariant
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
 import Architect
 
 /-!
@@ -154,4 +157,196 @@ theorem isObservable_iff_observabilityMatrix_rank_eq
     (observabilityMatrix A C)).trans ?_
   rw [Fintype.card_fin]
 
+/-- Membership in the unobservable subspace means that every finite-horizon
+output vanishes.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence. -/
+@[blueprint "lem:mem-unobservableSubspace-iff"
+  (statement := /-- A state $x$ belongs to $\mathcal N(A,C)$ if and only if
+    $CA^k x=0$ for every $k=0,\ldots,n-1$. -/)]
+lemma mem_unobservableSubspace_iff
+    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
+    (v : Fin n → ℂ) :
+    v ∈ unobservableSubspace A C
+      ↔ ∀ k : Fin n, (C * A ^ (k : ℕ)) *ᵥ v = 0 := by
+  simp [unobservableSubspace, Submodule.mem_iInf, LinearMap.mem_ker]
+
+/-- The unobservable subspace is trivial exactly when the system is observable
+in the textbook sense `IsObservable`.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence. -/
+@[blueprint "thm:unobservable-eq-bot-iff-observable"
+  (title := "Observability via the unobservable subspace")
+  (statement := /-- A finite-dimensional system $(A, C)$ is observable in the
+    sense of \cref{def:isObservable} if and only if its unobservable subspace
+    is trivial:
+    \[
+      \mathcal{N}(A, C) = \{0\} \iff \mathrm{IsObservable}(A, C).
+    \] -/)
+  (proof := /-- Both directions are membership unfoldings of
+    \cref{def:unobservableSubspace} against \cref{def:isObservable}. -/)]
+theorem unobservableSubspace_eq_bot_iff_isObservable
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    unobservableSubspace A C = ⊥ ↔ IsObservable A C := by
+  rw [Submodule.eq_bot_iff]
+  unfold IsObservable
+  refine ⟨fun h v hv => ?_, fun h v hv => ?_⟩
+  · exact h v ((mem_unobservableSubspace_iff v).mpr hv)
+  · exact h v ((mem_unobservableSubspace_iff v).mp hv)
+
+/-- Cayley-Hamilton consequence: a vector in the unobservable subspace is
+also annihilated by `C * A^n`, not just by `C * A^k` for `k < n`. The single
+extra power closes the gap that `A`-invariance needs. -/
+private lemma mulVec_aPowN_eq_zero_of_mem_unobservableSubspace
+    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
+    {v : Fin n → ℂ} (hv : v ∈ unobservableSubspace A C) :
+    (C * A ^ n) *ᵥ v = 0 := by
+  rw [mem_unobservableSubspace_iff] at hv
+  have hCH : A ^ n = -∑ i ∈ Finset.range n, A.charpoly.coeff i • A ^ i := by
+    have h := MatrixAlgebra.pow_card_eq_neg_sum_charpoly_coeff A
+    rwa [Fintype.card_fin] at h
+  have hlower : ∀ i ∈ Finset.range n, (C * A.charpoly.coeff i • A ^ i) *ᵥ v = 0 := by
+    intro i hi
+    rw [Finset.mem_range] at hi
+    rw [Matrix.mul_smul, Matrix.smul_mulVec, hv ⟨i, hi⟩, smul_zero]
+  rw [hCH, Matrix.mul_neg, Matrix.neg_mulVec, Matrix.mul_sum, Matrix.sum_mulVec,
+    Finset.sum_eq_zero hlower, neg_zero]
+
+/-- The unobservable subspace is `A`-invariant: applying `A` to any
+unobservable state keeps it unobservable. The proof for the boundary case
+`k = n - 1` uses Cayley-Hamilton through
+`mulVec_aPowN_eq_zero_of_mem_unobservableSubspace`.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence. -/
+@[blueprint "lem:unobservableSubspace-invariant"
+  (title := "$A$-invariance of the unobservable subspace")
+  (latexEnv := "lemma")
+  (statement := /-- The unobservable subspace is closed under the action of
+    $A$: for every $v \in \mathcal{N}(A, C)$, also $A\, v \in \mathcal{N}(A, C)$. -/)
+  (proof := /-- For $k = 0, \dots, n-2$ this is direct from the definition.
+    For $k = n - 1$ we land at $C\, A^{n}\, v$, which Cayley-Hamilton
+    rewrites as a $\mathbb{C}$-linear combination of $C\, A^{i}\, v$ for
+    $i < n$. Each of those is zero, so the combination is zero. -/)]
+lemma A_mulVec_mem_unobservableSubspace_of_mem
+    {A : Matrix (Fin n) (Fin n) ℂ} {C : Matrix (Fin p) (Fin n) ℂ}
+    {v : Fin n → ℂ} (hv : v ∈ unobservableSubspace A C) :
+    A *ᵥ v ∈ unobservableSubspace A C := by
+  rw [mem_unobservableSubspace_iff]
+  intro k
+  -- Bridge `(C * A^k.val) *ᵥ (A *ᵥ v) = (C * A^(k.val + 1)) *ᵥ v`.
+  rw [Matrix.mulVec_mulVec, Matrix.mul_assoc, ← pow_succ]
+  by_cases hk : k.val + 1 < n
+  · exact (mem_unobservableSubspace_iff v).mp hv ⟨k.val + 1, hk⟩
+  · -- `k.val + 1 = n`, so use the Cayley-Hamilton helper.
+    push Not at hk
+    have heq : k.val + 1 = n := by omega
+    rw [heq]
+    exact mulVec_aPowN_eq_zero_of_mem_unobservableSubspace hv
+
+/-- The unobservable subspace is exactly the kernel of the observability
+matrix acting by matrix-vector multiplication.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence. -/
+@[blueprint "thm:unobservableSubspace-eq-ker-observabilityMatrix"
+  (statement := /-- The unobservable subspace is the kernel of the
+    observability matrix:
+    \[
+      \mathcal N(A,C)=\ker \mathcal O(A,C).
+    \] -/)]
+theorem unobservableSubspace_eq_ker_observabilityMatrix
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    unobservableSubspace A C =
+      LinearMap.ker (observabilityMatrix A C).mulVecLin := by
+  ext v
+  simp only [unobservableSubspace, Submodule.mem_iInf, LinearMap.mem_ker]
+  constructor
+  · intro h
+    funext ki
+    exact congrFun (h ki.1) ki.2
+  · intro h k
+    funext i
+    exact congrFun h (k, i)
+
+/-- The dimension of the unobservable subspace plus the rank of the
+observability matrix is the state dimension.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence.
+This is the rank-nullity consequence of the observability-matrix kernel description. -/
+@[blueprint "thm:unobservableSubspace-finrank-add-rank"
+  (statement := /-- The dimension of the unobservable subspace plus the rank
+    of the observability matrix is the state dimension:
+    \[
+      \dim \mathcal N(A,C)+\operatorname{rank}\mathcal O(A,C)=n.
+    \] -/)]
+theorem finrank_unobservableSubspace_add_rank_observabilityMatrix
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    Module.finrank ℂ (unobservableSubspace A C) +
+      Matrix.rank (observabilityMatrix A C) = n := by
+  rw [unobservableSubspace_eq_ker_observabilityMatrix]
+  have h :=
+    LinearMap.finrank_range_add_finrank_ker (observabilityMatrix A C).mulVecLin
+  rw [Module.finrank_pi, Fintype.card_fin] at h
+  unfold Matrix.rank
+  omega
+
+/-- The unobservable subspace is contained in the output kernel.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence.
+This follows from the zero-time output condition. -/
+@[blueprint "lem:unobservableSubspace-le-ker-C"
+  (statement := /-- The unobservable subspace is contained in the output
+    kernel: $\mathcal N(A,C)\subseteq\ker C$. -/)]
+lemma unobservableSubspace_le_ker_C
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ) :
+    unobservableSubspace A C ≤ LinearMap.ker C.mulVecLin := by
+  intro x hx
+  rw [LinearMap.mem_ker]
+  by_cases hn : n = 0
+  · subst n
+    have hx0 : x = 0 := Subsingleton.elim _ _
+    rw [hx0, map_zero]
+  · have h0 :=
+      (show ∀ k : Fin n, (C * A ^ (k : ℕ)) *ᵥ x = 0 from
+        by simpa [unobservableSubspace, Submodule.mem_iInf, LinearMap.mem_ker] using hx)
+        ⟨0, Nat.pos_of_ne_zero hn⟩
+    simpa using h0
+
+/-- Every `A`-invariant subspace contained in the output kernel is contained
+in the unobservable subspace.
+
+Reference: Hespanha, *Linear Systems Theory* (2nd ed.), Theorem 15.7 (observability-matrix kernel);
+the algebraic characterization here is a derived consequence.
+This is a derived invariant-subspace characterization. -/
+@[blueprint "thm:unobservableSubspace-greatest-invariant"
+  (statement := /-- Every $A$-invariant subspace contained in $\ker C$ is
+    contained in the unobservable subspace. -/)]
+theorem le_unobservableSubspace_of_invariant_of_le_ker
+    (A : Matrix (Fin n) (Fin n) ℂ) (C : Matrix (Fin p) (Fin n) ℂ)
+    (S : Submodule ℂ (Fin n → ℂ))
+    (hA : S ∈ Module.End.invtSubmodule A.mulVecLin)
+    (hC : S ≤ LinearMap.ker C.mulVecLin) :
+    S ≤ unobservableSubspace A C := by
+  rw [Module.End.mem_invtSubmodule_iff_forall_mem_of_mem] at hA
+  intro x hx
+  simp only [unobservableSubspace, Submodule.mem_iInf, LinearMap.mem_ker]
+  intro k
+  have hpow : ∀ j : ℕ, A ^ j *ᵥ x ∈ S := by
+    intro j
+    induction j with
+    | zero => simpa using hx
+    | succ j ih =>
+        rw [pow_succ', ← Matrix.mulVec_mulVec]
+        exact hA _ ih
+  have hzero := hC (hpow k)
+  rw [LinearMap.mem_ker] at hzero
+  change (C * A ^ (k : ℕ)) *ᵥ x = 0
+  rw [← Matrix.mulVec_mulVec]
+  exact hzero
+
 end LinearSystems
diff --git a/LeanForControl/LinearSystems/plan.md b/LeanForControl/LinearSystems/plan.md
index e833199..3af90ae 100644
--- a/LeanForControl/LinearSystems/plan.md
+++ b/LeanForControl/LinearSystems/plan.md
@@ -27,13 +27,15 @@ LeanForControl/
       Defs.lean                 reachable subspace
       Reachability.lean         reachable-subspace characterizations, A-invariance
       Hautus.lean               controllability PBH test, via duality with Observability
-      Decomposition.lean        standalone controllable decomposition (planned)
+      DefsDecomposition.lean    restricted maps and explicit-basis matrices
+      Decomposition.lean        controllability of the restricted component
 
     Observability/
       Defs.lean                 observability matrix and predicate
-      Observability.lean        observability matrix, rank/kernel forms
-      Hautus.lean               unobservable subspace, observability PBH test
-      Decomposition.lean        standalone observable decomposition (planned)
+      Observability.lean        rank/kernel forms and unobservable-subspace facts
+      Hautus.lean               observability PBH test
+      DefsDecomposition.lean    quotient maps and explicit-basis matrices
+      Decomposition.lean        observability of the quotient component
 
     KalmanDecomposition/         needs both Controllability/ and Observability/
       Defs.lean                 the four coordinate sectors and their lattice relations
@@ -159,26 +161,39 @@ visible gap rather than an unstated assumption that this library is continuous-t
 
 | Result | Lean name | File | Status |
 |---|---|---|---|
-| Controllability matrix | `controllabilityMatrix` | `Controllability/Controllability.lean` | ✅ done |
+| Controllability matrix | `controllabilityMatrix` | `Controllability/Defs.lean` | ✅ done |
 | Controllability ⟺ full row rank | `isControllable_iff_controllabilityMatrix_rank_eq` | `Controllability/Controllability.lean` | ✅ done |
 | Reachable subspace | `reachableSubspace` | `Controllability/Defs.lean` | ✅ done |
 | Reachable subspace ⟺ controllability | `reachableSubspace_eq_top_iff_isControllable` | `Controllability/Reachability.lean` | ✅ done |
 | PBH test for controllability | `isControllable_iff_hautus` | `Controllability/Hautus.lean` | ✅ done |
 | Controllability/observability duality | `isControllable_iff_isObservable_transpose` | `Controllability/Hautus.lean` | ✅ done |
-| Controllable decomposition (standalone) | — | `Controllability/Decomposition.lean` | planned |
+| Controllable component on the reachable subspace | `reachableMatrices_isControllable` | `Controllability/{DefsDecomposition,Decomposition}.lean` | proved (PR #20) |
 | Stabilizability | — | `Controllability/Hautus.lean` | planned |
-| Observability matrix | `observabilityMatrix` | `Observability/Observability.lean` | ✅ done |
+| Observability matrix | `observabilityMatrix` | `Observability/Defs.lean` | ✅ done |
 | Observability ⟺ trivial kernel | `isObservable_iff_observabilityMatrix_ker_trivial` | `Observability/Observability.lean` | ✅ done |
 | Observability ⟺ full column rank | `isObservable_iff_observabilityMatrix_rank_eq` | `Observability/Observability.lean` | ✅ done |
-| Unobservable subspace, `A`-invariance | `unobservableSubspace` | `Observability/Hautus.lean` | ✅ done |
+| Unobservable subspace, `A`-invariance | `unobservableSubspace` | `Observability/{Defs,Observability}.lean` | ✅ done |
 | PBH test for observability | `isObservable_iff_hautus` | `Observability/Hautus.lean` | ✅ done |
-| Observable decomposition (standalone) | — | `Observability/Decomposition.lean` | planned |
+| Observable component on the quotient by the unobservable subspace | `observableMatrices_isObservable` | `Observability/{DefsDecomposition,Decomposition}.lean` | proved (PR #20) |
 | Detectability | — | `Observability/Hautus.lean` | planned |
 | Four coordinate sectors | — | `KalmanDecomposition/Defs.lean` | ✅ done |
 | Kalman decomposition | `exists_kalmanDecomposition` | `KalmanDecomposition/Decomposition.lean` | ✅ done |
 | Block zero pattern of the decomposition | `kalman_block_matrix_zero_pattern` | `KalmanDecomposition/Decomposition.lean` | ✅ done |
 | Minimal realizations | — | — | planned, no directory settled (needs both — see open questions) |
 
+The component modules correspond to Hespanha, *Linear Systems Theory* (2nd ed.),
+Theorems 13.2(2) and 16.2(2), respectively. Their restriction/quotient
+constructions express component properties without formalizing the full
+similarity-decomposition theorems.
+They retain separate definitions and theorems, following `CONTRIBUTING.md`.
+The four coordinate matrices take explicit bases indexed by `Fin r`; both component
+properties hold for every such basis. The observable definitions import only
+`Observability.lean`, where the foundational unobservable-subspace facts live.
+Only the component pairs are constructed here; no new ambient block similarity
+or transfer-function theorem is claimed. Restriction is field-generic. The quotient
+uses the existing complex unobservable-subspace API; generalizing that API and its
+Hautus consumers is deferred.
+
 ## Status: solutions
 
 | Result | Lean name | File | Status |
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index 960a20b..a96bfed 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -1474,14 +1474,26 @@ \subsection{Rank characterizations}
 
 \inputleannode{thm:isControllable-iff-rank}
 
-\subsection{Hautus observability}
+\subsection{Unobservable subspace}
 
 \inputleannode{def:unobservableSubspace}
 
+\inputleannode{lem:mem-unobservableSubspace-iff}
+
 \inputleannode{thm:unobservable-eq-bot-iff-observable}
 
 \inputleannode{lem:unobservableSubspace-invariant}
 
+\inputleannode{thm:unobservableSubspace-eq-ker-observabilityMatrix}
+
+\inputleannode{thm:unobservableSubspace-finrank-add-rank}
+
+\inputleannode{lem:unobservableSubspace-le-ker-C}
+
+\inputleannode{thm:unobservableSubspace-greatest-invariant}
+
+\subsection{Hautus observability}
+
 \inputleannode{def:hautusObservabilityMatrix}
 
 \inputleannode{lem:hautus-mulVec-eq-zero-iff}
@@ -1498,16 +1510,58 @@ \subsection{Hautus controllability}
 
 \inputleannode{thm:isControllable-iff-hautus}
 
-\section{Reachable subspace and Kalman decomposition}
+\section{Reachable subspace and controllable component}
 
 \inputleannode{def:reachableSubspace}
 
 \inputleannode{lem:mem-reachableSubspace-iff}
 
+\inputleannode{thm:reachableSubspace-eq-sum-range}
+
+\inputleannode{thm:range-B-le-reachableSubspace}
+
 \inputleannode{thm:reachableSubspace-eq-top-iff-controllable}
 
 \inputleannode{lem:reachableSubspace-invariant}
 
+The following algebraic constructions describe the controllable and observable
+components of the decompositions in Hespanha, \emph{Linear Systems Theory}
+(2nd ed.), Theorems 13.2(2) and 16.2(2). The reachable-subspace and
+observability-matrix facts correspond to Theorems 11.5, 12.1, and 15.7;
+the invariant-subspace and rank-nullity formulations are derived.
+The controllability predicate here means reachability from the origin, expressed
+by the finite controllability matrix. The controllable component is obtained by
+restriction; the observable component is represented by a quotient. The matrices
+take finite state bases as explicit arguments.
+
+\inputleannode{thm:reachableSubspace-finrank}
+
+\inputleannode{thm:reachableSubspace-least-invariant}
+
+\inputleannode{def:reachable-state-map}
+
+\inputleannode{def:reachable-input-map}
+
+\inputleannode{def:reachable-state-matrix}
+
+\inputleannode{def:reachable-input-matrix}
+
+\inputleannode{thm:reachable-matrices-controllable}
+
+\section{Observable component}
+
+\inputleannode{def:observable-state-map}
+
+\inputleannode{def:observable-output-map}
+
+\inputleannode{def:observable-state-matrix}
+
+\inputleannode{def:observable-output-matrix}
+
+\inputleannode{thm:observable-matrices-observable}
+
+\section{Kalman decomposition}
+
 \inputleannode{def:kalman-decomposition}
 
 \inputleannode{thm:kalman-subspaces-exist}