dAlembert_continuous_of_log_curvature
plain-language theorem explainer
Functions satisfying the d'Alembert equation with a finite logarithmic curvature condition at the origin are continuous on the reals. Researchers deriving the uniqueness of the J-cost function in Recognition Science would cite this to justify passing to the cosh solution. The proof proceeds by first extracting H(u) → 1 as u → 0 from the curvature hypothesis, then using the functional equation together with the dAlembert_diff_square identity to control sums and differences and obtain the limit at every shifted point t.
Claim. Let $H : ℝ → ℝ$ satisfy $H(0) = 1$, $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, and $lim_{t→0} 2(H(t)-1)/t² = κ$ for some real κ. Then $H$ is continuous.
background
In the Cost.FunctionalEquation module, which supplies helpers for the T5 J-uniqueness proof, the function H is the shifted cost H_F(t) := G_F(t) + 1. This reparametrization converts the Recognition Composition Law into the classical d'Alembert functional equation. HasLogCurvature H κ asserts that the second-order behavior near zero is controlled by the constant κ, specifically the limit of 2(H(t)-1)/t² equals κ. The module imports standard real analysis from Mathlib, including derivatives and Taylor expansions. Upstream, the lemma dAlembert_diff_square provides the identity (H(t+u) - H(t-u))² = 4 ((H t)² - 1) ((H u)² - 1), which is invoked to control the difference term. The tendsto_H_one_of_log_curvature lemma extracts the limit H(u) → 1 as u → 0 from the curvature hypothesis.
proof idea
The proof is a long tactic script establishing continuity at arbitrary t by verifying lim_{u→0} H(t+u) = H t. It invokes tendsto_H_one_of_log_curvature to obtain H(u) → 1. The d'Alembert equation shows that H(t+u) + H(t-u) tends to 2 H t. Then dAlembert_diff_square is applied to prove that the squared difference tends to zero, implying the absolute difference tends to zero. Adding the sum and difference limits yields the limit for 2 H(t+u), hence for H(t+u). This is rewritten as a limit under the shifted neighborhood nhds t.
why it matters
This result is a key step in establishing the cosh form of the solution under the log curvature condition, feeding directly into the theorem dAlembert_cosh_solution_of_log_curvature. It supports the T5 J-uniqueness claim in the Recognition Science forcing chain by ensuring that solutions to the functional equation are sufficiently regular to be identified with the hyperbolic cosine. The parent result closes the gap between the algebraic d'Alembert equation and the analytic properties needed for uniqueness in the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.