canonicalRemainderAlongLine
plain-language theorem explainer
Canonical nonlinear Regge-action remainder restricted to a conformal line through the flat potential in direction ξ. Anyone proving the nonlinear directional Hessian equals the incidence Hessian cites this one-dimensional remainder. The body simply evaluates the bulk remainder at the line potential for parameter t, relative to the canonical Hessian.
Claim. For an incidence-consistent 3D triangulation $K$, vertex potential $\xi$, and $t\in\mathbb{R}$, let $R_K(\xi,t)$ be the Regge-action remainder of $K$ relative to the canonical incidence Hessian, evaluated at the conformal line potential $t\cdot\xi$.
background
This module isolates the last hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The bulk remainder subtracts the quadratic form built from the canonical Hessian from the nonlinear Regge action. A conformal line is the one-parameter family of vertex potentials $t\mapsto t\cdot\xi$ through the zero (flat) potential. Restricting the remainder to that line yields a real function of $t$ whose second derivative at $0$ is the only remaining analytic content after the algebraic split.
Upstream, the remainder and the canonical Hessian come from the second-variation geometry layer; the line potential is the standard ray in the space of vertex potentials on an incidence-consistent triangulation.
proof idea
Pure definitional specialization: feed the triangulation, its incidence hypothesis, the canonical Regge Hessian, and the line potential at $(K,\xi,t)$ into the bulk remainder functional. No tactics, no lemmas, no rewriting.
why it matters
This is the algebraic reduction point for the nonlinear Hessian proof. Downstream, actionAlongLine_canonical_split writes the action along every conformal line as constant plus canonical quadratic plus this remainder; after that split, "the only remaining analytic content is the second variation of the canonical remainder."
The explicit subtraction form and the derivative-identity targets are phrased directly in terms of this line remainder. Closing those identities, together with the directional Hessian theorem, yields vanishing second variation of the remainder, which is exactly the reduction of the nonlinear Hessian problem to a remainder calculation. In the broader RS geometry chain this is the 1D gate between discrete curvature (Regge) and the continuum Hessian match at flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.