mollified
Mollified constructs the convolution of a real function G with a normalized ContDiffBump kernel φ on the line. Analysts working on continuous d'Alembert equations cite the construction to produce regularized approximants that support smoothness bootstraps. The definition is a direct left convolution of the normed bump with G under the lsmul map and Lebesgue measure.
claimLet $G : ℝ → ℝ$ and let $φ$ be a normalized $C^∞$ bump function with compact support. The mollified function is the left convolution $φ^{normed} ⋆ G$, taken with respect to Lebesgue measure on $ℝ$ via the scalar multiplication map.
background
The GeneralizedDAlembert module replaces the polynomial-degree-≤2 restriction on the route-independence combiner with mere continuity. It invokes the Aczél–Kannappan classification: a continuous $H : ℝ → ℝ$ satisfying $H(x+y) + H(x-y) = 2H(x)H(y)$ with $H(0)=1$ must be the constant 1, a hyperbolic cosine, or a trigonometric cosine. Mollification supplies the smoothing step that turns a continuous combiner into a smooth one while preserving the equation in the limit.
proof idea
The definition is a one-line wrapper that applies the convolution operator from Mathlib.Analysis.Convolution to the normed bump φ and the input G, using ContinuousLinearMap.lsmul and the volume measure.
why it matters in Recognition Science
Mollified supports mollified_continuous and mollified_pointwise_tendsto, which feed log_aczel_data_of_laws. That theorem extracts LogAczelData from any continuous SatisfiesLawsOfLogicContinuous instance, allowing the smoothness bootstrap to proceed from continuity alone. It relaxes the polynomial hypothesis of the Translation Theorem to continuity, aligning with the Aczél–Kannappan classification inside the Recognition framework.
scope and limits
- Does not assume G is continuous or bounded.
- Does not establish differentiability or pointwise convergence of the output.
- Does not invoke Recognition Science constants, J-cost, or the phi-ladder.
- Does not prove the Aczél–Kannappan classification.
formal statement (Lean)
212noncomputable def mollified (G : ℝ → ℝ) (φ : ContDiffBump (0 : ℝ)) : ℝ → ℝ :=
proof body
Definition body.
213 φ.normed (volume : MeasureTheory.Measure ℝ)
214 ⋆[ContinuousLinearMap.lsmul ℝ ℝ, (volume : MeasureTheory.Measure ℝ)] G
215
216/-- The normalized bump has compact support and is continuous; convolving
217with a continuous function leaves a continuous function. -/