even_deriv_at_zero
plain-language theorem explainer
Even functions from reals to reals that are differentiable at the origin have vanishing first derivative there. Researchers reducing the Recognition Composition Law to d'Alembert form for the T5 J-uniqueness proof cite this when preparing the calibration step that forces the cosh solution. The argument equates the derivative of H at zero with that of its composition against negation, applies the chain rule to obtain a sign flip, and concludes via linear arithmetic.
Claim. Let $H : ℝ → ℝ$ satisfy $H(-x) = H(x)$ for all $x$ and be differentiable at $0$. Then $H'(0) = 0$.
background
The Cost.FunctionalEquation module supplies supporting lemmas for the T5 cost-uniqueness argument. Here H is the shifted cost function defined by H(t) = G(t) + 1, where G itself arises from the J-cost reparametrization J(x) = (x + x^{-1})/2 - 1. Upstream, the theorem h_even from JCostConvexityInLogSpace records that the underlying cost function is even: h(t) = h(-t). This evenness is inherited by H and is the key hypothesis of the present lemma.
proof idea
The tactic proof introduces the auxiliary map negFun x := -x. It first proves deriv H 0 = deriv (H ∘ negFun) 0 by rewriting via the evenness hypothesis. It then invokes differentiability of negation together with the chain rule (deriv_comp) to obtain deriv (H ∘ negFun) 0 = -deriv H 0. Equating the two expressions and applying linarith yields the claim.
why it matters
The result is invoked by dAlembert_classification, dAlembert_cosh_solution, and dAlembert_cosh_solution_aczel, all of which classify solutions of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. These theorems in turn supply the cosh branch required by the T5 forcing step (J-uniqueness) in the Recognition Science chain. The lemma therefore closes the first-derivative calibration needed before the second-derivative condition selects the hyperbolic cosine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.