even_function_deriv_zero
plain-language theorem explainer
Even differentiable functions on the reals have zero derivative at the origin. Analysts working on the Recognition Science analytic bridge invoke this to fix the initial slope of the log-lifted cost function G under evenness symmetry. The proof equates G to its reflection via function extensionality, applies the chain rule to the composition with negation, and concludes by linear arithmetic.
Claim. Let $G : ℝ → ℝ$ be differentiable at $0$ and even, i.e., $G(-t) = G(t)$ for all $t ∈ ℝ$. Then $G'(0) = 0$.
background
The AnalyticBridge module reparametrizes cost functions via the log-lift G_of F(t) := F(exp t), converting multiplicative consistency conditions on F into additive functional equations on G. Evenness of G arises from symmetry hypotheses such as F(x) = F(x^{-1}). The module imports standard differentiation infrastructure from Mathlib together with local definitions G_of and the structural axioms from NecessityGates and CurvatureGate. Upstream results include the definition of G as the log-coordinate reparametrization and the negation operation used in the chain-rule step.
proof idea
The tactic proof first uses function extensionality on the evenness hypothesis to obtain equality of the reflected function with G. It then equates their derivatives at zero. The reflected function is rewritten as the composition G ∘ negation; the chain rule together with differentiability of negation yields the negative of the original derivative. Linear arithmetic then forces the derivative to equal its own negative, hence zero.
why it matters
This lemma supplies the vanishing first derivative at zero required by the initial conditions in F_forced_to_Jcost, which concludes that interaction forces F to equal the J-cost function. It thereby closes one step in the bridge theorem that structural axioms plus interaction admit no third option between additive and d'Alembert forms. In the broader chain it supports T5 J-uniqueness by ensuring the even log-lift G satisfies the boundary data that selects the hyperbolic solution G = cosh(log x) - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.