H_continuous_of_positive_continuous
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not establish differentiability or smoothness of H F.
- Does not extend to F defined on non-positive reals.
- Does not invoke the functional equation or specific constants such as G or phi.
- Does not prove uniqueness of the kernel by itself.
formal statement (Lean)
65private theorem H_continuous_of_positive_continuous (F : ℝ → ℝ)
66 (hCont : ContinuousOn F (Set.Ioi 0)) : Continuous (H F) := by
proof body
Term-mode proof.
67 have h := ContinuousOn.comp_continuous hCont Real.continuous_exp
68 have h' : Continuous (fun t => F (Real.exp t)) :=
69 h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
70 have h_add : Continuous (fun t : ℝ => F (Real.exp t) + (1 : ℝ)) :=
71 h'.add (continuous_const : Continuous fun _ : ℝ => (1 : ℝ))
72 simpa [H, G] using h_add
73