Lemma: Finite participating Gaussian density

The baseline restriction to ${\mathcal{F}}_{\mathrm{s}}(\mathfrak{k})$ has a normal centered gauge-invariant Gaussian density ${\rho }_{\mathfrak{k}}$. It need not factor between the selected packet space and its orthogonal complement in $\mathfrak{k}$.

Proof. In an orthonormal basis $e_i$, its occupation matrix is

It is positive and finite. Diagonalize $A$ by a passive finite-mode unitary. Each diagonal covariance is represented by the geometric density of that mean. Their product, rotated back, has the required Gaussian characteristic function and trace one. Uniqueness of finite-mode Weyl characteristic functions identifies the restricted state. Off-diagonal covariance is retained.