MollifierCkRoute
plain-language theorem explainer
MollifierCkRoute asserts existence of a sequence of ContDiffBump kernels on the reals whose outer support radii tend to zero. It is cited in arguments that replace polynomial-degree restrictions with continuity when classifying solutions to the d'Alembert equation. The definition is a direct existential statement over families of smooth bump functions equipped with the required filter convergence on rOut.
Claim. There exists a sequence of smooth compactly supported bump functions $φ_n$ on $ℝ$ such that the outer radius of $φ_n$ tends to $0$ as $n→∞$.
background
The GeneralizedDAlembert module discharges the polynomial-degree-≤2 hypothesis in the Translation Theorem by invoking the Aczél–Kannappan classification: a continuous $H:ℝ→ℝ$ with $H(0)=1$ satisfying the d'Alembert equation is constant, a hyperbolic cosine, or a trigonometric cosine. MollifierCkRoute supplies the analytic infrastructure for mollification of continuous functions, naming a family of $C^∞$ bump kernels with shrinking support. This predicate is infrastructure only; the actual blocker for the continuous route-independence argument is uniform derivative bounds on the mollified approximants. Upstream structures include the J-cost convexity statement from PhiForcingDerived.of and the spectral emergence structure from SpectralEmergence.of that forces the gauge content and three generations.
proof idea
The declaration is a definition, not a theorem. It directly encodes the existential proposition over sequences of ContDiffBump functions together with the Tendsto condition on their outer radii. No lemmas are applied and no tactics are used; the body is the proposition itself.
why it matters
MollifierCkRoute is invoked by mollified_pointwise_tendsto and mollifierCkRoute_exists. It supplies the missing analytic predicate for the continuous-combiner version of SatisfiesLawsOfLogic, allowing the module to drop the polynomial restriction while still reaching the Aczél–Kannappan trichotomy. In the Recognition framework this step aligns with the move from T5 J-uniqueness to continuous route independence, ultimately feeding the forcing chain that yields D=3. It leaves open the uniform compact-set derivative bounds required for the full continuous pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.