ode_regularity_bootstrap_of_smooth
Any infinitely differentiable real-valued function H satisfies the regularity bootstrap hypothesis for the linear ODE f'' = f. Recognition Science proofs of T5 J-uniqueness cite this result to close the smoothness gap inside the Aczél kernel path. The proof is a one-line wrapper that invokes the ContDiff ordering lemma to obtain C² from C^∞.
claimIf $H : ℝ → ℝ$ is infinitely differentiable, then the following holds: whenever $H''(t) = H(t)$ pointwise for all $t$, $H$ is continuous, and $H$ is differentiable, it follows that $H$ is twice continuously differentiable.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. H is the shifted cost reparametrization H(t) = G(t) + 1, where G satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) after the change of variables from CostAlgebra. The upstream result dAlembert_cosh_solution states that a continuous solution with H(0) = 1 and H''(0) = 1 equals cosh. The hypothesis ode_linear_regularity_bootstrap_hypothesis encodes the standard fact that pointwise solutions of the linear ODE f'' = f are automatically C² once continuity and differentiability are granted.
proof idea
This is a one-line wrapper. It applies the ContDiff ordering lemma (h.of_le le_top) directly to the infinite-differentiability assumption, yielding the required ContDiff ℝ 2 conclusion inside the hypothesis.
why it matters in Recognition Science
The declaration closes the regularity seam required by the Aczél classification. It is invoked by primitive_to_uniqueness_of_kernel, the public T5 theorem that converts PrimitiveCostHypotheses and an AczelRegularityKernel into the equality F x = Jcost x. The step supports the passage from d'Alembert solutions to the cosh form that yields J-uniqueness (T5) in the forcing chain.
scope and limits
- Does not establish that any given H satisfies the ODE equation itself.
- Does not treat functions with regularity below C^∞.
- Does not incorporate boundary conditions such as H(0) = 1.
- Does not derive the d'Alembert equation from the Recognition Composition Law.
Lean usage
have h_reg : ode_linear_regularity_bootstrap_hypothesis H := ode_regularity_bootstrap_of_smooth h_smoothformal statement (Lean)
1045theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1046 ode_linear_regularity_bootstrap_hypothesis H :=
proof body
Term-mode proof.
1047 fun _ _ _ => h.of_le le_top
1048
1049/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
1050 solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
1051
1052 This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/