exists_integral_ne_zero
plain-language theorem explainer
Continuous real functions H with H(0)=1 admit a positive δ such that the integral of H from 0 to δ is nonzero. Analysts classifying continuous solutions to d'Alembert's functional equation cite this to initiate the regularity bootstrap. The argument locates a neighborhood of positivity around zero via continuity and derives a contradiction to the mean-value theorem applied to the antiderivative if the integral vanishes at that scale.
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$. Then there exists $δ > 0$ such that $∫_0^δ H(s) ds ≠ 0$.
background
This lemma sits inside the Aczél smoothness module for continuous solutions of the d'Alembert equation. Phi is the antiderivative defined by Phi(H, t) := ∫ from 0 to t of H(s) ds. The module proves every continuous H satisfying H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is C^∞, via an integration bootstrap that first produces a representation formula for H in terms of Phi and then lifts regularity inductively. The upstream H from CostAlgebra is the shifted cost H(x) = J(x) + 1, under which the Recognition Composition Law becomes the standard d'Alembert equation.
proof idea
The proof first records H(0)=1>0 and uses continuity to obtain an eventual positivity neighborhood. It picks δ = ε/2 inside that neighborhood. Assuming Phi(H, δ)=0, it applies exists_hasDerivAt_eq_slope to Phi and H, together with phi_differentiable and phi_hasDerivAt, to produce a point c at which H(c) equals the zero slope. This contradicts positivity inside the ε-ball, yielding the required nonzero integral.
why it matters
The lemma supplies the nonzero δ required by the representation formula H(t) = (Phi(t+δ) − Phi(t−δ)) / (2 Phi(δ)). It is invoked directly inside dAlembert_contDiff_nat (both in AczelProof and AczelTheorem) to begin the induction that lifts continuity to C^n for every n. In the Recognition framework it removes the last remaining hypothesis H_AczelClassification, completing the classification of continuous solutions as cosh, cos, or constant and aligning with the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.