Theorem. Relabeling transports the state and its marginal [fdip-000H]

Let \(M,M'\) be finite-dimensional real positive inner-product spaces with their induced Borel Euclidean volumes \(\lambda ,\lambda '\). Let \(Q:M\to M\) be positive and self-adjoint, and let \(P:M\to M'\) be a linear isometry equivalence. Put \(Q'=PQP^{-1}\). Then \(Q'\) is positive and self-adjoint, and the Gaussian laws satisfy \[Z_{Q'}=Z_Q,\qquad P_*\mu _Q=\mu _{Q'}.\] Borel pushforward means \((P_*\mu )(A)=\mu (P^{-1}(A))\) for every Borel set \(A\), extending the finite convention. For every real or complex Borel function \(F'\), \[\begin {aligned} \int |F'|\,d\mu _{Q'}&=\int |F'\circ P|\,d\mu _Q,\\ F'\in L^1(\mu _{Q'})&\Longleftrightarrow F'\circ P\in L^1(\mu _Q). \end {aligned}\] The first identity allows infinity. Under the equivalent finite absolute-integral conditions, \[\omega _{Q'}(F')=\omega _Q(F'\circ P).\] In particular, the target observable transported from \(F\) is \(F'=F\circ P^{-1}\). Exact and signed arrows of real backgrounds supply such isometries.

Now let \(M=X\oplus Y\) and \(M'=X'\oplus Y'\) be orthogonal splittings that \(P\) carries by isometries \(P_X,P_Y\), so the split-square hypotheses hold. For the 4 components, \[\begin {aligned} A'&=P_XAP_X^{-1},&B'&=P_XBP_Y^{-1},\\ E'&=P_YEP_X^{-1},&C'&=P_YCP_Y^{-1}. \end {aligned}\] Here \(E=B^\dagger \), and \(C>0\). The retained precisions and eliminated Gaussian factors satisfy \[\begin {aligned} S'&=P_XSP_X^{-1},& S&=A-BC^{-1}E>0,\\ c_{C'}&=c_C,&c_C&=\frac {(2\pi )^{\dim Y/2}}{\sqrt {\det C}},\\ Z_{S'}&=Z_S,&(P_X)_*\mu _S&=\mu _{S'}. \end {aligned}\] Thus the complete fiber scalar and the additive effective-action constant \(-\log c_C\) are preserved, along with the normalized law.

For vertex bijections \(p:V\to V'\), take a nonempty proper \(R\subsetneq V\), set \(R'=pR\), and use the coordinate splits. The map \(P_R:\mathbb R^R\to \mathbb R^{R'}\) has the genuine moving target \(\mathbb R^{pR}\). At \(p(v)\), \(v\in R\), both \(\pi _{R'}Pf\) and \(P_R\pi _Rf\) have value \(f(v)\). Thus:

The lower map exists because the retained subset is transported. Keeping the target labels fixed can select an inequivalent marginal; the adjacent-versus-opposite example gives both the precision calculation and a failure of projection factorization.

These conclusions use positive precisions and the stated product volumes. Fixing an eliminated field, taking a conditional-density kernel, and taking a marginal are different operations. A singular full-fiber integral is not repaired by a pseudoinverse: changing the integration space changes the measure. The massless projected cycle law has its proved density on the specified retained image, and is not obtained by inserting a mean-zero constraint into the unconstrained marginal formula.

[friedli2017statistical, Proposition B.55, p. 505] gives the Gaussian change-of-variables convention.

[tao2011measure, Theorem 1.7.15, pp. 200-202] gives the nonnegative integration convention on the Borel product measures; absolute integrability precedes signed subtraction.

[boyd2004convex, Appendix A.5.5, pp. 650-651] gives the real block convention, with its first pivot exchanged to \(C\).

Mathlib's LinearIsometryEquiv.measurePreserving supplies volume preservation for finite-dimensional real linear isometry equivalences. TauCeti's TauCeti.Probability.map_affine_multivariateGaussian supplies covariance-parameter transport. Set mean and shift to zero, linear map to \(P\), and covariance to \(Q^{-1}\); the precision-density identification and the proved inverse identity align it with this law. These interfaces do not supply the endpoint data, declared partition or its counterexample.