CanonicalRemainderLineContDiffTarget
plain-language theorem explainer
Names the analytic target that the canonical Regge remainder, restricted to short rays through the flat configuration, is C³ on the unit interval. Anyone assembling the cubic Taylor bound for the nonlinear Regge action cites this Prop as the contDiff half of the line-jet package. It is a pure interface definition: existence of a positive radius with a ContDiffOn hypothesis along each ray.
Claim. For an incidence-consistent 3D triangulation $K$, the following holds: there exists $r>0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, the map $t\mapsto R_K(t\xi)$ is $C^3$ on $[0,1]$, where $R_K$ is the Regge action remainder after subtracting the value at the zero potential and the quadratic form of the canonical graph-Laplacian Hessian.
background
The module isolates the final analytic Taylor theorem needed once the nonlinear Hessian of the discrete Regge action is identified. The heavy content is a local third-order bound 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 $t\mapsto t\xi$ is the straight ray through the flat configuration in direction $\xi$.
ContDiffOn $\mathbb{R}$ of order 3 on the compact interval $[0,1]$ is the regularity needed so that a one-variable Taylor expansion with cubic remainder can be written along every short ray, which is the standard route from jet data to a uniform cubic bound in finite dimension.
proof idea
Definition only: the body is the Prop $\exists r>0,;\forall\xi,;|\xi|<r\Rightarrow$ ContDiffOn $\mathbb{R}$ order 3 of $t\mapsto$ reggeActionRemainder$(K,hK,$ canonicalReggeHessian$,$ linePotential $K,\xi,t)$ on $[0,1]$. No proof obligations; discharge is deferred to theorems such as canonicalRemainderLineContDiff_of_flatConfiguration.
why it matters
This target is one leg of the cascade that closes the cubic Taylor theorem for the nonlinear Regge remainder. CanonicalRemainderAnalyticClosureCert packages it as line_contDiff_from_flat: FlatConfiguration implies this Prop. lineTaylorData_of_splitTargets consumes it together with the quadratic-jet-zero and third-derivative-bound targets to assemble full line Taylor data. That data feeds nonlinearReggeLocalHessianTaylorInputs and ultimately NonlinearReggeCubicTaylorTheorem.
In the Recognition geometry stack the cubic remainder bound is the analytic step that turns the identified discrete Hessian into a controlled nonlinear expansion around flat configurations, which is required before continuum or curvature-limit arguments. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it sits strictly in the Regge-calculus geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.