mollified_continuous
plain-language theorem explainer
Mollification of a continuous real function G by a normalized ContDiffBump kernel φ produces a continuous output. Researchers relaxing polynomial-degree hypotheses to continuity in the d'Alembert functional equation would cite this result. The proof is a term-mode wrapper that unfolds the convolution definition and applies the general continuity theorem for left convolution against a compactly supported continuous kernel.
Claim. Let $G : ℝ → ℝ$ be continuous and let $φ$ be a normalized $C^∞$ bump function centered at the origin with compact support. Then the mollification of $G$ by $φ$, given by the convolution $φ ⋆ G$, is continuous.
background
The module GeneralizedDAlembert discharges the polynomial-degree-≤-2 restriction on the route-independence combiner P by invoking the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation. A continuous $H : ℝ → ℝ$ with $H(0)=1$ satisfying $H(x+y)+H(x-y)=2H(x)H(y)$ must be the constant 1, a hyperbolic cosine, or a trigonometric cosine. The mollified definition is the left convolution of G against the normalized bump: $φ.normed ⋆ G$ using the lsmul map and Lebesgue measure. Upstream results supply the bump-function properties (compact support, ContDiff at level 0) and the local-integrability fact for continuous functions.
proof idea
The term proof unfolds mollified to expose the convolution, then applies HasCompactSupport.continuous_convolution_left. It supplies three arguments: the compact support of the normed bump, the fact that ContDiff at level 0 implies continuity of the normed kernel, and the local integrability of the continuous input G.
why it matters
The result supplies the continuity preservation step needed for the continuous-combiner version of SatisfiesLawsOfLogic, which in turn lets the Aczél–Kannappan trichotomy replace the stricter polynomial hypothesis in the Translation Theorem. It completes Move 3 of the module by showing that mere continuity of the combiner is sufficient for the classification into constant, cosh, or cos solutions. The declaration sits inside the Recognition Science pipeline that derives the d'Alembert equation from the Recognition Composition Law and then classifies its continuous solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.