canonicalRemainderLine_value_at_zero
plain-language theorem explainer
The nonlinear Regge remainder, taken with the canonical Hessian, vanishes when the ray through any vertex potential is evaluated at the origin. Anyone assembling the cubic Taylor bound along that ray cites this base value. The proof rewrites the line at zero to the flat potential and applies the known remainder-vanishing lemma there.
Claim. For any incidence-consistent 3D triangulation $K$ and any vertex potential $\xi$, the nonlinear Regge remainder $R_K$ (after subtracting the flat value and the canonical Hessian quadratic) satisfies $R_K(0\cdot\xi)=0$, where $t\mapsto t\cdot\xi$ is the straight-line path in potential space.
background
This module isolates the cubic Taylor bound for the nonlinear Regge remainder after the Hessian has been fixed. The remainder $R_K(H,\xi)$ is the full Regge action minus its value at the flat (zero) potential minus half the quadratic form of a candidate Hessian $H$. The canonical choice of $H$ is the graph-Laplacian built from incidence dual weights on the triangulation.
The straight-line path in vertex-potential space is $t\mapsto t\cdot\xi$ (denoted line potential). At $t=0$ that path is the zero potential. Upstream, the remainder is already known to vanish at the zero potential for every candidate Hessian: "The nonlinear remainder vanishes at the flat potential, for every candidate Hessian."
The local setting is finite-dimensional analysis on vertex potentials of an incidence-consistent 3D triangulation, preparing third-order estimates along rays from the flat configuration.
proof idea
Term-mode, two steps. First rewrite the line potential at parameter $0$ to the zero (flat) potential via the identity that $0\cdot\xi$ is the zero potential. Then apply the upstream lemma that the remainder vanishes at the zero potential for any Hessian, specializing the Hessian argument to the canonical graph-Laplacian Hessian. No further analytic work.
why it matters
This is the order-zero jet input for the cubic Taylor program on the canonical remainder line. Downstream, iteratedDerivWithin_zero_canonicalRemainderLine quotes it to obtain that the $0$-th iterated derivative of $t\mapsto R_K(t\cdot\xi)$ on $[0,1]$ at $0$ is zero, the first of the jet conditions needed for a third-order remainder bound.
In the broader Recognition geometry stack, the Regge action and its Hessian encode discrete curvature on the triangulation; controlling the nonlinear remainder along rays is the analytic step that turns the identified canonical Hessian into a usable cubic Taylor theorem (the module's stated goal after nonlinear Hessian identification). It does not itself touch the forcing chain T0–T8, but sits in the discrete-geometry layer that supports continuum limits of recognition curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.