phi_zero
plain-language theorem explainer
The lemma states that the integral operator Phi applied to any real function H vanishes at the lower limit zero. Analysts proving regularity for d'Alembert-type equations cite this base case during the integration bootstrap from continuity to smoothness. The proof is a one-line simp wrapper on the definition of Phi together with the degenerate-interval integral fact.
Claim. Let $Phi(H)(t) := int_0^t H(s) ds$. Then $Phi(H)(0) = 0$.
background
The module establishes Aczél's theorem: every continuous solution H of 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 antiderivative operator defined by integration from 0 to t. The reparametrization H(x)=J(x)+1 converts the Recognition Composition Law into d'Alembert form, as recorded in CostAlgebra.H.
proof idea
One-line wrapper that applies simp to the definition of Phi and intervalIntegral.integral_same.
why it matters
Supplies the zero base case required by the integral representation that bootstraps regularity. It is invoked directly by exists_integral_ne_zero and representation_formula in both AczelProof and AczelTheorem. The representation_formula doc-comment identifies the resulting identity as the key step that bootstraps regularity. It fills the first line of the integration-bootstrap outline given in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.