CanonicalRemainderLineQuadraticTaylorZeroTarget
plain-language theorem explainer
Packages the local vanishing of the degree-2 Taylor polynomial of the line-restricted canonical Regge remainder at t=1. Anyone assembling the cubic Taylor bound for the nonlinear Regge action cites this as the quadratic-jet half of the line Taylor data. It is a Prop definition: existence of a positive radius on which that evaluation is identically zero for small vertex potentials.
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 degree-2 Taylor polynomial (on $[0,1]$, expanded at $0$) of $t \mapsto R_K(H_{\mathrm{can}}, t\xi)$ evaluates to $0$ at $t=1$, where $R_K$ is the Regge action remainder after subtracting the flat value and the canonical Hessian quadratic form, and $H_{\mathrm{can}}$ is the canonical graph-Laplacian Hessian.
background
The module isolates the final analytic Taylor theorem needed once the nonlinear Hessian is identified: a local third-order bound on the Regge remainder in finite-dimensional vertex-potential space.
The Regge action remainder $R_K(H,\xi)$ subtracts the flat value and a candidate quadratic Hessian term from the full Regge action. Here $H$ is fixed to the canonical graph-Laplacian Hessian induced by incidence dual weights. The line potential $t\mapsto t\xi$ is the straight ray through the flat configuration in direction $\xi$.
taylorWithinEval f n s x y is the degree-$n$ Taylor polynomial of $f$ on set $s$, expanded at $x$, evaluated at $y$. The target asks that this polynomial of the line-restricted remainder, at order 2 on $[0,1]$ about $0$, vanish at $t=1$ for all sufficiently small $\xi$.
proof idea
Definition only: no proof obligations. The body is the existential Prop that a positive radius $r$ exists so the degree-2 within-Taylor evaluation of the line-restricted canonical remainder is zero at $t=1$ whenever $|\xi|<r$. Downstream theorems discharge it from flatness plus first- and second-variation jet inputs (or from flatness, first variation, and the directional Hessian theorem).
why it matters
This is the quadratic-vanishing half of the line Taylor data for the cubic remainder bound. It feeds lineTaylorData_of_splitTargets (together with contDiff and third-derivative bound targets), the jet-input closure canonicalRemainderLineQuadraticTaylorZero_of_jetInputs, and the flat-plus-directional-Hessian route. The cascade certificate CanonicalRemainderAnalyticClosureCert records it as line_quadratic_zero_from_jets.
In the Recognition geometry stack this is the analytic step that makes the nonlinear Regge remainder genuinely $O(|\xi|^3)$ along rays once the canonical Hessian has absorbed the quadratic piece, supporting the local cubic Taylor theorem after Hessian identification. It does not itself invoke the forcing chain (T0–T8) or RCL; it is pure discrete-geometry analysis on 3D triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.