ActionLineDifferentiabilityNearZeroTarget
plain-language theorem explainer
Names the local differentiability target for the nonlinear Regge action along every conformal line through the flat potential: near t = 0 the restricted action is differentiable. Downstream Hessian and remainder lemmas cite this Prop as a hypothesis interface. The body is a pure Prop abbreviation, not a proof.
Claim. For a finite 3D triangulation $K$ with incidence consistency, the following holds: for every vertex conformal potential $\xi$, the map $t \mapsto S_K(\text{flat} + t\xi)$ (nonlinear Regge action along the conformal line) is differentiable at all $t$ in some neighborhood of $0$.
background
The module isolates the remaining hard step for the full nonlinear Regge Hessian: the second directional derivative of the Regge action 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.
A Triangulation3D carries finite vertex/edge/tet counts and abstract incidence; IncidenceConsistent strengthens this with global squared-edge data, local-to-global edge agreement, and a closed-form local Schläfli field. Vertex conformal potentials are maps Fin nV → ℝ. The one-parameter restriction actionAlongLine K hK ξ t is the nonlinear Regge action evaluated on the conformal line through the flat potential in direction ξ.
This declaration does not assert the property; it packages it as a named Prop so later theorems can assume or discharge local differentiability near zero without repeating the quantifiers.
proof idea
Definitional: the body is the Prop
$\forall \xi,; \forall^{\mathrm{f}} t \in \mathcal{N}(0),; \mathrm{DifferentiableAt},(\mathrm{actionAlongLine},K,hK,\xi),t$.
No tactics or lemmas are applied. Discharge sites (e.g. under a flat configuration) later invoke smoothness-to-eventual-differentiability helpers such as differentiableAt_eventually_of_contDiffAt_top.
why it matters
This target sits on the nonlinear Hessian proof path. It is assumed by the transfer lemma that upgrades action-line differentiability to canonical-remainder-line differentiability near zero, and by the combination lemma that, together with the nonlinear directional Hessian theorem, yields vanishing second variation of the canonical remainder.
A sibling theorem already closes the target under a flat configuration hypothesis, so the interface is not left open in the flat case. In the broader Recognition geometry stack this is scaffolding for matching the second variation of the nonlinear Regge action to the incidence Hessian (the endpoint of the second chain-rule calculation flagged in the module doc), not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.