phi_zero
plain-language theorem explainer
The lemma shows that the antiderivative operator Phi applied to any real-valued function H satisfies Phi H 0 = 0. Analysts proving smoothness of solutions to the d'Alembert equation cite this identity as the initial step in the integration bootstrap. The proof is a one-line simplification that invokes the definition of Phi together with the property that the integral over a degenerate interval vanishes.
Claim. Let $Phi(H)(t) := int_0^t H(s) ds$. Then $Phi(H)(0) = 0$.
background
In the module establishing Aczél's smoothness theorem, any continuous solution H of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is shown to be real analytic. The auxiliary operator Phi is defined by Phi(H)(t) := integral from 0 to t of H(s) ds; this appears in both the AczelProof and AczelTheorem files. The upstream H is the shifted cost function H(x) = J(x) + 1 from CostAlgebra, which converts the Recognition Composition Law into the standard d'Alembert identity.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of Phi and the Mathlib lemma intervalIntegral.integral_same establishing that the integral over [a,a] is zero.
why it matters
This lemma is called by exists_integral_ne_zero and representation_formula inside AczelProof and their counterparts in AczelTheorem; those results carry out the integration bootstrap that upgrades continuity to C^infty. It corresponds to the first step listed in the module documentation for the Aczél argument. In the Recognition Science setting it supplies the elementary integral identity needed before the ODE derivation that recovers the cosh form tied to the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.