F_zero
plain-language theorem explainer
The residual F(s,h) = cosh(s+h) − cosh s − sinh(s)·h − h²/2 vanishes at h = 0 for every real s. Anyone establishing nonnegativity or a quadratic well for this residual cites the zero basepoint first. The proof is a one-line simplification of the definition.
Claim. For every real $s$, $F(s,0)=0$, where $F(s,h)=\cosh(s+h)-\cosh s-\sinh s\cdot h-h^{2}/2$.
background
In the sourced-minimizer diameter module, the helper $F(s,h)$ measures the excess of $\cosh(s+h)$ over its first-order Taylor piece at $s$ plus a quadratic penalty $h^{2}/2$. Explicitly, $F(s,h)=\cosh(s+h)-\cosh s-\sinh s\cdot h-h^{2}/2$.
This residual appears when controlling how a sourced tick or hinge stationarity condition behaves under small shifts $h$. The companion map $g$ and its derivative facts live in the same file; $F$ is the integrated object whose sign and growth feed diameter bounds.
The local setting is real analysis on $\mathbb{R}$ (cosh/sinh calculus), not yet the full Recognition ladder or $\phi$-scaling. An unrelated display function also named $F$ exists in AnchorPolicy (the gap map); the present $F$ is the private hyperbolic residual in this module.
proof idea
One-line wrapper: simp [F] unfolds the definition. Substituting $h=0$ gives $\cosh(s+0)-\cosh s-\sinh s\cdot 0-0^{2}/2$, which cancels termwise to $0$. No external lemmas are required.
why it matters
Supplies the base value for F_nonneg, which proves $F(s,h)\ge 0$ for all real $s,h$ by a monotone-on-derivative argument on $[0,\infty)$ (and a symmetric treatment for negative $h$). That nonnegativity is the analytic core of the sourced-tick quadratic well and the approximate tick-distance controls in the same module.
In the broader Seven Gaps gravity stack, a nonnegative residual with a known zero at the expansion point is the standard way to turn a second-order Taylor identity for cosh into a diameter or stationarity bound. The declaration itself is elementary; its place is as the clean zero-point lemma that the sign proof and the well lemma both need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.