phi_zero
plain-language theorem explainer
The lemma states that the antiderivative Phi of any real function H vanishes at the origin. Researchers deriving regularity for d'Alembert solutions from the Recognition Composition Law cite this identity as the base case for the integration bootstrap. The proof is a one-line simp wrapper that reduces the claim to the definition of the interval integral and the degenerate-interval rule.
Claim. Let $Phi(H)(t) := int_0^t H(s) ds$. Then $Phi(H)(0) = 0$.
background
In the AczelTheorem module the auxiliary function Phi is the indefinite integral of a solution H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1. This equation is obtained by substituting the shifted cost H(x) = J(x) + 1 into the Recognition Composition Law, converting the multiplicative form into the additive d'Alembert identity. The same Phi appears in the sibling AczelProof module and is the central object in the representation formula that bootstraps continuity to C^infty regularity.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of Phi together with the Mathlib lemma intervalIntegral.integral_same.
why it matters
The lemma supplies the zero base case required by exists_integral_ne_zero and representation_formula, which together close the integration bootstrap that eliminates the former H_AczelClassification hypothesis. It therefore completes the fully proved Aczel classification inside the Recognition framework, confirming that every continuous solution of the J-cost equation is C^infty and hence yields the cosh or cos forms that appear in the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.