exists_integral_ne_zero
Any continuous real-valued H with H(0)=1 has its antiderivative Phi H nonzero at some positive argument. Analysts proving smoothness for d'Alembert solutions cite this as the initial bootstrap step from continuity. The argument extracts local positivity of H near zero from continuity, then applies the mean-value theorem to Phi H to reach a contradiction if the integral vanishes at the chosen scale.
claimLet $H : {R} {to} {R}$ be continuous with $H(0)=1$. Then there exists $delta > 0$ such that $int_0^delta H(s) ds neq 0$.
background
The module establishes Aczél's smoothness theorem: every continuous solution H of 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 operator defined by Phi H t := integral from 0 to t of H(s) ds. The shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into the standard d'Alembert form. Upstream lemmas establish that Phi H is differentiable with derivative H and that Phi H vanishes at zero.
proof idea
Continuity and H(0)=1 yield an open interval around zero on which H remains positive. The proof selects delta equal to half the radius of that interval. It assumes for contradiction that Phi H delta equals zero, invokes exists_hasDerivAt_eq_slope on Phi H and H to locate a point c in (0,delta) where the derivative of Phi H equals the zero slope, hence H(c)=0, and obtains the contradiction from the positivity neighborhood.
why it matters in Recognition Science
The lemma supplies the first step of the integration bootstrap inside dAlembert_contDiff_nat, which lifts continuous solutions to C^n for every n and thereby feeds the full classification in Aczél's theorem. In the Recognition Science setting it converts the algebraic cost function H (arising from J via the RCL) into the analytic regime required for the forcing chain. No open scaffolding remains at this node.
scope and limits
- Does not assume the d'Alembert functional equation.
- Does not presuppose differentiability of H.
- Does not produce an explicit numerical value for delta.
- Does not address complex-valued or higher-dimensional analogues.
Lean usage
obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_contformal statement (Lean)
48private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
49 ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
proof body
Tactic-mode proof.
50 have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
51 have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
52 h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
53 obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
54 refine ⟨ε / 2, by positivity, ?_⟩
55 intro h_eq
56 have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
57 obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
58 ((phi_differentiable H h_cont).continuous.continuousOn)
59 (fun x _ => phi_hasDerivAt H h_cont x)
60 rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
61 linarith [hε (show dist c 0 < ε by
62 simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
63