actionAlongLine_canonical_split
plain-language theorem explainer
Along every conformal line through the flat potential, the nonlinear Regge action splits exactly into its value at zero, the canonical quadratic piece, and a canonical remainder. Cited by anyone reducing the nonlinear directional Hessian to a remainder calculation. Proof is pointwise: unfold the three line maps and apply the Regge Taylor decomposition.
Claim. For every incidence-consistent 3D triangulation $K$ and every vertex potential $\xi$, the restriction of the nonlinear Regge action to the conformal line through the zero potential in direction $\xi$ equals, as a function of the line parameter $t\in\mathbb{R}$, the sum of the action at the zero potential, the canonical quadratic contribution along that line, and the canonical remainder along that line.
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that chain-rule calculation is in hand, the existing second-variation input package follows at once.
In this discrete setting, a 3D triangulation carries vertex potentials; the zero potential is the flat reference configuration. A conformal line is the one-parameter family of potentials obtained by scaling a fixed direction $\xi$ by a real parameter $t$. The Regge action along that line is an ordinary real function of $t$.
The canonical Regge Hessian is the quadratic form fixed by the linearized incidence geometry. Upstream, a Taylor decomposition writes the full nonlinear action as value at zero plus that quadratic piece plus a remainder. Restricting the decomposition to a conformal line yields the exact one-dimensional split used by the Hessian argument.
proof idea
Term-mode packaging, not a new calculation. Apply function extensionality in the line parameter $t$. Unfold the three definitions (action along the line, canonical quadratic along the line, canonical remainder along the line). Feed the line potential at $t$ into the existing Regge Taylor decomposition at the canonical Regge Hessian, and finish with simpa. The identity is purely algebraic once the Taylor split is available.
why it matters
Direct input to nonlinearDirectionalHessian_of_remainder_identically_zero, which concludes the nonlinear directional Hessian theorem as soon as the canonical remainder vanishes identically on every vertex potential. The doc-comment states the role cleanly: after this split, the only remaining analytic content is the second variation of the canonical remainder. That is exactly the endpoint the module is built to expose. In the broader Recognition geometry layer this bookkeeping sits under the discrete-curvature side of the D=3 forcing story, but the lemma itself makes no continuum or forcing claim; it is the algebraic cut that lets the Hessian proof finish once the remainder's second derivative is controlled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.