Prove controllable and observable component properties

[dongxuelian2]

The state and input maps restricted to the reachable subspace give a controllable pair. The state and output maps induced on the quotient by the unobservable subspace give an observable pair. The four matrix definitions take an explicit state basis indexed by Fin r, and the component theorems hold for every supplied basis.

Reference: Hespanha, Linear Systems Theory, reachable subspace, controllability-matrix test, controllable decomposition, unobservable subspace, observability tests, and observable decomposition. The observable quotient is a quotient-space construction corresponding to the observable component. This PR establishes its observability without introducing a complement, similarity, transfer-function, or realization theorem. The invariant-subspace characterizations and rank-nullity identity are identified as derived statements; the coordinate definitions use Mathlib's LinearMap.toMatrix.

Review cleanup:

• Removed the coercion/power helpers and basis wrappers; kept invariant/coordinate proof helpers private.
• Made bases explicit in all four matrices and both component theorems. The restriction remains field-generic; the quotient uses upstream's complex unobservable-subspace API.
• Moved membership, the observability criterion, and invariance of the unobservable subspace into Observability.lean, together with the private Cayley–Hamilton helper. Observable component definitions now depend on this lower module rather than Hautus.
• Gave every new or materially changed public declaration a blueprint node and readable content entry; removed obsolete documentation markers and normalized references.
• Updated the roadmap and regenerated umbrella imports. Integrated current upstream cleanup without rewriting earlier review commits.

Validation: focused and full lake build, lake exe runLinter, all 16 linters on the six component/foundation modules, lake exe mk_all --check, lake build :blueprint, leanblueprint pdf, leanblueprint web, leanblueprint checkdecls, python3 scripts/check_blueprint_labels.py, and git diff --check pass. The affected PDF pages were visually inspected. All eight new public theorem proofs use only propext, Classical.choice, and Quot.sound; the PR introduces no sorry, admit, custom axiom, or unsafe.

[AnandGokhale]

Thanks for splitting it up, let me understand whats going on in these files and give you a review in a few hours

[AnandGokhale]

Please align the terminology used in your PR with standard controls terminology, actually referencing a book. As it stands, a lot of the generated results may be correct, but need to be carefully stated. Moreover, you are missing blueprints on a lot of your documentation.

[dongxuelian2]

Addressed in 543798d. I checked the terminology and statements against Hespanha's Linear Systems Theory and documented the restriction as the controllable component and the quotient as an equivalent realization of the observable component. The invariant-subspace characterizations and rank-nullity result are marked as derived; chosen-coordinate definitions are identified as Lean infrastructure. The principal statements and blueprints now describe the chosen basis actually used.

I removed five public plumbing/basis declarations, made six proof helpers private, generalized the controllable component to any field, and moved the ambient unobservability lemmas into the existing observability module. Added blueprints cover the four system maps and the smallest-invariant-subspace characterization; all eleven mathematical nodes added by this PR are included in the readable blueprint.

The focused and full builds, linters, import check, blueprint extraction, PDF/web rendering, and declaration check pass. The eight new public theorem proofs use only the standard Lean axioms. The PDF has one unresolved comparison-lemma reference, independently reproduced on upstream main fbaa7d7. The PR description now reflects the component scope and these checks.

[AnandGokhale]

Please cite exact theorem numbers, and not a whole book.