actionAlongLine
plain-language theorem explainer
Restricts the nonlinear Regge action to the one-parameter family of vertex potentials along a conformal line through the flat configuration. Anyone proving second-variation or Hessian identities for discrete gravity on a 3D triangulation cites this restriction. The body is a one-line composition: evaluate the full Regge action on the line potential at scale t.
Claim. Given an incidence-consistent 3D triangulation $K$ and a vertex potential $\xi$, the action along the conformal line is the real function $t \mapsto S_{\mathrm{Regge}}(K,\,\phi_0 + t\xi)$, where $\phi_0$ is the flat (zero) potential and the line potential is the affine path through flat space in the direction $\xi$.
background
The module packages second-variation and cubic-remainder targets for the nonlinear Regge action in a form usable before the full Cayley-Menger/arccos chain-rule expansion is complete. Analytic hypotheses sit in named input structures rather than being proved inline.
A vertex potential assigns a real value to each vertex of the triangulation. The flat (zero) potential is the reference configuration. The line potential is the affine path that starts at that flat potential and scales a fixed direction $\xi$ by the real parameter $t$. The nonlinear Regge action $S_{\mathrm{Regge}}$ is the usual discrete Einstein-Hilbert functional built from hinge deficits and dual volumes on an incidence-consistent 3D complex.
The first-variation module supplies the underlying action and the line-potential construction; this definition only freezes the action onto that one-dimensional family so that ordinary real calculus (derivatives at $t=0$) can replace variational calculus on the full potential space.
proof idea
Pure definitional wrapper. The value at $t$ is exactly the nonlinear Regge action evaluated on the line potential at scale $t$. No lemmas are applied; the equality is by unfolding.
why it matters
Every nonlinear Hessian argument in the geometry stack factors through this restriction. Downstream, the canonical split decomposes the line action into the constant flat value plus a quadratic Hessian term plus a remainder; first-order tangency and near-zero linearization targets are stated as statements about the ordinary derivative of this real function of $t$; product-rule and $C^\infty$ smoothness-at-zero theorems likewise quantify over conformal lines via this map.
In the Recognition geometry program the second variation of the Regge action at the flat point is the discrete avatar of the linearized Einstein operator. Isolating the action on conformal lines converts that variational claim into ordinary one-variable calculus, which is what the Hessian-proof module then discharges (conditionally on the named analytic input structures). The module doc is explicit that the heavy Cayley-Menger/arccos expansion is still pending; this definition is the stable interface those expansions will plug into.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.