deriv_phi_eq
plain-language theorem explainer
The lemma states that the antiderivative Phi of any continuous real-valued H recovers H exactly under differentiation. Analysts working on regularity bootstrap for d'Alembert solutions cite this identity as the base step that lifts C^0 to C^1. The proof is a one-line wrapper that applies funext to the pointwise HasDerivAt result from phi_hasDerivAt.
Claim. Let $H:ℝ→ℝ$ be continuous and let $Φ(H)(t):=∫_0^t H(s)ds$. Then $d/dt Φ(H)(t)=H(t)$ for all real $t$.
background
The Aczél module proves every continuous solution of the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) with H(0)=1 is C^∞, yielding the classification into the constant, cosh, and cos cases. Phi is the antiderivative defined by Phi(H)(t)=∫_0^t H(s)ds. Upstream, H is the shifted cost H(x)=J(x)+1; under this substitution the Recognition Composition Law becomes the d'Alembert equation, as stated in the CostAlgebra.H doc-comment.
proof idea
The proof is a one-line wrapper: funext reduces the equality to a pointwise statement, then the .deriv projection is applied to the HasDerivAt result supplied by phi_hasDerivAt.
why it matters
This identity initiates the integration bootstrap that upgrades continuous H to C^1 and then inductively to all orders. It is invoked directly by phi_contDiff_succ in both the Proof and Theorem modules to obtain the inductive ContDiff step. The lemma completes the Aczél classification inside the Recognition framework, removing the last external hypothesis from the foundation chain and enabling the ODE derivation H''=cH that produces the explicit cosh and cos solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.