conformalTetSqEdges_hasDerivAt_line_zero
plain-language theorem explainer
Along the straight line of conformal vertex potentials through the flat background in direction η, the six squared-edge coordinates of any tetrahedron are differentiable at t = 0. The derivative is the explicit map sending each local edge index to the corresponding directional derivative of that squared length. First-variation and chain-rule packages for the nonlinear Regge action cite this fact. The proof is a one-line pi-component reduction to the already-proved single-edge derivative.
Claim. Let $K$ be a 3D triangulation and $\eta$ a real potential on its vertices. For every tetrahedron $\tau$, the map $t \mapsto$ (the six conformally scaled squared edge lengths of $\tau$ at the potential $t\eta$) is differentiable at $t=0$, with derivative equal to the six-tuple of directional derivatives of those squared lengths at the flat potential.
background
This module develops the analytic first variation of the nonlinear Regge action on a 3D triangulation. The geometric target is vanishing of that variation at a flat conformal background, via Schläfli cancellation plus zero deficit; the present lemmas supply the exact differentiability statements needed before the closed-form local Schläfli identities are fully expanded.
A vertex potential is a real function on the vertices of $K$. The line potential through the flat background in direction $\eta$ is the ray $t \mapsto t\eta$. Under the conformal ansatz, each tetrahedron $\tau$ carries six squared-edge coordinates obtained by scaling the background squared lengths by the endpoint potentials; packaging those six values yields the Cayley–Menger squared-edge vector of $\tau$.
The directional derivative of a single local squared edge at the flat point is already known: it equals the background squared length times the sum of the two endpoint values of $\eta$. The single-edge theorem asserts that each component map $t \mapsto$ (that squared edge along the line potential) has that directional derivative at $t=0$.
proof idea
The squared-edge vector is the product (over the six local edge indices) of the individual conformal squared-edge maps. Differentiability of a product map at a point is equivalent to componentwise differentiability, via the Mathlib identity hasDerivAt_pi. After rewriting with that identity, the goal reduces to one real derivative per edge index $f$. Each component is discharged by the already-proved single-edge theorem conformalLocalSqEdge_hasDerivAt_line_zero. No further calculus is performed here.
why it matters
First variation of the Regge action requires differentiating dihedral angles and hinge measures with respect to the conformal edge lengths. Those chain-rule steps need the squared-edge vector itself to be differentiable along the line of potentials. This theorem packages the six component derivatives into a single HasDerivAt fact for the tetrahedron.
It is consumed directly by localAngleSqEdgeChainRulePackage_of_flat, which assembles the local angle–edge chain-rule data at a flat configuration. That package is part of the analytic scaffolding toward the module target: vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential (Schläfli cancellation plus zero deficit). In the broader Recognition geometry stack this sits under the discrete curvature and action calculus that eventually interfaces with the eight-tick and $D=3$ forcing landmarks, though the present lemma is purely local differential geometry on one tetrahedron.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.