CanonicalRemainderLineThirdDerivBoundTarget
plain-language theorem explainer
Existence of a radius r>0 and constant M≥0 so that, along every ray t↦tξ through the flat configuration, the third ordinary derivative of the canonical Regge remainder is bounded by M‖ξ‖³ for all t∈[0,1] and ‖ξ‖<r. Analysts closing the cubic Taylor theorem for the nonlinear Regge action cite this target. It is a pure Prop interface; proofs discharge it via chain rule plus a local Fréchet third-derivative bound.
Claim. For an incidence-consistent 3D triangulation $K$, the following holds: there exist $r>0$ and $M\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$ and every $t\in[0,1]$, $$\bigl|\partial_s^3 R_K\bigl(s\xi\bigr)\big|_{s=t}\bigr| \le M\|\xi\|^3,$$ where $R_K$ is the nonlinear Regge action remainder after subtracting the value at the zero potential and the quadratic form of the canonical graph-Laplacian Hessian, and $s\xi$ is the straight line through the flat potential in direction $\xi$.
background
The module isolates the final analytic Taylor step once the nonlinear Hessian is identified: a local third-order bound on the remainder in the finite-dimensional space of vertex potentials on a 3D triangulation.
The remainder $R_K(\xi)$ is the full Regge action minus its value at the zero (flat) potential minus half the quadratic form of a candidate Hessian $H$. Here $H$ is fixed to be the canonical graph-Laplacian Hessian built from incidence dual weights. The line potential $s\mapsto s\xi$ is the straight ray through the flat configuration in direction $\xi$.
The target asks only for a uniform cubic bound on the ordinary third derivative of the scalar function $s\mapsto R_K(s\xi)$ for small $\xi$ and $s\in[0,1]$. Upstream pieces supply the remainder definition, the canonical Hessian, and the line embedding; smoothness and Fréchet bounds live in sibling targets closed under a flat-configuration hypothesis.
proof idea
No proof: this is a Prop-valued definition packaging an existential third-derivative estimate. Downstream closures prove it. The main path is canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm, which takes a chain-rule bound on the line-restricted third derivative and a local norm bound on the third Fréchet derivative of the remainder, then sets $r:=\delta$ from the local ball and reuses the same $M$. The flat-configuration closure composes that with canonicalRemainderLineChainRuleBound_of_flatConfiguration and the local Fréchet bound under flatness. A further wrapper folds the result into line Taylor data via lineTaylorData_of_splitTargets.
why it matters
This target is one of the three split analytic inputs (continuity/smoothness, quadratic jet vanishing, third-derivative bound) that assemble into line Taylor data and thence the cubic Taylor theorem for the nonlinear Regge remainder. Downstream, canonicalRemainderLineThirdDerivBound_of_flatConfiguration closes it from flatness alone; CanonicalRemainderAnalyticClosureCert and nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_remainderJetTarget consume it in the cascade that yields the cubic Taylor theorem. The audit lemma canonicalRemainderLineThirdDerivBound_closed records discharge. In the broader Recognition geometry stack this is the last local analytic estimate needed after Hessian identification, before global discrete-to-continuum comparison; it does not itself touch T0–T8 or the RCL, but sits in the Regge side of the geometric forcing chain toward continuum curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.