Develop Kalman decomposition and finite-dimensional realization theory

[dongxuelian2]

Summary

This PR develops a textbook-aligned finite-dimensional structural and realization theory for LTI systems. It starts from canonical reachable and unobservable subspaces, completes the semantic Kalman decomposition, and builds through minimal realization theory, uniqueness up to similarity, finite Markov determinacy, Hankel rank theory, and a constructive finite Ho–Kalman synthesis.

The development is algebraic and time-agnostic. It uses feedthrough plus Markov parameters rather than Laplace transforms or analytic transfer-function infrastructure.

The main references are João P. Hespanha, Linear Systems Theory; Kailath, Linear Systems; R. E. Kalman's classical realization/decomposition theory; and Ho–Kalman realization theory where appropriate. References are descriptive and do not depend on edition-specific theorem numbers.

The dependency spine is:

controllability / observability
        ↓
Kalman decomposition
        ↓
canonical controllable-observable core
        ↓
realization + Markov behavior
        ↓
minimal realization theorem
        ↓
uniqueness up to similarity
        ↓
finite Markov determinacy
        ↓
finite Hankel rank theory
        ↓
finite Ho–Kalman synthesis

Kalman structural semantics

The K1 layer now includes:

• reachable-subspace finrank equal to controllability-matrix rank;

• the unobservable subspace as the kernel of the observability matrix, together with observability rank-nullity;

• four-sector dimension identities and dimension canonicality across noncanonical complements;

• standalone controllable and observable decompositions;

• the canonical controllable-observable core

  $$ \mathcal R/(\mathcal R\cap\mathcal N); $$

• proofs that the core is controllable and observable; and

• exists_kalmanDecomposition_with_semantics.

The arbitrary co complement in a chosen Kalman decomposition is not incorrectly asserted to be A-invariant. The semantic controllable-observable object is instead represented canonically by the quotient R / (R ∩ N).

Algebraic realization semantics

The realization layer introduces Realization 𝕜 n m p with state, input, output, and feedthrough matrices A, B, C, and D. It reuses the existing controllability and observability predicates and defines Markov parameters

$$ CA^kB; $$

behavioral equivalence across differing state dimensions, explicit realization similarity, and similarity invariance of Markov behavior.

D is included in behavioral equivalence through the feedthrough term, but it does not affect structural controllability or observability.

Hankel theory

The finite Hankel layer provides:

• arbitrary finite-horizon controllability matrices;
• arbitrary finite-horizon observability matrices;
• finite block-Hankel matrices;
• the factorization H = O C;
• rank bounded by state dimension;
• full Hankel rank for controllable-observable realizations; and
• rank stabilization for horizons r, s ≥ n.

These results provide the rank infrastructure for minimal realization theory.

Minimal realization theorem

The main characterization is:

$$ \boxed{\text{minimal}\iff\text{controllable and observable}} $$

over the implemented scalar setting (currently ℂ). The layer also proves that the canonical core preserves behavior, every realization admits a behaviorally equivalent minimal realization, minimal state dimension equals the stabilized Hankel rank, and behaviorally equivalent minimal realizations have equal state dimensions.

Uniqueness up to similarity

The uniqueness milestone is:

$$ \boxed{\text{behaviorally equivalent minimal realizations}\Rightarrow\text{similar}} $$

and, in the appropriate fixed-dimension minimal formulation:

$$ \boxed{\text{behavioral equivalence}\iff\text{similarity}} $$

The similarity map is constructed from controllable representatives; observability establishes its well-definedness.

Finite Markov determinacy

For state dimensions n₁ and n₂, equality of the feedthrough matrices together with equality of Markov parameters in the explicit window

$$ k < n_1+n_2 $$

suffices to prove full behavioral equivalence. The bound is formally proved using finite-dimensional algebra and Cayley–Hamilton recurrence machinery; it is not stated merely as “finitely many parameters”.

Finite Ho–Kalman synthesis

The completed construction provides:

• a block-Hankel state space;

• quotient/range descent;

• the induced shift/state map;

• canonical input and output maps;

• a coordinate realization;

• state dimension equal to Hankel rank;

• block recovery

  $$
  C_H A_H^k B_H=M_k;
  $$

• full behavioral equivalence for sufficiently large finite windows;

• controllability;

• observability;

• minimality; and

• uniqueness across valid stabilized horizons and basis choices up to similarity.

The exact behavioral-equivalence bound currently proved is

$$ n+\operatorname{rank}H_0\le s $$

