Theorem: Coefficientwise classical covariance

The formal original-rod construction is gauge invariant through second order:

for the admitted formal diffeomorphisms. Consequently, every ${\mathcal{O}}_f$ is invariant to that order.

Proof. The scalar $T=F(\varphi )$ transforms by composition with $\rho$. The diffeomorphism maps its clock slices to the corresponding old slices. Pullback preserves the induced metric and the slice-harmonic scalar equation.

The pullback of an old rod is therefore a solution of the new rod equation with the same asymptotic labels. The uniqueness argument of Proposition prop:rods, applied coefficientwise, identifies it with the new rod through second order. Thus

The raw lapse is a scalar formed by contraction of a covector with the inverse metric, so $N^{\prime }=N\circ \rho$. The inverse coordinate map is ${\alpha }^{\prime }={\rho }^{-1}\circ \alpha$. Hence $N^{\prime }\circ {\alpha }^{\prime }=N\circ \alpha$. The fixed label-space smearing preserves the equality.