hasDerivAt_F
plain-language theorem explainer
At every real point h, the remainder F(s,·) after the order-1 Taylor expansion of cosh about s, with an extra −h²/2, is differentiable with derivative g(s,h)=sinh(s+h)−sinh s−h. Gravity/SevenGaps arguments cite this to feed nonnegativity of F via a monotone-derivative test. The proof is elementary calculus: differentiate each summand and reassemble.
Claim. For all real $s$ and $h$, the map $x \mapsto \cosh(s+x) - \cosh s - (\sinh s)\, x - x^2/2$ is differentiable at $h$, and its derivative there equals $\sinh(s+h) - \sinh s - h$.
background
In the SevenGaps sourced-minimizer module, the private helper $F(s,h) := \cosh(s+h) - \cosh s - (\sinh s), h - h^2/2$ measures how much $\cosh$ exceeds its first-order Taylor jet at $s$, after subtracting an extra quadratic $h^2/2$. The companion helper $g(s,h) := \sinh(s+h) - \sinh s - h$ is the formal $h$-derivative of that expression.
The local setting is real one-variable calculus on hyperbolic functions, imported through the hinge-stationarity core. No Recognition-specific constants enter the statement: $s$ and $h$ are arbitrary reals. Downstream, nonnegativity of $F$ on half-lines is obtained from the sign of this derivative together with $F(s,0)=0$.
proof idea
Build HasDerivAt for each piece at $h$:
- $\cosh(s+x)$ by composing
Real.hasDerivAt_coshwithid.const_add s, giving derivative $\sinh(s+h)$; - the constant $\cosh s$, derivative $0$;
- the linear term $(\sinh s), x$, derivative $\sinh s$;
- $x^2/2$ via
hasDerivAt_pow 2and division by $2$, derivative $h$.
Subtract in order: $(\cosh\circ(\mathrm{id}+s)) - \mathrm{const} - \mathrm{lin} - \mathrm{quad}$. The resulting derivative is $\sinh(s+h)-\sinh s-h$. Finish by simpa [F, g].
why it matters
This is the differentiability engine for $F$ inside SourcedMinimizerSupDiameter. The sole direct consumer is F_nonneg, which marks $F(s,\cdot)$ differentiable, continuous, and monotone on $[0,\infty)$ by testing that the derivative $g$ is nonnegative there, then concludes $F\ge 0$ from $F(s,0)=0$.
That nonnegativity underwrites the sourced-tick quadratic well and the approximate tick-distance estimates in the same module: the extra $-h^2/2$ turns the hyperbolic remainder into a controlled nonnegative defect used when bounding sourced minimizer diameters. In the broader Gravity/SevenGaps chain this is pure analytic scaffolding, not a T0–T8 forcing step, but it closes the calculus gap needed before those geometric bounds can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.