phi_zero
plain-language theorem explainer
The lemma shows that the integral from 0 to 0 of any real function H equals zero. Analysts working on regularity for d'Alembert functional equations cite it as the base case in the integration bootstrap. The proof is a one-line simp reduction on the integral definition and the degenerate-interval property.
Claim. For any function $H : ℝ → ℝ$, the integral from 0 to 0 of $H(s)$ ds equals 0.
background
The module carries out the integration bootstrap for Aczél's smoothness theorem on continuous solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. Phi is the antiderivative operator defined by the definite integral from 0 to t of H. The shifted cost H arises in CostAlgebra as J(x) + 1, converting the Recognition Composition Law into d'Alembert form with H(0) = 1.
proof idea
One-line wrapper that applies simp to unfold the integral definition of Phi and invoke the fact that the integral over a point interval vanishes.
why it matters
The result is called by exists_integral_ne_zero and representation_formula, which feed the main smoothness theorem in both AczelProof and AczelTheorem. It supplies the zero base case required for the antiderivative representation that lifts continuity to C^∞. In the Recognition Science setting it anchors the translation of the RCL into the d'Alembert equation used for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.