Theorem: Whole-sum old gluing

The entire new-domain sum has zero old overlap:

Every prescribed new coefficient therefore glues uniquely with the unchanged old coefficient on this declared domain.

Proof. Every new tensor domain has at least one argument in $\mathcal{B}$. Thus

Use Lemma lem:anchored with $B=\mathcal{B}$, $P={\mathcal{P}}_{\mathrm{mc}}$ and Theorem thm:separation. Proposition prop:newdirect already handles all relations inside the new sum.