reggeActionRemainder_zero
plain-language theorem explainer
The nonlinear Taylor remainder of the 3D Regge action vanishes at the flat (zero) vertex potential, for every candidate Hessian. Anyone assembling the cubic Taylor bound or the local Hessian interface for finite Regge triangulations cites this. The proof unfolds the remainder, applies vanishing of the quadratic form at zero, and closes by ring arithmetic.
Claim. Let $K$ be an incidence-consistent finite 3D triangulation and let $H$ be any candidate Hessian on vertex pairs. Writing $R_K(H,\xi)$ for the nonlinear remainder of the Regge action after subtracting its value at the flat configuration and the quadratic term $\tfrac12 H(\xi,\xi)$, one has $R_K(H,0)=0$ at the zero vertex potential.
background
This module isolates the final analytic Hessian step for a finite 3D Regge triangulation: a concrete action under the conformal ansatz, its second variation, and the bridge into the existing Regge-Hessian data interface.
The remainder is defined by subtracting from the full Regge action both its value at the flat configuration and a candidate quadratic form: $R_K(H,\xi)=S_K(\xi)-S_K(0)-\tfrac12,Q_H(\xi)$. The zero (flat) vertex potential is the configuration with vanishing conformal edge deformations. The companion lemma hessianQuadratic_zeroPotential states that this quadratic form itself evaluates to zero at that flat point, for every matrix $H$.
Incidence consistency of $K$ is the structural hypothesis that makes the discrete deficit angles and hinge measures well-defined on the triangulation, so the action and its remainder are meaningful.
proof idea
Unfold the remainder definition. At the zero potential the two Regge-action terms cancel, leaving $-\tfrac12,Q_H(0)$. Rewrite that quadratic term via the sibling lemma that $Q_H$ vanishes at the flat potential, then finish with ring arithmetic to obtain zero. No triangulation geometry beyond the already-proved quadratic vanishing is used.
why it matters
This is the base-point identity for the nonlinear remainder jet. Downstream, the cubic Taylor bound module uses it to show that the canonical remainder along the line potential vanishes at parameter zero, and to assemble the local Hessian Taylor input package from an eventually-zero edge stencil plus a remainder jet target. Without $R(0)=0$, the second-order truncation would not sit cleanly inside the Regge-Hessian interface that the module is built to feed. In the broader Recognition geometry stack this is bookkeeping for the discrete curvature action, not a forcing-chain step (T5–T8), but it is required before any claim that the quadratic Hessian controls the action near flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.