Theorem: Exact initial-surface support in the flat realization

For $L_{\mathrm{fl}}={\mathsf{E}}_{\mathrm{fl}}C$,

Proof. The lower inclusion is Theorem thm:sphere. For every source $a=-f\mathrm{d}\varphi$, the transposed formula has support in $N_F$. Applying the local $C^{\ast }$ does not enlarge it. The surface term has support in $\{0\}\times S_F$. The scalar derivative is supported in $F$, away from $\Sigma$. The compact set $N_F\cup F$ contains every first derivative support and meets $\Sigma$ exactly in $\{0\}\times S_F$. Lemma lem:derivativesupport proves the upper inclusion.