Theorem: Preflight obstruction on the frozen algebra

The coordinate prescription (eq:regcoord)–(eq:coorddata) fails first-order gauge covariance on ${\mathfrak{g}}_U$. For the free scalar

the first-order relational variation smeared with the frozen $f$ is $c_{\epsilon }>0$.

Proof. The scalar variation is $X_{{\xi }_{\ast }}{\varphi }_0=\psi$. The coordinate variation is $S_{\epsilon }{\xi }_{\ast }$, whose action on ${\varphi }_0$ is $S_{\epsilon }\psi$. Their difference has smearing (eq:ceps), which is positive by Lemma lem:positivegap. The complete relational expansion proving the insertion sign appears in Section sec:observable.