Theorem: Finite-width insertion admission

For fixed $\epsilon >0$:

1. ${{\mathcal{O}}_{f,ϵ}}^{\mathrm{D},(1)}$ has a compact mixed kernel with wavefront in $Z_2$;

2. ${{\mathcal{O}}_{f,ϵ}}^{\mathrm{D},(2)}[h,0,\varphi ]$ has a compact kernel with wavefront in $Z_3$;

3. the $k$-linear contribution is ${{\mathcal{O}}_{f,ϵ}}^{\mathrm{D},(1)}[k,\varphi ]$;

4. these polynomials and all their fixed smooth directional derivatives belong to ${\mathcal{P}}_{\mathrm{mc},\mathrm{pol}}$.

The coefficient maps are continuous on fixed-support test stages with their corresponding normal-topology kernel stages.

Proof. At order one, integration by parts gives a derivative of

with constant fibre tensors. It is a two-slot balanced kernel.

At order two, the inverse-coordinate formula contains:

1. two first-order coordinate lines ending at the observation vertex and a scalar derivative there;

2. a coordinate line from the observation to a local quadratic metric vertex, with two metric slots joined to that vertex by delta lines;

3. a nested coordinate line, a local metric slot, and a further first-order coordinate line.

Every term is a finite sum of differentiated balanced trees. The $k$-term follows by linearity of $a_1$.

The observation vertex lies in $\mathrm{supp}f$. Every retarded ancestor lies in its causal past, and each coordinate-source vertex has a factor ${\sigma }_{\epsilon }$ or a derivative of ${\sigma }_{\epsilon }$; it is therefore at nonnegative time. Delta-attached field slots coincide with such vertices. All relevant supports lie in a fixed compact causal region. Lemma lem:tree applies.

A nonzero tuple wholly in the future or past causal cone cannot have zero sum. Thus $Z_n$ implies the microcausal exclusion. Smearing a slot against a smooth configuration inserts zero covector in that slot, so the remaining tuple still has zero sum.

For continuity, there are finitely many smooth multiplications, compatible fixed-kernel products, differentiations, and support-proper projections. Their normal-topology continuity and hypocontinuity properties apply on the just-checked stages BDH. No global completeness or global hypocontinuity claim is required.