The complete first-stage commutator calculation

No compactness of $\varphi$ is required: compactness belongs to the functional kernel, while configurations are smooth. If the configuration space is constrained, the realization assumption in this lemma must instead be proved within that space.