Theorem: Whole-sum old-product compatibility

The full new-domain sum has zero old overlap:

Thus

For each fixed real $c$, all prescribed coefficients glue uniquely with the unchanged old coefficients on $D_{\mathrm{decl}}$.

Proof. Every new domain has a factor in $\mathcal{B}$ in at least one argument. Hence

Theorem thm:separation gives $\mathcal{B}\cap {\mathcal{P}}_{\mathrm{mc}}=0$. Apply Lemma lem:anchored with $A={\mathcal{P}}_{\Sigma }$, $B=\mathcal{B}$, and $P={\mathcal{P}}_{\mathrm{mc}}$. This proves vanishing of the old overlap of the entire new sum, including any potential sum-domain relation.

Proposition prop:newdirect already constructs each coefficient on $D_{\mathrm{new}}$. Combining it with ${C_j}^H$ on the disjoint old domain gives a unique map on $D_{\mathrm{decl}}$.