Worked geometry of the phase level sets of a future null wave covector

Clause (a). By [L1], $k^{\mathrm{♯}}=\varpi (e_0+{\sum }_i{s}_i{e}_i)$ with $\varpi >0$ and $\mathrm{\mid }s\mathrm{\mid }=1$, so $\eta (k^{\mathrm{♯}},k^{\mathrm{♯}})={\varpi }^2(-1+{\sum }_i{s}_i^2)={\varpi }^2(\mathrm{\mid }s{\mathrm{\mid }}^2-1)=0$ by [L1, L3], and $k(k^{\mathrm{♯}})=\eta (k^{\mathrm{♯}},k^{\mathrm{♯}})$ by [L1]. For every $p\in A$ and $\lambda \in \mathbb{R}$ the defining identity of the phase gives $\theta (p+\lambda k^{\mathrm{♯}})=\theta (p)+\lambda k(k^{\mathrm{♯}})=\theta (p)$, so $\theta$ is constant on the lines $p+\mathbb{R}{k}^{\mathrm{♯}}$.

Clause (b), kernel and sign. By [L2] and $\varpi >0$, $v\in \ker k$ is equivalent to $v^0=s\cdot v_{\mathrm{v}\mathrm{e}\mathrm{c}}$, and $\ker k$ is a $3$-dimensional subspace [L2]. For $v\in \ker k$, substituting $v^0=s\cdot v_{\mathrm{v}\mathrm{e}\mathrm{c}}$ into [L3] gives $\eta (v,v)=-(s\cdot v_{\mathrm{v}\mathrm{e}\mathrm{c}}{)}^2+\mathrm{\mid }{v}_{\mathrm{v}\mathrm{e}\mathrm{c}}{\mathrm{\mid }}^2$; by [L4] with $\mathrm{\mid }s\mathrm{\mid }=1$ this is $\ge 0$, and it is $0$ exactly when $\mathrm{\mid }s\cdot v_{\mathrm{v}\mathrm{e}\mathrm{c}}\mathrm{\mid }=\mathrm{\mid }{v}_{\mathrm{v}\mathrm{e}\mathrm{c}}\mathrm{\mid }$, which by the equality clause of [L4] holds exactly when $v_{\mathrm{v}\mathrm{e}\mathrm{c}}=\lambda s$ for some real $\lambda$. For such a $v$, $v^0=s\cdot v_{\mathrm{v}\mathrm{e}\mathrm{c}}=\lambda$, so $v=\lambda (e_0+{\sum }_i{s}_i{e}_i)=\lambda {\varpi }^{-1}{k}^{\mathrm{♯}}$ lies in $\mathrm{span}(k^{\mathrm{♯}})$; conversely every multiple of $k^{\mathrm{♯}}$ lies in $\ker k$ because $k(k^{\mathrm{♯}})=0$ by step 1.1. For every $w\in \ker k$ one has $\eta (k^{\mathrm{♯}},w)=k(w)=0$, so this line lies in the radical; conversely a radical vector has zero self-pairing and thus lies in this line by the equality calculation. Hence $\eta {\mathrm{\mid }}_{\ker k}$ is positive semidefinite, its radical is $\mathrm{span}(k^{\mathrm{♯}})$, and its only null elements are the nonzero multiples of $k^{\mathrm{♯}}$.

Clause (b), null directions. By [L1] and [L6] the vector $k^{\mathrm{♯}}$ is future null and $-k^{\mathrm{♯}}$ is past null, so the nonzero multiples of $k^{\mathrm{♯}}$ are exactly the two rays ${\mathbb{R}}_{>0}{k}^{\mathrm{♯}}$ (future null) and ${\mathbb{R}}_{>0}(-k^{\mathrm{♯}})$ (past null) of the line $\mathrm{span}(k^{\mathrm{♯}})$; combined with step 2.1 and [L5], the line through $k^{\mathrm{♯}}$ is the only null direction contained in $\ker k$.

Clause (c). By [L2] and step 2.1 the kernel of the nonzero functional $k$ is the $3$-dimensional subspace $\ker k$, and the level set $\mathrm{\Sigma }=\{p:\theta (p)=\theta (p_0)\}$ is the affine hyperplane $p_0+\ker k$ through $p_0$; its direction subspace is $\ker k$, whose normal covector is $k$ (the linear functional defining the direction subspace), and $k$ is null by hypothesis. Since $k^{\mathrm{♯}}\in \ker k$ by step 1.1, both rays $p_0+{\mathbb{R}}_{\ge 0}{k}^{\mathrm{♯}}$ and $p_0+{\mathbb{R}}_{\le 0}{k}^{\mathrm{♯}}$ lie in $\mathrm{\Sigma }$; every other direction vector of $\mathrm{\Sigma }$ lies in $\ker k$ outside $\mathrm{span}(k^{\mathrm{♯}})$ and is spacelike by steps 2.1 and 3.1 and [L5]. This proves (a), (b) and (c). The computation is exact algebra and no choice principle was used.