actionLineDifferentiabilityNearZero_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation that is flat, the nonlinear Regge action restricted to every conformal line through the flat potential is differentiable on a neighborhood of the origin. Anyone assembling the second-variation identity for the nonlinear Hessian cites this. The proof is a one-line transfer from C^∞ at zero to eventual differentiability nearby.
Claim. Let $K$ be an incidence-consistent 3D triangulation that admits a flat configuration. Then for every vertex potential $\xi$, the scalar map $t \mapsto S_K(\phi_0 + t\xi)$ (nonlinear Regge action along the conformal line) is differentiable at all $t$ in some neighborhood of $0$.
background
The module isolates the hard endpoint of the nonlinear Regge second-variation calculation: the second directional derivative of the full nonlinear action at a flat potential must recover the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
actionAlongLine is the nonlinear Regge action restricted to a one-dimensional conformal line through the flat potential: $t \mapsto \mathrm{reggeAction}(K,\phi_0+t\xi)$. A flat configuration means the background edge lengths realize vanishing deficit angles (zero curvature) on the triangulation.
The target proposition asserts that, for every direction $\xi$, differentiability of this line map holds eventually in a neighborhood of $t=0$. Upstream, the same flat hypothesis already yields $C^\infty$ of the line map at the origin; a general real-analysis lemma then converts infinite differentiability at a point into eventual differentiability nearby.
proof idea
Term-mode one-liner. Fix an arbitrary vertex potential $\xi$. Apply differentiableAt_eventually_of_contDiffAt_top to $f = \mathrm{actionAlongLine}(K,hK,\xi)$ at $x=0$, feeding the already-proved fact that $f$ is $C^\infty$ at $0$ under the flat-configuration hypothesis (actionAlongLine_contDiffAt_zero_of_flatConfiguration). That general lemma extracts a neighborhood on which $f$ is differentiable by restricting the $C^\infty$ germ to order $1$ and using the resulting $C^1$ chart.
why it matters
This is a small but necessary regularity gate on the path to the nonlinear Hessian identity. Downstream, canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration consumes exactly this target (via the intermediate that packages nonlinear Hessian plus line differentiability near zero) to conclude that the canonical remainder has vanishing second variation at the flat point.
In the Recognition geometry stack, the Regge action is the discrete curvature functional whose second variation at flat space must match the incidence Hessian; that match is the discrete avatar of linearized gravity on the triangulation. The module doc frames the whole file as the endpoint of the second chain-rule calculation, not a new physical assumption. Without eventual differentiability of every action line near zero, the second-derivative comparison cannot even be stated pointwise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.