phi_hasDerivAt
plain-language theorem explainer
The lemma establishes that the antiderivative Phi of any continuous real-valued H satisfies Phi'(t) = H(t) at every real t. Analysts working on regularity for d'Alembert functional equations cite it as the opening step of the integration bootstrap. The proof is a direct one-line application of the interval-integral differentiation theorem under continuity.
Claim. Let $H : ℝ → ℝ$ be continuous. Define $Φ(t) := ∫_0^t H(s) ds$. Then $Φ$ is differentiable at every $t ∈ ℝ$ with $Φ'(t) = H(t)$.
background
Phi is the antiderivative defined by integration of H from 0 to t. H is the shifted cost function H(x) = J(x) + 1, which converts the Recognition Composition Law into the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1. The module proves every continuous solution is C^∞ via bootstrap: continuous H implies Phi is C^1, which upgrades H to C^1, and so on. Upstream results include the CostAlgebra definition of H and the identical Phi construction in AczelProof.
proof idea
The proof is a one-line wrapper that applies intervalIntegral.integral_hasDerivAt_right. It passes the interval integrability of H on [0,t] (from continuity), strong measurability at the filter, and continuity at t.
why it matters
This lemma starts the regularity bootstrap that eliminates the former H_AczelClassification hypothesis, the last remaining foundation axiom. It is invoked directly by deriv_phi_eq, phi_differentiable, and representation_formula, which together yield the ODE H'' = c H and the classification into 1, cosh, and cos. The result anchors the smoothness claim in the Aczél theorem for the cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.