Proposition. Reindexing and splitting reference volume [fdip-002J]

For a bijection \(e:V\to W\), define \(U_e:X_V\to X_W\) by \((U_ex)(w)=x(e^{-1}w)\). It is a linear homeomorphism, with inverse \(U_{e^{-1}}\), preserving the counting pairing, and \[(U_e)_*\lambda _V=\lambda _W,\qquad f_*\mu (B):=\mu (f^{-1}B).\] For a disjoint decomposition \(V=R\sqcup D\), the restriction-pair map \(\sigma (x)=(x|_R,x|_D)\) has inverse pasting and satisfies \[\sigma _*\lambda _V=\lambda _R\otimes \lambda _D.\] Either factor may be empty, carrying singleton mass one.

These finite-coordinate proofs use the product convention of [tao2011measure, Section 1.7.4, pp. 194-199, preliminary version]. The corresponding sigma-finite APIs are MeasureTheory.measurePreserving_piCongrLeft and MeasureTheory.measurePreserving_piEquivPiSubtypeProd; the latter uses a decidable splitting predicate. A one-coordinate split is TauCeti.measurePreserving_piSplitAt, and the specified four-coordinate grouping is TauCeti.measurePreserving_finFourArrowPairPair.

Bare restriction \(\rho _R\) is measurable, but if \(D\ne \varnothing \) it is not reference-preserving: for a Borel \(A\subseteq X_R\) of finite positive mass, \(\rho _R^{-1}(A)\) has mass \(\lambda _R(A)\lambda _D(X_D)=\infty \). This includes \(R=\varnothing \), when the target singleton has mass one. The probability-factor assumption in TauCeti.measurePreserving_pi_comp_embedding excludes these unnormalized Lebesgue factors. Normalized marginals are a different measure statement.