CanonicalRemainderLineTaylorDataTarget
plain-language theorem explainer
Packages the one-variable analytic data needed on every conformal ray through the flat configuration: the canonical Regge remainder, restricted to t ↦ tξ, is C³ on [0,1], its quadratic Taylor jet at 0 vanishes when evaluated at 1, and the third derivative is O(‖ξ‖³). Anyone closing the cubic Taylor theorem for the nonlinear Regge remainder cites this target. It is a pure Prop definition assembling three Mathlib-shaped conditions with uniform radius and constant.
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$, the map $t\mapsto R_K(t\xi)$ (canonical Regge remainder along the ray through $\xi$) is $C^3$ on $[0,1]$, its degree-$2$ Taylor polynomial at $0$ evaluates to $0$ at $t=1$, and $|\partial_t^3 R_K(t\xi)|\le M\|\xi\|^3$ for all $t\in[0,1]$.
background
The module isolates the last analytic step after the nonlinear Hessian of the discrete Regge action has been identified with the canonical graph-Laplacian Hessian built from incidence dual weights. The remainder
$$R_K(\xi)=S_K(\xi)-S_K(0)-\tfrac12 H(\xi,\xi)$$
subtracts the flat value and that quadratic form; the goal is a uniform cubic bound on $R_K$ near the origin in the finite-dimensional space of vertex potentials.
Geometric reductions already cut the problem down to one-variable restrictions along conformal lines $\mathrm{linePotential}(K,\xi,t)=t\xi$. Upstream, canonicalReggeHessian supplies the candidate quadratic term and reggeActionRemainder the nonlinear leftover. The present target records exactly the Mathlib data (ContDiffOn of order 3 on the unit segment, vanishing quadratic Taylor evaluation, and a third-derivative bound scaled by $|\xi|^3$) needed to feed a standard one-variable Taylor remainder estimate.
proof idea
Pure definition of a Prop; no proof obligations. The body is an existential package: witnesses $r>0$, $M\ge 0$, and a universal quantifier over directions $\xi$ inside the ball of radius $r$. For each such $\xi$ three conjuncts are required of the scalar path $t\mapsto R_K(t\xi)$ on $[0,1]$: (i) ContDiffOn of order 3, (ii) taylorWithinEval of order 2 at 0 equals 0 when evaluated at 1, (iii) pointwise bound on the third iterated derivative by $M|\xi|^3$. Downstream lemmas discharge the package by assembling separate ContDiff, quadratic-vanishing, and third-derivative targets (or by cascade from FlatConfiguration plus first/second jet inputs).
why it matters
This is the precise analytic bridge left after all geometric reductions in the cubic Taylor program for the nonlinear Regge remainder. Downstream, lineTaylorData_of_splitTargets builds it from three split targets; lineCubicEstimate_of_lineTaylorData turns it into a cubic remainder estimate (factor $M/6$); and nonlinearReggeCubicTaylorTheorem_of_lineTaylorData lifts that estimate to the full finite-dimensional cubic Taylor theorem. Cascade closures (canonicalRemainderLineTaylorData_of_flat_and_remainderJets, CanonicalRemainderAnalyticClosureCert) show the target follows from FlatConfiguration plus remainder first- and second-variation jet inputs once chain-rule and local-norm bounds are closed. In the broader Recognition geometry stack this supplies the last analytic ingredient that converts discrete Hessian identification into a controlled cubic error, the discrete analogue of a $C^3$ Taylor expansion of the Einstein–Hilbert action about flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.