J_log_second_deriv_at_zero
plain-language theorem explainer
The second derivative of the log-cost function J_log at zero equals one. Researchers formalizing the Recognition Science cost landscape cite this to fix the curvature scale that sets the minimum step cost for discrete configurations. The proof is a direct differentiation of the cosh definition of J_log, reducing via sinh to the known value of cosh at zero.
Claim. $ (J_ {log})''(0) = 1 $ where $ J_{log}(t) := cosh(t) - 1 $.
background
In the DiscretenessForcing module the multiplicative cost J(x) = ½(x + x^{-1}) - 1 is rewritten in logarithmic coordinates. The sibling definition J_log(t) := cosh(t) - 1 produces a convex bowl centered at t = 0 whose second derivative at the minimum supplies the stiffness scale. The module argument is that continuous spaces allow infinitesimal perturbations at infinitesimal cost while discrete spaces trap configurations behind finite cost barriers.
proof idea
The tactic proof first shows deriv J_log = sinh by unfolding the definition and rewriting with the derivative of cosh. It then applies the derivative of sinh to obtain cosh and evaluates at zero using the known identity cosh(0) = 1.
why it matters
This equality supplies the curvature term inside the parent theorem discreteness_forcing_principle, which lists four conditions that together force discrete ontology from the cost functional. The module doc-comment states that J''(1) = 1 sets the minimum step cost; the result therefore closes one of the four conjuncts required for the discreteness forcing principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.