mollifierCkRoute_exists
plain-language theorem explainer
Existence of a sequence of bump functions on the real line with outer radii shrinking to zero is established by explicit construction. Workers on continuous solutions to the d'Alembert equation in the Recognition Science framework cite this to support mollification steps that drop the polynomial-degree restriction. The proof exhibits radii 1/(2(n+1)) and 1/(n+1), verifies the inequality by linarith, and invokes a standard tendsto lemma for the limit at infinity.
Claim. There exists a sequence of $C^k$ bump functions $φ_n$ on $ℝ$ such that the outer radius of $φ_n$ tends to zero as $n→∞$.
background
The GeneralizedDAlembert module discharges the polynomial restriction on the route-independence combiner by moving to a continuous version of SatisfiesLawsOfLogic. The Aczél–Kannappan classification states that a continuous $H:ℝ→ℝ$ with $H(0)=1$ satisfying the d'Alembert equation is constant 1, a hyperbolic cosine, or a trigonometric cosine. MollifierCkRoute supplies the shrinking-support bump family required for mollification arguments in this setting.
proof idea
The tactic proof opens with classical, then refines to a pair. The first component is a function sending each $n$ to a ContDiffBump whose radii are $rIn=1/(2(n+1))$ and $rOut=1/(n+1)$; positivity and the strict inequality are discharged by linarith after casting $n$ to reals. The second component is the tendsto statement for the outer radii, obtained directly from tendsto_one_div_add_atTop_nhds_zero_nat.
why it matters
This supplies the concrete bump family needed to justify mollification once the combiner is assumed merely continuous rather than polynomial of degree ≤2. It supports the transition to SatisfiesLawsOfLogicContinuous inside the module and aligns with the Aczél–Kannappan step that removes the polynomial hypothesis. The declaration remains infrastructure; uniform derivative bounds on the mollified objects are left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.