Theorem: Null-sphere lower support under (TC)

Assume (TC) and the copied adjoint identity. For every $x=(t,\mathbf{x})\in F$ with $t>0$,

Moreover,

Proof. First suppose $f(x)\ne 0$, and fix $\mathbf{z}$ with $|\mathbf{x}-\mathbf{z}|=t$. Choose a nonnegative compact smooth cutoff $\chi$, positive at $x$, supported in a small interior neighbourhood of $x$ on which

is smooth and nonzero. Define

This is a smooth compact configuration, and its support is away from $\Sigma$. Consequently $a=-f\mathrm{d}\varphi$ is an allowed source for (eq:TC).

On the cone $v=r_{\mathbf{z}}(\mathbf{w})$,

Its temporal trace component is therefore

The integral is finite, and its integrand is positive on a nonempty open spatial set. This construction respects the restriction $a=-f\mathrm{d}\varphi$; it does not treat its components as independently selectable sources.

If configurations are required to be real, write $\varphi ={\varphi }_1+i{\varphi }_2$. Since the trace map is complex-linear and the displayed result is nonzero, at least one real configuration ${\varphi }_j$ gives nonzero trace.

Injectivity of $\mathsf{B}$, followed by Lemma lem:no-cancel, shows that $(0,\mathbf{z})$ lies in the support of the actual metric derivative. The derivative-support characterization places it in ${\mathrm{supp}}_{\mathrm{fun}}{B}_f$.

For an arbitrary $x\in F$ with $t>0$, take $x_j=(t_j,{\mathbf{x}}_j)\to x$ with $f(x_j)\ne 0$. For a given sphere point write $\mathbf{z}=\mathbf{x}+t\mathbf{n}$, $|\mathbf{n}|=1$, and set ${\mathbf{z}}_j={\mathbf{x}}_j+t_j\mathbf{n}$. The preceding argument applies to each ${\mathbf{z}}_j$. Closedness of functional support proves (eq:sphere-lower).

Finally, any point of $F\cap \Sigma$ is a limit of interior points where $f\ne 0$, unless $f$ is identically zero near it, in which case it is not in $F$. The same construction with $t_j\to 0$ gives sphere points converging to that boundary point. This proves (eq:boundary-F-lower).