Theorem: Null-sphere lower support under (TC)

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

Proof. First take $f(x)\ne 0$, and fix a sphere point $\mathbf{z}$. Near $x$, $r_{\mathbf{z}}(\mathbf{w})=|\mathbf{w}-\mathbf{z}|$ is smooth and positive. Choose a nonnegative compact cutoff $\chi$, positive at $x$, supported in that neighbourhood, and set

Its support is in the positive-time chart. The metric derivative of $B_f$ is $L^{\ast }a$, where

On $v=r_{\mathbf{z}}(\mathbf{w})$, ${\partial }_v{\varphi }_{\mathbb{C}}=\overline{f}\chi$. Thus (TC) gives

The integrand is positive on a nonempty open set. This respects the restricted source $a=-f\mathrm{d}\varphi$; its components have not been chosen independently.

Decompose ${\varphi }_{\mathbb{C}}$ into real and imaginary parts. At least one real configuration has nonzero trace. Lemma lem:surfaceinjective gives a nonzero surface coefficient; Lemma lem:nocancel prevents its cancellation by the bulk term. The derivative-support characterization places $(0,\mathbf{z})$ in ${\mathrm{supp}}_{\mathrm{fun}}{B}_f$.

For an arbitrary $x\in F$, choose $x_j=(t_j,{\mathbf{x}}_j)\to x$ with $f(x_j)\ne 0$. Writing $\mathbf{z}=\mathbf{x}+t\mathbf{n}$, use ${\mathbf{z}}_j={\mathbf{x}}_j+t_j\mathbf{n}$. Closedness of functional support proves the result.