Theorem. Relabeling transports the state and its marginal [fdip-000H]
AGENTDRAFTED
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.