symmetric_second_diff_limit_hypothesis
plain-language theorem explainer
This definition packages the symmetric second difference limit hypothesis for functions H obeying the d'Alembert equation. Workers closing regularity gaps in the T5 J-uniqueness argument cite it when discharging the second-order Taylor condition. It is a direct definition that assembles the premises H(0)=1, continuity, the functional equation, the derivative condition at zero, and the limit statement into one Prop.
Claim. Let $H : ℝ → ℝ$. The symmetric second difference limit hypothesis at $t$ asserts that if $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and the derivative of $H'$ at 0 equals 1, then the limit as $u→0$ of $(H(t+u)+H(t-u)-2H(t))/u^2$ equals $H(t)$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost reparametrization H(x) = J(x) + 1, which converts the Recognition Composition Law into the classical d'Alembert equation. The upstream dAlembert_continuous_implies_smooth_hypothesis records Aczél's theorem that continuous solutions with H(0)=1 are analytic and satisfy the ODE H''=H.
proof idea
One-line definition that directly encodes the hypothesis as the implication from the d'Alembert premises plus the HasDerivAt condition to the second-difference limit equaling H(t). No tactics or lemmas are applied inside the body; the definition simply assembles the Prop.
why it matters
It closes one of the five regularity hypothesis gaps in washburn_uniqueness, as stated in the module documentation. Once the Aczél axiom is added, the hypothesis becomes provable and yields a hypothesis-free uniqueness theorem. The definition supports the T5 step that forces J-uniqueness as (x + x^{-1})/2 - 1 and the subsequent derivation of the ODE from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.