H_continuous_of_positive_continuous
plain-language theorem explainer
The theorem shows that continuity of F on the positive reals implies continuity of the reparametrized cost map H F on the reals. Researchers establishing kernel uniqueness under Aczel regularity in the Recognition Science cost framework cite it to close the continuity seam before smoothness. The term proof composes the input continuity with the exponential map then adds the constant function one.
Claim. If $F : ℝ → ℝ$ is continuous on $(0, ∞)$, then the map $t ↦ F(e^t) + 1$ is continuous on $ℝ$.
background
The Aczel Classification module packages the regularity bridge for d'Alembert solutions in the cost framework. Continuous solutions become smooth once the calibrated ODE kernel is reached, allowing downstream exclusivity code to avoid the raw Aczel axiom directly.
proof idea
The term proof composes ContinuousOn.comp_continuous on the given hCont with Real.continuous_exp to obtain continuity of t ↦ F(exp t). It then adds the constant function 1 via continuous addition and simplifies using the definitions of H and G.
why it matters
This lemma supplies the continuity of H F required by primitive_to_uniqueness_of_kernel, which concludes F equals the J-cost under PrimitiveCostHypotheses and AczelRegularityKernel. It advances the d'Alembert forcing chain by securing the reparametrized kernel continuity needed for the T5 J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.