Lemma: Closed target cone

The cone in (eq:contractioncone) is closed and lies in $G_N$. It bounds the unsymmetrized output wavefront set. The permuted target cone is also closed and microcausal.

Proof. The wavefront bound is the product–pushforward bound with convention (eq:orientation); dropping the null-geodesic restriction only enlarges it. The causal exclusion is the argument of Theorem thm:product.

For closedness, take convergent nonzero output covectors and witnesses $(y_j,{y^{\prime }}_j,q_j)$. The base variables stay compact. If $q_j$ were unbounded, divide the first input tuple by $|q_j|$. A subsequence would limit to a nonzero tuple $(0,q_{\infty })$ wholly in $V_{-\sigma }$ and in the closed cone ${\Gamma }_1$, a contradiction. Thus the witnesses have a convergent subsequence. The closed input cones then give a witness for the limit. Finite permutation unions preserve the assertions.