Theorem: Global Friedrichs wavefront relation

For the massless Friedrichs spectral covariance (eq:W) on the regular host (eq:host),

The equality holds on all of $M\times M$, including the diagonal, crossings of geometric fronts, and every geometric–diffractive angular transition.

Every first endpoint covector is future null, every second endpoint covector is past null, and neither endpoint covector is zero.

Proof. Proposition prop:upper gives the global upper bound. Proposition prop:geolower gives the geometric lower bound. Outside $\mathcal{Q}$, Proposition prop:criterion gives the entire diffracted lower bound. Inside $\mathcal{Q}$, Proposition prop:quotient removes every strictly diffractive covector outside ${\mathcal{G}}^{+}$. The orientation and nonzero-endpoint statements were established in Proposition prop:upper and the definitions of the two relations.