phi_differentiable
Continuous H admits the antiderivative Phi H that is differentiable on the reals. Analysts proving regularity for d'Alembert equations cite this during the first bootstrap step from continuity. The argument is a one-line wrapper that applies phi_hasDerivAt and extracts differentiableAt.
claimLet $H : ℝ → ℝ$ be continuous. Define $Φ(t) := ∫_0^t H(s) ds$. Then $Φ$ is differentiable on $ℝ$.
background
The module proves Aczél smoothness: any continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is real analytic. Phi is the antiderivative operator $Φ(t) := ∫_0^t H(s) ds$. Upstream, H is the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$ from CostAlgebra; under this change the Recognition Composition Law becomes the standard d'Alembert equation. The supporting lemma phi_hasDerivAt records that the derivative of Phi H at t equals H t.
proof idea
The proof is a one-line wrapper. For arbitrary t it calls phi_hasDerivAt H h_cont t to obtain HasDerivAt (Phi H) (H t) t, then projects to differentiableAt.
why it matters in Recognition Science
The lemma supplies the C^1 step in the integration bootstrap of Aczél's theorem. It is invoked by exists_integral_ne_zero and phi_contDiff_succ, which in turn feed the ODE derivation and analytic classification inside AczelTheorem. In the Recognition setting it underpins the passage from the J-uniqueness and RCL to the explicit cosh or cos forms that appear in the forcing chain.
scope and limits
- Does not assume H satisfies the d'Alembert equation.
- Does not prove continuity of the derivative of Phi.
- Does not establish higher-order differentiability.
formal statement (Lean)
41private lemma phi_differentiable (H : ℝ → ℝ) (h_cont : Continuous H) :
42 Differentiable ℝ (Phi H) :=
proof body
Term-mode proof.
43 fun t => (phi_hasDerivAt H h_cont t).differentiableAt
44