Proposition: Exact first-order plateau invariance

For every datum in Specification spec:data and every $\xi \in {\mathfrak{g}}_U$,

This is invariance under the declared additive first-order gauge action, not unrestricted diffeomorphism invariance.

Proof. Since all derivatives of $\xi$ are supported where $\chi =1$, $\chi K\xi =K\xi$. Lemma lem:gaugeidentities gives

The last equality holds because $X_{\xi }{\varphi }_0$ is compactly supported and vanishes near ${\Sigma }_0$.

Likewise, (eq:CK), the vanishing initial data of $\xi$, and uniqueness of (eq:w) imply

The two terms in (eq:observable) therefore cancel exactly.