Theorem: Supported-sector reference distribution

For every vertex component $D$, the product

is defined on $U\setminus N_U$. In the fixed normal coordinates its exact normal form is

Smooth vertex weights, fiber contractions, and output $y$ derivatives may be applied to this distribution.

The reference agrees with the canonical grouped composition where that composition was already proved. It includes every normal derivative and both scalar-root terms.

Its support is contained in $S_{\mathrm{resp}}$, subject to the existing weights, and its wavefront set is bounded by

This is a local reference theorem for $K_{\mathrm{supp}}$, not for the full $K_{\mathrm{ret}}$.

Proof. At a point of $S_{\mathrm{resp}}\setminus N_U$, the proof of Lemma lem:traces bounds the cross-line wavefront by a conormal with nonzero $y$ component. The wavefront of $K_{\mathrm{supp}}$ is contained in $N^{\ast }{S}_{\mathrm{resp}}$, whose covectors have zero $y$ component. There is therefore no opposing pair at that point.

Off $S_{\mathrm{resp}}$ the internal supported distribution is locally zero, so the product is zero there. These local products glue on $U\setminus N_U$.

For smooth cross-line coefficients the exact formula is (eq:smoothjetproduct). For the present traceable distribution the same identity follows from the restriction and product calculus. Locally, one may regularize the single singular relative line in its admissible wavefront topology. Its normal traces converge by the restriction theorem; the products with the normal-jet distribution converge by the product theorem. The smooth identity therefore passes to the limit. This argument is entirely within the domain of Lemma lem:traces; no convergence at $N_U$ is claimed.

The normal traces have the tangential bounds in that lemma. Multiplication by $v_{\alpha }$ adds no wavefront, and Lemma lem:insertWF adds arbitrary response-normal covectors. This gives (eq:referenceWF). The finite vertex operations preserve the bound.

Every operation agrees with the canonical distributional operations on their common domain, proving agreement. The normal form was obtained from the complete response sector in Proposition prop:normalform, so no source or mass term has been removed.