Theorem: Admitted first-stage products

The formulas

define bilinear maps on $\mathcal{B}\times \mathcal{W}$ and $\mathcal{W}\times \mathcal{B}$, respectively, with values in ${{\mathcal{V}}_{\Sigma }}^{[3]}$. They satisfy classical normalization, the locked first-stage normalization, and reversal under complex conjugation.

Proof. Lemma lem:injective identifies each element of $\mathcal{B}$ and $\mathcal{W}$ with its unique test. The formulas are bilinear in those tests and therefore are well defined on the named actual-functional spaces.

Classical closure places $B_f{W}_g$ and $W_g{B}_{f^{\prime }}$ in ${\mathcal{P}}_{\Sigma }$. The selected contractions are admitted by the inherited result and Proposition prop:reverse. Thus both formal outputs belong to ${{\mathcal{V}}_{\Sigma }}^{[3]}$. Their order-zero term is the pointwise product. Equation (eq:Qadjoint) proves reversal. No additional binary contraction is possible for these pairs: each sharp insertion has only one metric slot and no middle scalar slot with which its scalar slot could contract.