This is the complete Section 18.6 of the programme reading Detecting regularity without choosing coordinates. It proves that the normal restrictions are the actual strong smooth distribution family and reconstruct the joint distribution. Its original section and formula labels are retained.
The preceding Sections 18.1–18.5 supply every wavefront, Fourier, Gaussian and pullback identity cited below, with their full prerequisite readings. In particular WF1 is distributional Fourier inversion, WF2 is compact wavefront localization, WF11–WF13 construct the normal pullback and identify its Gaussian limit. The Schwartz and Fourier foundation, F1–F5, supplies the test decay and inversion; the metric foundation, Sections 12–13, supplies finite localization and Taylor remainders; and the integration foundation, Sections 15–16, supplies the absolute integrals and dominated limits.
18.6. Absence of parameter-normal covectors gives the actual smooth family
Let be a distribution on an open product in the original variables , with no wavefront covector , . Every slice embedding satisfies WF11, because its transpose sends to . Thus the already constructed restriction exists.
Fix compact spatial test support and a small compact parameter neighborhood. The compact base set and the compact unit sphere in the original -coordinates have a finite regular cone/base cover. Use its finite spatial partition and common smaller parameter neighborhood. After each compact localization , WF2 gives a constant such that decreases to every order when ; on the whole space it has the original polynomial bound . Summing the finitely many localized formulas retains all their cutoff derivatives.
For a spatial test , the actual pairing on the neighborhood where the parameter cutoff is one is
In , the rapid decrease of dominates every original factor and both integration dimensions, while . In the complementary region, . The polynomial bound for , multiplied by the Schwartz bound
is integrable after both integrations when . The integral in WF17 is bounded by finitely many original test derivative seminorms on the fixed support, with every binomial and derivative from retained in that full operator. These bounds are uniform on bounded sets of tests. For each derivative order, take a corresponding ; no one fixed finite test order for all parameter derivatives is inferred.
Dominated differentiation therefore gives every derivative in WF16. Taylor's remainder for , bounded by a constant times , and the same bounds with two additional frequency powers prove convergence of difference quotients uniformly on every bounded set of spatial tests. Continuity uses the same dominated bounds. This is precisely smoothness into the strong distribution topology, whose seminorms are suprema of pairings over bounded test sets. It is stronger than only the smoothness of each single pairing.
To verify that WF16 is the original pullback, apply WF13 to , then restrict the smooth Gaussian approximations. Their transforms acquire the full factor , bounded by one. The just proved absolute envelopes allow its limit and every fixed parameter derivative in WF16, agreeing with WF12 for the slice map. Finally testing against any original compact smooth and applying these absolute bounds permits integration in , and recovers the original distribution pairing by WF1. Thus the family reconstructs , rather than an unrelated family with the same notation. Finite localization and restriction compatibility paste these actual families on the whole parameter domain. For there is no parameter derivative; for the no-normal condition is absence of all nonzero covectors and Section18.1 proves the required scalar smoothness.