[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 (2nd ed.), Theorems 13.2(2) and 16.2(2) for the controllable and observable component conclusions; Theorems 11.5, 12.1 and 15.7 for the reachable-subspace, controllability-matrix and observability-matrix statements, with Theorem 15.9 for the PBH observability result. These exact references are in the source, roadmap and blueprint. The restriction/quotient constructions and invariant-subspace/rank-nullity formulations are identified as algebraic or derived versions; this PR does not claim the full textbook similarity-decomposition theorem.

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.

Synchronization follow-up (2026-10-23): merged current upstream main at 1436289 to resolve the Hautus conflict. Foundational unobservable-subspace facts remain in Observability.lean, retaining upstream's shorter Cayley–Hamilton proof and blueprint titles. Umbrella imports were regenerated. The exact-citation commit 6251f41 is retained.

Local validation: 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. All eight new public theorem proofs use only propext, Classical.choice, and Quot.sound; the PR introduces no sorry, admit, custom axiom, or unsafe.

OpenAI Codex assisted with this follow-up, validation and review response. No human code review is claimed.

Latest upstream Lean Action CI run 39889142906 is action_required and awaits maintainer workflow approval. The checks listed above were executed locally; no upstream CI pass is claimed.

[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.

[dongxuelian2]

The exact references are in 6251f41: Hespanha, Linear Systems Theory (2nd ed.), Theorems 13.2(2) and 16.2(2) for the two component conclusions, with Theorems 11.5, 12.1, 15.7 and 15.9 attached to the related reachability, matrix and PBH results. The source, roadmap and blueprint distinguish the restriction/quotient constructions and derived invariant-subspace/rank-nullity facts from the full textbook similarity decompositions.

I also synchronized current main in 0ae493c to clear the upstream conflict, retaining the lower-level proof organization, the shorter upstream Cayley–Hamilton argument and its blueprint titles. The local full build, declaration linter, all 16 linters on the six affected control modules, regenerated-import check, blueprint extraction, PDF/web builds, label integrity and declaration-link checks pass. The eight audited public theorem proofs use only propext, Classical.choice and Quot.sound. OpenAI Codex assisted with this follow-up; no human review is claimed.

The new upstream Lean Action CI run is awaiting maintainer workflow approval (action_required); no upstream CI pass is claimed.