contDiff_top_of_contDiff_nat
A real-valued function on the line that meets the ContDiff condition at every finite order is automatically infinitely differentiable. The result is invoked inside the continuous-combiner construction to lift finite-order certificates to the top-level smoothness statement required downstream. The proof is a direct one-line application of Mathlib's contDiff_infty equivalence.
claimIf $f : ℝ → ℝ$ satisfies ContDiff $ℝ$ $n$ $f$ for every natural number $n$, then ContDiff $ℝ$ $⊤$ $f$, where $⊤$ is the top element of the extended naturals.
background
The module supplies a finite-to-top smoothness helper for the continuous-combiner route inside the generalized d'Alembert construction. Mathlib encodes $C^∞$ smoothness as ContDiff $𝕜$ $⊤$ $f$ and records via contDiff_infty that this is equivalent to the conjunction of all finite-order conditions. The file isolates the promotion step so the main module need not treat it as an axiom.
proof idea
The proof is a one-line wrapper that applies the second projection of contDiff_infty directly to the finite-order hypothesis.
why it matters in Recognition Science
The declaration supplies the promotion step required by residual input 1b in continuous_combiner_finite_smoothness_to_top. That parent theorem consumes the resulting top-level smoothness to finish the log-cost argument for the continuous combiner. It therefore closes the finite-to-infinite gap between mollifier certificates and the infinite differentiability needed by the generalized d'Alembert route.
scope and limits
- Does not supply derivative bounds or growth rates.
- Does not apply outside the real line.
- Does not imply analyticity or stronger regularity.
- Does not invoke Recognition Science constants or forcing steps.
Lean usage
theorem usage {f : ℝ → ℝ} (h : ∀ n : ℕ, ContDiff ℝ n f) : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) f := contDiff_top_of_contDiff_nat hformal statement (Lean)
18theorem contDiff_top_of_contDiff_nat
19 {f : ℝ → ℝ}
20 (hFinite : ∀ n : ℕ, ContDiff ℝ n f) :
21 ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) f := by
proof body
Term-mode proof.
22 exact (contDiff_infty).2 hFinite
23
24end SmoothnessTop
25end GeneralizedDAlembert
26end Foundation
27end IndisputableMonolith