deriv_phi_eq
plain-language theorem explainer
The lemma shows that the antiderivative of a continuous real-valued function H recovers H upon differentiation. Researchers proving regularity for solutions of the d'Alembert equation cite this step when bootstrapping from continuity to higher smoothness. The argument is a direct one-line reduction to the fundamental theorem of calculus via the pointwise hasDerivAt property of the integral.
Claim. Let $H : ℝ → ℝ$ be continuous. Define the antiderivative operator by $Φ(H)(t) := ∫_0^t H(s) ds$. Then the derivative of $Φ(H)$ equals $H$.
background
The module establishes Aczél's smoothness theorem: any continuous solution H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is real analytic. The antiderivative Phi is defined as the integral of H from 0 to t. This construction appears in the cost algebra where the shifted cost H(x) = J(x) + 1 satisfies the d'Alembert equation under the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the hasDerivAt lemma for the integral at each point t and extracts the derivative via funext.
why it matters
This lemma supplies the differentiation step that feeds the successor lemma phi_contDiff_succ, which lifts ContDiff regularity. It forms part of the integration bootstrap in Aczél's theorem and supports smoothness of the cost function H in Recognition Science, which is required for the phi-ladder, the eight-tick octave, and derivation of constants such as ħ = phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.