where n is the source realization's state dimension, H₀ is the unshifted finite Hankel block in the shifted compatible pair, and s is the supplied horizon in the theorem's (r, s) construction.

Abstract compatible finite data can also be synthesized under explicit kernel/range compatibility hypotheses. The minimal-source corollary discharges those compatibility conditions automatically at the stated sufficient horizons.

Remaining scope

This PR does not contain:

• Laplace-transform theory;
• analytic transfer functions;
• BIBO theory;
• Gramians;
• stabilizability/detectability; or
• observer/controller synthesis.

Two small deferred Ho–Kalman API improvements remain:

• a strict finite Fin N storage/container for finite Markov data; and
• a user-facing theorem deriving the compatibility hypotheses directly from classical rank-stability equalities.

These are API/convenience follow-ups, not blockers to the completed mathematical theory.

Examples

Regression coverage includes controllable/observable one-state systems, degenerate zero-dimensional systems, multiple Kalman sectors, pure feedthrough, redundant/nonminimal states, explicit two-state minimal realizations related by a nonidentity shear, finite Markov-window calculations, the uniqueness theorem, a nonminimal counterexample, Ho–Kalman recovery of a minimal two-state system, reduction of a redundant realization to a smaller Hankel-rank realization, and different stabilized horizons yielding similar realizations.

Documentation

The roadmap is recorded in:

• LinearSystems/KalmanDecomposition/plan.md;
• LinearSystems/Realization/plan.md; and
• the global LinearSystems/plan.md.

These roadmaps now reflect the theorem dependency structure rather than only file layout.

Validation

Focused validation passed for the structural Kalman targets (Decomposition, Dimensions, Semantic, and regression examples), Realization.HoKalman, and Realization.Examples. Focused lint passed for KalmanDecomposition.Semantic and Realization.HoKalman. lake exe mk_all --check passed after confirming the tracked aggregate file was unchanged. The existing touched Kalman blueprint declarations are covered by the compiled milestone modules; no new blueprint facet was added in this stack.

Also passed:

• git diff --check;
• proof-placeholder audit: no sorry or proof-level admit in the structural/realization development; and
• milestone axiom audits, which report only the standard established footprint: propext, Classical.choice, and Quot.sound.

Repository-wide lake build, aggregate blueprint build, and aggregate leanblueprint checkdecls remain blocked by pre-existing failures in LeanForControl/ODEs/ComparisonLemma.lean around lines 57 and 89. The same failure exists on the baseline upstream commit b93941684cf5d4a1dcfb17bf7b67fa1fe73aeceb, and this PR does not modify that file. The local environment also does not provide the leanblueprint executable, so that aggregate check is not claimed green.

Suggested review order

1. Kalman decomposition dimensions and the semantic core;
2. Realization/Defs and Markov behavior;
3. Hankel factorization;
4. the minimality theorem;
5. similarity uniqueness;
6. finite determination;
7. Ho–Kalman synthesis; and
8. examples and roadmaps.

[AnandGokhale]

This is quite a large commit, do you think there is a logical way to break this down into several smaller PRs?
I would also recommend citing a book or a paper for each result that you have in your PR

[dongxuelian2]

I addressed both review points by rebuilding this work as six sequential, independently building review units from current main (and preserving the original branch):

1. Prove controllable and observable component properties #20 codex/kalman-reachable-observable — reachable restriction and observable quotient; open against main now.
2. codex/kalman-four-sector — Kalman sector dimensions and canonical controllable-observable core; based on 1.
3. codex/realization-minimality — realization behavior, Hankel foundations, and minimality; based on 2.
4. codex/realization-similarity-determination — similarity, finite Markov determination, and Hankel rank stabilization; based on 3.
5. codex/ho-kalman-finite-core — finite compatible Hankel range/shift realization; based on 4.
6. codex/ho-kalman-recovery — sufficient-window recovery, minimal synthesis, uniqueness, and regression examples; based on 5.

All six branch tips passed lake build; the final tip also passed lake exe runLinter and lake build :blueprint. The relevant result families now have local book/paper pointers, and the final branch includes a verified source map in LeanForControl/LinearSystems/references.md. Exact horizon bounds are identified as Lean consequences where they are not verbatim statements of the cited source.

Only #20 is open against main so the later PRs do not duplicate prior diffs. The five follow-up branches are pushed to the fork and can be proposed in order as their bases become available upstream. I am closing this large PR as superseded; its discussion and original head branch remain available.