exists_integral_ne_zero
Continuous real functions H with H(0) = 1 admit a positive δ such that the integral of H from 0 to δ is nonzero. Analysts working on functional equations cite this to launch the regularity bootstrap for d'Alembert solutions. The argument uses continuity to locate a neighborhood where H stays positive, then applies the mean value theorem to the antiderivative Phi to reach a contradiction if the integral vanishes.
claimLet $H:ℝ→ℝ$ be continuous with $H(0)=1$. Then there exists $δ>0$ such that $Φ_H(δ)≠0$, where $Φ_H(t)=∫_0^t H(s) ds$.
background
The module proves every continuous solution H to the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) with H(0)=1 is C^∞, recovering the Aczél classification (constant 1, cosh, or cos). Phi is the antiderivative Phi(H)(t) := ∫_0^t H(s) ds. Upstream, H is the shifted cost J(x)+1, which turns the Recognition Composition Law into the standard d'Alembert equation.
proof idea
The proof first records H(0)=1>0, then uses continuity to obtain an ε-neighborhood where H(x)>0. It assumes for contradiction that Phi(ε/2)=0 and invokes exists_hasDerivAt_eq_slope on Phi H (differentiable by phi_differentiable, with derivative H by phi_hasDerivAt). This yields c in (0,ε/2) with H(c)=0, contradicting positivity. phi_zero supplies the base case at the origin.
why it matters in Recognition Science
The lemma supplies the nonzero δ required by the representation formula inside dAlembert_contDiff_nat, which establishes that continuous d'Alembert solutions are C^∞ for all orders. It removes the last foundation hypothesis (H_AczelClassification) from the IndisputableMonolith codebase. In Recognition Science this confirms smoothness of the shifted cost H, aligning with J-uniqueness and the phi fixed point in the T0-T8 forcing chain.
scope and limits
- Does not assume the d'Alembert equation.
- Does not produce an explicit numerical bound on δ.
- Does not apply to discontinuous H.
- Does not classify solutions or derive the ODE H''=cH.
Lean usage
obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_contformal statement (Lean)
112private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
113 ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
proof body
Tactic-mode proof.
114 have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
115 have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
116 h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
117 obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
118 refine ⟨ε / 2, by positivity, ?_⟩
119 intro h_eq
120 have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
121 obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
122 ((phi_differentiable H h_cont).continuous.continuousOn)
123 (fun x _ => phi_hasDerivAt H h_cont x)
124 rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
125 linarith [hε (show dist c 0 < ε by
126 simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
127
128/-- The representation formula: H(t) = (Φ(t+δ) − Φ(t−δ)) / (2·Φ(δ)).
129 This is the key identity that bootstraps regularity. -/