ode_regularity_differentiable_of_smooth
Any infinitely differentiable real-valued function H satisfies the regularity hypothesis that continuous solutions to the linear ODE f'' = f are differentiable. Researchers closing uniqueness arguments for the Recognition cost kernel via Aczél methods cite this result to discharge the differentiable leg of the bootstrap. The argument is a direct term that extracts first-order differentiability from the C^∞ assumption without using the ODE or continuity premises.
claimIf $H : ℝ → ℝ$ is $C^∞$, then $(∀ t, H''(t) = H(t)) → (H$ continuous$) → (H$ differentiable$)$.
background
The module isolates Aczél-dependent closure theorems for the cost functional equation, separate from the axiom-free core. The shifted cost H is defined by H(x) = J(x) + 1, where J satisfies the Recognition Composition Law and converts it to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Upstream, ode_regularity_differentiable_hypothesis asserts that pointwise satisfaction of f'' = f together with continuity implies differentiability; the companion ode_linear_regularity_bootstrap_hypothesis lifts this to C².
proof idea
Term-mode one-liner. The construction ignores the ODE equality and continuity assumptions, reduces ContDiff ℝ ⊤ to ContDiff ℝ 1 via of_le le_top, then invokes the differentiable method with a decide tactic confirming the order is nonzero.
why it matters in Recognition Science
It supplies the differentiable regularity bridge used by primitive_to_uniqueness_of_kernel, the public T5 statement that extracts J-uniqueness from PrimitiveCostHypotheses plus an AczelRegularityKernel. The result sits inside the cost-domain bootstrap that supports the J-uniqueness step (T5) of the forcing chain.
scope and limits
- Does not establish that H obeys the second-order ODE.
- Does not derive continuity of H.
- Does not apply when H is merely continuous or C¹.
- Does not yield derivative bounds or growth rates.
formal statement (Lean)
138theorem ode_regularity_differentiable_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
139 ode_regularity_differentiable_hypothesis H :=
proof body
Term-mode proof.
140 fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable
141 (by decide : (1 : WithTop ℕ∞) ≠ 0)
142
143/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/