The original observation lift and its symplectic complement
Abstract
A positive Hamiltonian with a closed surjective observation map determines complementary symplectic subspaces through the original energy lift.
Theorem 1.1 (The positive lift, its inverse, and the two restricted forms).
Proof. Machine-checked in Lean as D5/S3/QuadraticForms/OriginalDataSymplecticSplit.original_data_symplectic_retract (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let E be the real functions on Fin n plus Fin n and F the real functions on Fin r. The canonical matrix J is [[0,I],[-I,0]], the negative of Mathlib’s Matrix.J. Let S be positive definite, O map E onto F, and O(JS)=KO. Set P=OS-inverse O-transpose, L=S-inverse O-transpose P-inverse, U=range L, V=ker O, and w(x,y)=x-transpose J y. In the displayed formula these definitions are bound by equalities; they are not additional independent assumptions.
Surjectivity of O makes its transpose injective. Positive congruence therefore makes P positive definite and OL=I. Restricting O to U gives a linear equivalence whose inverse is exactly L. Every vector z decomposes as LOz plus z-LOz. The two summands lie in U and V respectively, and their intersection is zero. The identity L-transpose S=P-inverse O gives energy orthogonality.
The kernel V is invariant under A=JS by the observation closure. If x in V lies in the radical of the restricted symplectic form, test it against Ax, which is again in V. The resulting equality w(x,Ax)=-x-transpose S x contradicts positive energy unless x=0. Thus the restriction to V is nondegenerate. Since A is injective, its restriction to finite-dimensional V is surjective. Expressing v in V as Az shows that w(u,v)=-u-transpose S z vanishes for u in U. Complement dimensions identify U with the symplectic orthogonal of V; taking the orthogonal again gives exactly V as the orthogonal of U. The existing restriction criterion then gives nondegeneracy on U.
Both alternating forms and both positive energy forms restrict to these same subspaces. The existing finite-dimensional Darboux theorem supplies bases b and c on U and V. Their cardinalities give r=2k and n=k+h. No nonempty index or positive dimension is required: r=0, r=2n, and the zero ambient space remain included.
Surjectivity of A and O makes K surjective, hence invertible. The identity KP=OJO-transpose then proves invertibility of the reduced skew matrix. The symplectic orthogonal characterization and energy orthogonality make U invariant under A; applying the inverse observation on U gives AL=LK for the original lift.
These bases belong to the original range L and kernel O. Constructing their ambient coordinate maps, the global position-momentum permutation, and a common final map for the two Williamson congruences requires further coordinate identities. The present statement asserts the retract and the two bases; it does not assert that complete coordinate normal form.