exists_integral_ne_zero
plain-language theorem explainer
For continuous H with H(0)=1 the antiderivative Phi H is nonzero at some δ>0. Analysts studying functional equations cite it to start the bootstrap from continuity to C^∞ in the d'Alembert setting. The proof uses eventual positivity of H near zero together with the mean value theorem on Phi to reach a contradiction if Phi vanishes at a small positive point.
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$. Define $Φ(t) := ∫_0^t H(s) ds$. Then there exists $δ > 0$ such that $Φ(δ) ≠ 0$.
background
The module establishes Aczél's smoothness theorem: any continuous solution H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is real analytic. Phi is the antiderivative Phi H t := ∫_0^t H(s) ds. This lemma initiates the integration bootstrap that upgrades continuity to higher differentiability before the ODE step and classification into cosh, cos, or constant solutions.
proof idea
The argument first records H(0)=1>0, then invokes continuity to obtain a neighborhood where H>0. It selects δ=ε/2 inside that neighborhood and assumes Phi H δ=0 for contradiction. Application of exists_hasDerivAt_eq_slope to Phi H on [0,δ], using phi_differentiable and phi_hasDerivAt, produces c ∈ (0,δ) with H(c)=0. This contradicts the positivity neighborhood, since phi_zero supplies the boundary values needed for the slope to be zero.
why it matters
The lemma supplies the nonzero integral required by representation_formula inside dAlembert_contDiff_nat, which proves continuous d'Alembert solutions are C^n for every n. It therefore completes the first step of the integration bootstrap in the module documentation for Aczél's theorem. Within Recognition Science it supports analyticity of the shifted cost H = J + 1 that converts the Recognition Composition Law into d'Alembert form, underpinning the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.