CanonicalRemainderLineCubicEstimateTarget
plain-language theorem explainer
Existence of a local cubic bound on the canonical nonlinear Regge remainder along every ray through the flat configuration: for small vertex potentials ξ, the remainder at ξ is at most C‖ξ‖³. Analysts closing the Regge cubic Taylor theorem cite this as the one-dimensional line form of the third-order estimate. It is a Prop definition packaging radius and constant; discharge comes from one-variable Taylor data with a uniform third-derivative bound on segments.
Claim. For an incidence-consistent triangulation $K$ in three dimensions, there exist $r>0$ and $C\ge 0$ such that every vertex potential $\xi$ with $\|\xi\|<r$ satisfies $\|R_K(H_{\mathrm{can}},\xi)\|\le C\|\xi\|^3$, where $R_K$ is the nonlinear Regge remainder (full action minus value at the zero potential minus half the quadratic form of the canonical graph-Laplacian Hessian) and the evaluation point is the unit-parameter point on the ray $t\mapsto t\xi$.
background
The module isolates the last analytic step after the nonlinear Hessian of the Regge action has been 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(H,\xi)$ subtracts the action at the flat (zero) potential and the candidate quadratic term $\tfrac12$ hessianQuadratic $H,\xi$ from the full Regge action. Here $H$ is fixed to 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$; evaluating at parameter $t=1$ places the remainder at $\xi$ itself.
The surrounding development already has first- and second-variation vanishing at the flat point along these rays. What remains is a cubic estimate, which this target states in pure one-dimensional form so a standard scalar Taylor theorem can finish the job.
proof idea
Definitional packaging only: the body is the existential Prop asserting a radius $r>0$ and constant $C\ge 0$ such that the norm of the canonical remainder at linePotential $K,\xi,1$ is $\le C|\xi|^3$ whenever $|\xi|<r$. No tactics or lemmas are applied at this declaration. Downstream, lineCubicEstimate_of_lineTaylorData discharges it from CanonicalRemainderLineTaylorDataTarget by taking $C=M/6$ from a uniform third-derivative bound $M$ on the segment.
why it matters
This is the bridge Prop between one-variable Taylor data and the full nonlinear cubic Taylor theorem for the Regge remainder. The parent theorem nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate lifts any proof of this line estimate to NonlinearReggeCubicTaylorTheorem by the same radius and constant. The sibling lineCubicEstimate_of_lineTaylorData is the intended discharge route: feed in zero value, vanishing first and second variations, and a bound on third derivatives along the segment.
In the Recognition geometry stack this closes the analytic remainder control once the canonical Hessian is fixed, so the discrete action sits in the cubic-Taylor regime needed for continuum comparison. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those live upstream of the geometric model. The open work it touches is purely the supply of line Taylor data (third-derivative bounds) on concrete triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.