ActionLineDifferentiabilityTarget
plain-language theorem explainer
Packages the demand that the nonlinear Regge action, restricted to any conformal line through the flat potential on an incidence-consistent 3D triangulation, is differentiable at every real parameter. Downstream remainder-line and second-variation lemmas cite this Prop as a named hypothesis. Body is a pure universal quantification of DifferentiableAt; no proof content.
Claim. For every incidence-consistent finite 3D triangulation $K$ and every vertex conformal potential $\xi$, the real map $t \mapsto S_{\mathrm{Regge}}(K,\,\phi_0 + t\xi)$ (nonlinear Regge action along the conformal line through the flat potential) is differentiable at every $t \in \mathbb{R}$.
background
The ambient module isolates the hard endpoint of the nonlinear Regge Hessian calculation: the second directional derivative of the full nonlinear action at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input structure follows at once.
A Triangulation3D is a finite abstract 3D Regge complex (vertex, edge, tetrahedron counts plus incidence and nondegenerate squared-edge data). IncidenceConsistent strengthens that scaffold with global squared-edge lengths, local-to-global edge agreement up to orientation, and a local closed-form Schläfli certificate. Vertex conformal potentials are maps from vertices to reals; the zero potential is the flat background.
actionAlongLine restricts the nonlinear Regge action to the one-parameter family obtained by adding $t\xi$ to the flat potential. The present definition simply names the statement that this real function of $t$ is differentiable everywhere.
proof idea
Definitional packaging only: the body is the Prop $\forall,\xi,,t.;\mathrm{DifferentiableAt},\mathbb{R},(\mathrm{actionAlongLine},K,hK,\xi),t$. No tactics, no lemmas applied. Downstream theorems treat the name as a hypothesis and discharge concrete goals by specializing it.
why it matters
In the nonlinear Hessian proof interface this target is the differentiability half of the remainder analysis. canonicalRemainderLineDifferentiability_of_actionLineDifferentiability lifts it, together with automatic differentiability of the canonical quadratic along the line, to differentiability of the canonical remainder. That remainder package then feeds canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_actionLineDiff, which combines the present target with the nonlinear directional Hessian theorem to conclude that the second variation of the remainder vanishes at the flat point.
Thus the definition is the named gate between "action is differentiable on lines" and the chain-rule endpoint that the module doc identifies as discharging ReggeActionSecondVariationInput. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete-geometry scaffolding for the Regge side of the RS geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.