phi_differentiable
plain-language theorem explainer
Continuous real functions H yield differentiable integrals Phi H. Recognition Science analysts cite this when bootstrapping regularity for the shifted cost function derived from the Recognition Composition Law. The argument is a one-line wrapper that extracts differentiability from the has-derivative property of the integral at each point.
Claim. Let $H : ℝ → ℝ$ be continuous. Then the function $Φ(H)$ given by $Φ(H)(t) = ∫_0^t H(s) ds$ is differentiable on $ℝ$.
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. Phi is the auxiliary antiderivative defined by Phi(H)(t) := ∫ from 0 to t of H(s) ds, used to initiate the integration bootstrap from continuity to C^∞. Upstream, H is the shifted cost H(x) = J(x) + 1, under which the Recognition Composition Law reduces to the d'Alembert equation; the companion lemma phi_hasDerivAt states that HasDerivAt (Phi H) (H t) t holds whenever H is continuous.
proof idea
The proof is a one-line wrapper that applies phi_hasDerivAt to obtain HasDerivAt (Phi H) (H t) t and then invokes differentiableAt to conclude Differentiable ℝ (Phi H).
why it matters
This lemma supplies the base differentiability step that feeds exists_integral_ne_zero and the inductive lift phi_contDiff_succ, completing the integration bootstrap in Aczél's theorem. It anchors the Recognition Science claim that the cost-derived H is smooth enough to support the phi-ladder, eight-tick octave, and D = 3 spatial structure. The module documentation references Aczél (1966) for the subsequent ODE classification that yields analyticity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.