Theorem: Conditional native insertion and regular-probe products

Fix an actual representative $W$ satisfying (eq:W), a declared subtraction germ, and Assumptions ass:internal and ass:external. Then, on $\mathcal{X}$ with central smooth second jets,

is a cutoff-independent native Wick symbol. Its products on either side with compact regular probe polynomials exist through the retained contraction order.

For a linear probe, the external contraction is explicitly

Every rod in this formula is the original spatial Newton inverse.

Proof. The classical limit of $F_{f,R}$ is $F_f$ in the seminorm topology of Theorem thm:classicaldomain. Lemma lem:internal supplies the scalar normalization limit.

For (eq:external), differentiate (eq:Fclass) in the free first jet. The symmetric polarization gives the displayed formula. Local entries of $w_g$ are smooth and only sampled on $\mathrm{supp}f$. The term $\text{calRz}$ is defined by Lemma lem:Newton. Assumption (eq:externalIR) gives the same lemma for ${\text{calRw}}_g$. Therefore each term in $b(z,w_g)$ is a smooth integrable compact-output expression.

A compact regular polynomial has smooth compact derivative kernels. After fixing the remaining compact field variables, its first derivative is a finite or continuously compact-tested superposition of probes of the above type. The uniform bounds in Assumption ass:external justify that integration. The reverse ordered product uses the transposed contraction. Its causal difference, compact tested in one slot, has uniformly compact spatial support on compact time intervals, so its rod composition satisfies the compact-source version of Lemma lem:Newton.

Thus both product orders exist. Cutoff independence follows from the same bounds. No infrared bound on a two-rod state covariance has been used.