EL_stationary_at_zero
plain-language theorem explainer
Derivative of the log-domain cost vanishes at the origin. Researchers modeling the Recognition Science energy functional cite this to confirm the stationary point condition required for the Euler-Lagrange property. The proof is a one-line simplification that applies derivative rules to the explicit hyperbolic form of the cost.
Claim. $ (d/dt) [ (e^t + e^{-t})/2 - 1 ] |_{t=0} = 0 $
background
Jlog is the log-domain cost obtained by composing the base cost with the exponential map, producing the explicit expression ((exp t + exp(-t))/2) - 1. This converts the multiplicative cost into an additive function on the logarithmic scale, matching the J-uniqueness form from the forcing chain. The upstream definition of Jlog supplies the hyperbolic cosine expression used for differentiation.
proof idea
One-line wrapper that applies the simp tactic. The tactic unfolds the definition of Jlog and reduces the derivative at zero using standard rules for the exponential and hyperbolic cosine.
why it matters
This result supplies the stationary condition inside EL_holds, which packages the full Euler-Lagrange property for the cost functional together with the global minimum. It anchors the zero point of the cost structure, consistent with the self-similar fixed point and J-uniqueness step in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.