HasSecondDerivAt
plain-language theorem explainer
Predicate asserting that a real function of one variable has a prescribed second derivative at a point. It is the local analytic atom for directional Hessian comparisons along lines in vertex-potential space. Anyone citing the nonlinear Regge second-variation or cubic-remainder targets will hit this wrapper. The body is a one-line packaging of Mathlib's first-derivative predicate applied to the first derivative.
Claim. For $f:\mathbb{R}\to\mathbb{R}$, a candidate value $d_2\in\mathbb{R}$, and a point $x\in\mathbb{R}$, the statement that the map $t\mapsto f'(t)$ is differentiable at $x$ with derivative $d_2$ (equivalently, $f''(x)=d_2$ in the one-variable sense).
background
The module fixes the nonlinear second-variation and cubic-remainder targets for the Regge action in a form usable before the full Cayley-Menger/arccos chain-rule expansion is complete. Analytic obligations therefore live in named input structures rather than in a finished closed-form expansion.
Along a line $t\mapsto t\xi$ in the space of vertex potentials, the restricted action (or its quadratic and remainder pieces) becomes an ordinary real function of one real variable. Second directional derivatives then reduce to ordinary second derivatives of that restriction. The present predicate is exactly that one-variable statement: the first derivative map is itself differentiable at the evaluation point with a named value.
It sits next to the first-variation infrastructure imported from the sibling first-variation module and is the second-order counterpart used when comparing the nonlinear action to the canonical Regge Hessian quadratic form.
proof idea
Pure definition, not a proved theorem. The body is the Mathlib predicate that the function $t\mapsto(\mathrm{deriv},f),t$ has derivative $d_2$ at $x$. No lemmas are applied; no tactics run. Downstream proofs either discharge instances by direct differentiation of explicit quadratics or assume the predicate as a field of an input structure.
why it matters
This is the shared second-derivative interface for the whole Regge second-variation stack. Downstream, the nonlinear Hessian proof uses it to state that the canonical quadratic along a line has second derivative equal to the canonical Hessian quadratic form at zero, and to package several routes to vanishing second variation of the remainder (identically zero remainder, nonlinear Hessian plus derivative identity, and the near-zero variant). The cubic Taylor bound module consumes the same predicate inside the remainder second-variation input to force the second iterated derivative of the remainder line to vanish at zero, which is the jet condition needed for a cubic remainder.
In the broader Recognition geometry layer this is bookkeeping, not a forcing-chain step: it lets directional Hessian comparisons be stated uniformly while the heavy arccos expansion remains staged behind named targets. It does not itself touch T5-T8, RCL, or the mass ladder; it only keeps the discrete-curvature second-variation story mathematically precise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.