deriv_phi_eq
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume or use the d'Alembert equation.
- Does not establish continuity or differentiability of H.
- Does not address discontinuous functions.
- Does not compute the constant c in the resulting ODE.
formal statement (Lean)
109private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
proof body
Term-mode proof.
110 funext fun t => (phi_hasDerivAt H h_cont t).deriv
111