sinh_deriv_at_zero
plain-language theorem explainer
The derivative of sinh at zero equals one, so the first-order linearization of sinh(ε) is just ε with unit coefficient. Gravity and continuum-limit arguments cite it when the Euler-Lagrange equation of the J-cost action is reduced to the lattice Laplacian. The proof is a one-line rewrite via the standard derivative of sinh and cosh(0) = 1.
Claim. The real derivative satisfies $\frac{d}{dx}\sinh(x)\big|_{x=0} = 1$. Equivalently $\cosh(0) = 1$, so near the vacuum the expansion $\sinh(\varepsilon) = \varepsilon + O(\varepsilon^3)$ needs no rescaling factor.
background
This module gives a direct cubic-lattice proof that J-cost Regge dynamics on $\mathbb{Z}^D$ converge to the continuum variational principle (linearized Einstein equations), replacing a general Cheeger-Müller-Schrader axiom. The cost is fixed: $J(e^\varepsilon) = \cosh(\varepsilon) - 1$, so the Euler-Lagrange equation involves $\sinh$.
Tier 2 of the strategy linearizes that EL equation. Replacing $\sinh(\varepsilon)$ by $\varepsilon$ is legitimate only if the linearization coefficient is unity, i.e. $\sinh'(0) = 1$. The lattice Laplacian $(\Delta_{\mathrm{lat}} f)(x) = \sum_k\bigl[f(x+e_k)+f(x-e_k)-2f(x)\bigr]$ then appears as the exact linearization of the discrete EL operator.
Upstream continuum-limit infrastructure supplies that Laplacian and the second-order mesh expansion used in Tier 3; the present lemma is the elementary analytic input that makes the coefficient clean.
proof idea
Term-mode, two steps. Rewrite the goal with Mathlib's Real.deriv_sinh, which states $\mathrm{deriv},\sinh = \cosh$. The goal becomes $\cosh(0) = 1$, discharged by Real.cosh_zero. No Recognition-specific lemmas are required; the result is pure real analysis used as a coefficient check.
why it matters
Tier 2 of the cubic Regge convergence chain needs $\sinh'(0)=1$ so that the linearized EL operator equals minus the lattice Laplacian with no extra constant. Downstream, proved_convergence_chain records this fact explicitly as step5_linearization, and cubic_regge_convergence_cert packages the whole zero-axiom, zero-sorry certificate (action quadratic approximation, EL equals Laplacian, flat solutions).
In the RS forcing picture the cost is already fixed as $J(x)=\cosh(\log x)-1$ (T5 J-uniqueness), so the EL linearization coefficient is not free: it must be one. That is why a one-line Mathlib fact earns a named theorem here: it closes the coefficient gap between discrete J-cost dynamics on $\mathbb{Z}^D$ and continuum $\nabla^2$ at $O(a^2)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.