Minimal Symmetric Realization Uniqueness

Abstract

Equal moments determine a minimal symmetric real realization up to an orthogonal intertwiner.

Theorem 1.1 (Orthogonal equivalence of minimal symmetric realizations).

$$\begin{array}{r}\forall U:\mathrm{Type}\left(\right),E:\mathrm{Type}\left(\right),W:\mathrm{Type}\left(\right),\\ [\mathrm{NormedAddCommGroup}\left(U\right),\mathrm{InnerProductSpace}\left(\mathbb{R},U\right),\mathrm{FiniteDimensional}\left(\mathbb{R},U\right)],\\ [\mathrm{NormedAddCommGroup}\left(E\right),\mathrm{InnerProductSpace}\left(\mathbb{R},E\right),\mathrm{FiniteDimensional}\left(\mathbb{R},E\right)],\\ [\mathrm{NormedAddCommGroup}\left(W\right),\mathrm{InnerProductSpace}\left(\mathbb{R},W\right),\mathrm{FiniteDimensional}\left(\mathbb{R},W\right)],\\ \forall A:\mathrm{LinearMap}\left(\mathbb{R},E,E\right),\tilde{A}:\mathrm{LinearMap}\left(\mathbb{R},W,W\right),\\ B:\mathrm{LinearMap}\left(\mathbb{R},U,E\right),\tilde{B}:\mathrm{LinearMap}\left(\mathbb{R},U,W\right),\\ (\mathrm{IsSymmetric}\left(A\right))⟹\\ (\mathrm{IsSymmetric}\left(\tilde{A}\right))⟹\\ (\forall k:\mathbb{N},\mathrm{comp}\left(\mathrm{adjoint}\left(B\right),\mathrm{comp}\left(A^k,B\right)\right)=\mathrm{comp}\left(\mathrm{adjoint}\left(\tilde{B}\right),\mathrm{comp}\left({\tilde{A}}^k,\tilde{B}\right)\right))⟹\\ (\mathrm{reachableSubspace}\left(A,B\right)=\mathrm{top}\left(\right))⟹\\ (\mathrm{reachableSubspace}\left(\tilde{A},\tilde{B}\right)=\mathrm{top}\left(\right))⟹\\ \exists Q:\mathrm{LinearIsometryEquiv}\left(\mathbb{R},E,W\right),\\ (\mathrm{comp}\left(\mathrm{toLinearMap}\left(Q\right),A\right)=\mathrm{comp}\left(\tilde{A},\mathrm{toLinearMap}\left(Q\right)\right))\wedge (\mathrm{comp}\left(\mathrm{toLinearMap}\left(Q\right),B\right)=\tilde{B})\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/MinimalSymmetricRealizationUniqueness.minimal_symmetric_realization_uniqueness (✓ std3). ∎

Citation. Jan C. Willems (1976). Realization of systems with internal passivity and symmetry constraints. DOI: 10.1016/0016-0032(76)90081-8.

Commentary.

The spaces U, E, and W are arbitrary finite-dimensional real inner-product spaces. W represents the second state space. LinearMap denotes a real linear map, adjoint is the inner-product adjoint, and comp is composition. In orthonormal coordinates the adjoint is the transpose in the source formula.

IsSymmetric is imposed on both dynamics: the inner product of A x with y equals that of x with A y, and likewise for the second dynamics. The two reachableSubspace hypotheses use the frozen repository definition displayed below, with all nonnegative powers and all input vectors. LinearIsometryEquiv is a surjective linear inner-product isometry; toLinearMap retains its underlying linear map.

$$\begin{array}{r}\forall U:\mathrm{Type}\left(\right),E:\mathrm{Type}\left(\right),\\ [\mathrm{NormedAddCommGroup}\left(U\right),\mathrm{InnerProductSpace}\left(\mathbb{R},U\right),\mathrm{FiniteDimensional}\left(\mathbb{R},U\right)],\\ [\mathrm{NormedAddCommGroup}\left(E\right),\mathrm{InnerProductSpace}\left(\mathbb{R},E\right),\mathrm{FiniteDimensional}\left(\mathbb{R},E\right)],\\ \forall A:\mathrm{LinearMap}\left(\mathbb{R},E,E\right),B:\mathrm{LinearMap}\left(\mathbb{R},U,E\right),\\ \mathrm{reachableSubspace}\left(A,B\right)=\mathrm{span}\left(\mathbb{R},\{x:E\mid \exists k:\mathbb{N},v:U,x=\left(A^k\right)\left(B\left(v\right)\right)\}\right)\end{array}$$

The proof sends each finite sum of iterated inputs to the same sum in the second realization. Symmetry and moment equality yield equality of the two Gram forms, hence equality of their kernels. The map descends through the quotient; minimality gives surjectivity on both sides. Increasing the generator power gives the dynamics identity, and power zero gives the input identity.

The literature attribution concerns minimal internally symmetric realizations and their invariant quadratic form. This formalization proves the real positive-metric case directly from moments.

References

• Truth anchor: D5/S3/Quantum/Measurements/MinimalSymmetricRealizationUniqueness.minimal_symmetric_realization_uniqueness
• Dependency: D5/S3/Observer/LinearMemory/ReachableObservableQuotientReachability