phi_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume continuity or any other regularity on H.
- Does not prove existence of a positive delta where Phi H delta is nonzero.
- Does not invoke the d'Alembert equation or the condition H(0)=1.
- Does not address differentiability or analyticity of H.
formal statement (Lean)
33private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by
proof body
One-line wrapper that applies simp.
34 simp [Phi, intervalIntegral.integral_same]
35