Logical boundary of the result

The proof separates four assertions that should not be identified:

1. The sharp-Cauchy insertion is a well-defined smooth polynomial functional on smooth classical fields.

2. Its fixed kernels are compactly supported distributions.

3. Those kernels belong to a prescribed quantum insertion domain.

4. Retarded products with those kernels exist in a common normalization prescription.

The first two assertions hold for ${{\mathcal{B}}_f}^{(1)}$. The third fails in the domain of Definition def:poly. The fourth is therefore not reached by the stated termwise construction.

Theorem thm:onshell establishes that the analogous failure for a linear coordinate observable can be bypassed after restricting to the free equations of motion. It does not supply the nonlinear extension of that bypass. In particular, replacing a distributional metric smearing by an on-shell equivalent smooth smearing inside an interacting composite requires an additional proof controlling field dependence, support, and equation-of-motion contact terms.

The resulting manuscript is a closed boundary-domain result. It leaves the existence of a suitably repaired second-order relational insertion open.