Formalize the finite-dimensional Kalman decomposition

[dongxuelian2]

Summary

This PR formalizes the classical finite-dimensional Kalman decomposition on top of the existing controllability, observability, and Hautus development.

Main additions

• A dedicated LeanForControl/LinearSystems/Reachability/ subject-area directory with a living plan.md.
• A finite-horizon reachable subspace, with its definition separated into DefsReachability.lean and its characterizations and invariance results in Reachability.lean.
• The relationship between the reachable subspace and controllability, including the Cayley–Hamilton proof of state-matrix invariance.
• A KalmanDecomposition data structure in Reachability/DefsKalmanDecomposition.lean, separated from its theorem implementation.
• An adapted direct-sum linear equivalence and bases for the four coordinate sectors cuo, co, uuo, uo.
• Transported A/B/C maps and an explicit entrywise block-zero theorem for their adapted matrices.
• Standalone regression examples, including zero-dimensional state spaces, and blueprint integration for the precise reachability-membership equivalence.

Provenance

The mathematical results are classical finite-dimensional linear-systems results. References used in the source are:

• João P. Hespanha, Linear Systems Theory.
• 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.
• Kailath, Linear Systems.

The Lean-specific relative direct-sum construction, coordinate equivalence, basis transport, finite-horizon proof plumbing, and entrywise matrix packaging are marked as original formalization infrastructure for LeanForControl.

Interpretation and limitations

The four named sectors are coordinate sectors adapted to the reachable and unobservable subspaces, in the order cuo, co, uuo, uo. The chosen complements are noncanonical vector-space complements, and they are not individually claimed to be A-invariant. The theorem asserts the forced block-zero pattern; no vanishing claim is made for the starred blocks.

Reachability remains tied to the existing finite-horizon controllability matrix rather than being defined as an invariant closure. The formalization follows the existing complex-matrix convention, treats LTI triples (A, B, C), does not include a feedthrough matrix D, and does not claim a numerical decomposition algorithm.

Validation

• lake exe cache get — passed
• lake build — passed
• lake exe runLinter — passed
• Standalone build of LeanForControl.LinearSystems.Reachability.KalmanDecompositionExamples — passed
• lake build :blueprint — passed
• leanblueprint checkdecls — passed
• Trust audit of reachable-subspace invariance, Kalman-decomposition existence, and the final block-zero theorem — only propext, Classical.choice, and Quot.sound
• No executable sorry/admit and no new custom axioms
• git diff --check — passed

[AnandGokhale]

Can you please add a reference to a paper which has these results. I believe Joao Hespanha's Linear systems theory book should have what you are looking for!

Thank you!
Anand

[AnandGokhale]

Another quick comment, I dont think having different files for so many results is a scalable approach. Can you create a directory called Reachability within which your results live?

[AnandGokhale]

Please add a docstring

[dongxuelian2]

Added a precise docstring for this declaration.

[AnandGokhale]

This statement is vague, lots of undefined terms. Also please use blueprints for docstrings

[dongxuelian2]

Rewritten as an explicit mathematical equivalence and added a blueprint annotation; the indexed input vector and controllability matrix are now stated explicitly.

[AnandGokhale]

Please use better names for lemmas

[dongxuelian2]

Renamed the Cayley–Hamilton boundary helper to a semantic name and updated its uses.

[dongxuelian2]

Thanks for the review. I reorganized the new development under LinearSystems/Reachability/ and added a living plan.md. I also added Hespanha's Linear Systems Theory and Kalman's 1963 paper as references, while retaining Kailath as an additional textbook source. The reachability membership statement now has an explicit blueprint formulation, and the boundary helper names have been cleaned up. All local Lean, linter, blueprint, checkdecls, and axiom checks pass.