The full coupled observation-compatible coordinate theorem
Abstract
One coordinate realization of the original observation lift couples the symplectic split, the positive energy blocks, the canonical permutation, and both Williamson normal forms.
Theorem 1.1 (Original data and one shared coordinate realization).
Proof. Machine-checked in Lean as D5/S3/QuadraticForms/OriginalDataCoupledCoordinates.original_data_coupled_coordinates (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a natural number m, I_m is Fin m plus Fin m and C_m is the real functions on I_m. The block index I_k plus I_h represents C_k times C_h by Sum.elim. Write Jplus_m=[[0,I],[-I,0]]=-Matrix.J (Fin m) real. The first half of each Darboux basis is labelled q and the second p because its inl/inr pairing is positive delta. Matrix(e) always means the standard-coordinate matrix of the displayed linear equivalence e.
The only hypotheses are the original positive definite S, surjective O, closure O(Jplus_n S)=KO, and the original strict bounds 0<r<2n. Define P=OS-inverse O-transpose, L=S-inverse O-transpose P-inverse, U=range L, and V=ker O. No invertibility, complementarity, nondegeneracy, evenness, invariant lift, or coordinate basis is assumed.
The result is one inhabitant of CoupledCoordinates S O. All eight groups below refer to the same fields of that inhabitant. Choose one such inhabitant and keep it fixed throughout all the displays. The typed witnesses and all clauses below are read together for this one inhabitant, not as separate existential choices. P,L,Sv,Sh,Jb,Dv,Dh,W,Pi,e and iota are definitionally fixed abbreviations, not additional premises or independently chosen replacements.
Typed witnesses and fixed definitions
C1–C3: original images and actual coordinate equivalences
Apply original_data_symplectic_retract to the original S,O,K. Its restricted-radical argument tests x in ker O against (Jplus_n S)x; the vanishing pairing is negative strictly positive energy unless x=0. That argument remains on the live dependency path to the two returned Darboux bases. Include their vectors in the ambient space to obtain the columns of Tv and Th. The supplier Basis.equivFun gives their coordinate equivalences onto exactly U and V. Compose the visible equivalence with the bridge’s actual observation restriction to get B. The supplier Submodule.prodEquivOfIsCompl assembles T from these same two basis maps. The returned dimension equalities and the strict bounds imply k,h>0.
C4–C5: symplectic and energy congruences for the same T
Read the Darboux pairings as matrix entries. Alternation gives the reverse inr/inl pairing with a minus sign, producing Jplus in both diagonal blocks. The bridge identifies the exact symplectic orthogonal U-perp with V, giving the upper-right zero block; transposition and skew symmetry give the lower-left zero block. Its energy orthogonality gives the upper-right energy zero block; symmetry of S gives the lower-left block. Positive congruence with the injective Tv and Th proves positivity of exactly Sv=Tv-transpose S Tv and Sh=Th-transpose S Th. The original lift satisfies L-transpose S=P-inverse O and OL=I, hence L-transpose S L=P-inverse. Substitution of Tv=LB proves Sv=B-transpose P-inverse B.
C6–C7: canonical ordering and every covector
The mode concatenation e sends a visible index to the first k entries and a hidden index to the following h entries, followed by the equality n=k+h. The index map iota sends block order (qv,pv,qh,ph) to global order (qv,qh,pv,ph). Pi is the 0/1 matrix with entry one exactly when iota(i)=j. It acts on coordinate functions by composition with iota. Reindexing the identity matrix proves both inverse identities and identifies the inverse linear equivalence’s matrix with Pi-transpose. Reindexing Jplus gives Pi-transpose Jb Pi=Jplus_n. Transposing OT=[B,0] proves the covector identity for every a, and composition with Pi gives its permuted version.
C8: the two exact Williamson applications and one final R
Apply the existing positive_definite_williamson separately to exactly Sv and Sh. Retain the actual returned Wv,Wh and strictly positive frequency functions nuv,nuh. Their symplectic membership gives invertibility, so the block map W is a linear equivalence. Define Bhat=BWv, That=TW, and R=That Pi as actual compositions of equivalences. Surjectivity of Wv and Wh preserves range Tv and range Th. Multiplication preserves TvWv=L Bhat and the observation identity. Block multiplication gives the exact two diagonal energy blocks, and the fixed Pi gives the displayed global energy. The final covector formula uses the transpose of this same R, not a separately chosen global Williamson map.
The bridge retains arbitrary n,r and empty/full endpoints. The existing Darboux, complement, permutation and Williamson constructions support empty finite indices; only the present strict-bound consumer concludes k,h>0. Covectors transform by R-transpose when z=Rx. No displacement transformation, physical implementation, metaplectic operator, tensor product, Gibbs state, or thermal assertion is part of the result.