reggeAction_along_line_hasDerivAt_fderiv
plain-language theorem explainer
Along any straight line of conformal vertex potentials through the flat background, the nonlinear 3D Regge action is differentiable at t = 0, and that ordinary derivative equals the Fréchet derivative of the action at the zero potential applied to the direction. Anyone proving the first-variation formula from a directional formula cites this. The proof is the chain rule: Fréchet differentiability at flat plus the elementary derivative of the line map.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat under the vertex-conformal ansatz, and let $\eta$ be any vertex potential. Then the real function $t \mapsto S_K(t\eta)$ is differentiable at $t = 0$, and its derivative equals $DS_K(0)[\eta]$, the Fréchet derivative of the Regge action at the zero potential in the direction $\eta$.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is to make the directional derivative along conformal lines rigorous before expanding the closed-form local identities.
The concrete action is $S_K(\xi) = \sum_e \ell_e(\xi),\delta_e(\xi)$: hinge measure times deficit angle under the vertex-conformal ansatz. The line through the flat background is $\mathrm{linePotential}(K,\eta,t) = t\eta$, so at $t = 0$ one recovers the zero potential. Flatness supplies continuous differentiability of $S_K$ at zero, hence a Fréchet derivative there.
Upstream, linePotential_hasDerivAt_zero gives $\frac{d}{dt}|_{0}(t\eta) = \eta$ in the product topology on vertex potentials, and linePotential_zero identifies the base point of the line with the zero section.
proof idea
From flatness, $S_K$ is continuously differentiable at the zero potential, so it is differentiable there and admits a Fréchet derivative $DS_K(0)$. Rewrite the base point as $\mathrm{linePotential}(K,\eta,0)$ via the zero-line identity. Compose that Fréchet derivative with the ordinary derivative of $t \mapsto t\eta$ at $0$ (which is $\eta$) by HasFDerivAt.comp_hasDerivAt. A final simpa clears the composition and the zero-line rewrite, yielding the claimed HasDerivAt at $t = 0$.
why it matters
This is the analytic bridge from Fréchet calculus on the space of vertex potentials to ordinary one-variable derivatives along conformal rays. The sole downstream consumer is firstVariationFormula_of_directionalFormula, which assembles a full first-variation formula once a directional formula is supplied. Without this identification, criticality of the flat potential (the module's target: first variation vanishes at flat) cannot be stated as an ordinary derivative of $t \mapsto S_K(t\eta)$. In the broader Recognition geometry stack it sits under the 3D triangulation and Schläfli infrastructure that supports discrete curvature balance, feeding the same conformal ansatz used for deficit and hinge measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.