Theorem: Stagewise product hypocontinuity

Each symmetrized contraction is hypocontinuous from the two named input stages to ${\mathcal{E}}_{K_{\mathrm{out}},{\Gamma }_{\mathrm{out}}}^{\prime }$. For $N=0$ its target is $\mathbb{C}$. The zero-contraction term is included using the usual tensor cone and its permutations.

Proof. Tensoring the two varying inputs is hypocontinuous. Multiplication by the fixed line kernel is continuous linear on the compatible tensor stage. Proper pushforward and finite permutation pullbacks are continuous linear. Their composition is hypocontinuous. Compatibility was checked in Theorem thm:product, and the uniform target cone is Lemma lem:targetcone. Complete contraction is the same proper pushforward to a point.