Proposition: Faithful continuous bulk inclusion

The inclusion ${\mathcal{P}}_{\mathrm{mc}}\hookrightarrow {\mathcal{P}}_{\Sigma }$ is injective and continuous on each fixed-degree, fixed-support, fixed-wavefront normal-topology bulk stage. All its boundary coordinates vanish.

The topology induced on ${\mathcal{P}}_{\mathrm{mc}}$ is its strong coefficient subspace topology, not an asserted identification with the finer normal topology.

Proof. Injectivity follows from uniqueness of actual kernels. Lemma lem:bulk puts every relevant linear metric descendant in ${\mathcal{M}}_1$, where $\mathfrak{b}$ vanishes. Only the coefficient topology remains on the bulk. Normal stages contain those strong seminorms, giving the stated continuous inclusion.