Theorem: Admitted first-stage products

The prescriptions

define bilinear maps on $\mathcal{B}\times \mathcal{W}$ and $\mathcal{W}\times \mathcal{B}$, with values in

They satisfy classical normalization, locked first-stage normalization, and reversal.

Proof. Injective generating tests make the displayed bilinear assignments unambiguous on the actual argument spaces. Classical closure and the admitted mixed outputs place their coefficients in ${\mathcal{P}}_{\Sigma }$. Proposition prop:reverse proves reversal.