conformalLocalSqEdgeDirectionalDeriv
plain-language theorem explainer
Names the directional derivative of a local conformal squared-edge length along a one-parameter family of vertex potentials, evaluated at the flat (zero) potential. The value is the bare squared edge length times the sum of the potential values at the edge's two endpoints. Cited by the HasDerivAt lemmas that justify differentiating the conformal edge map, and by the local-angle chain-rule packages in the first-variation calculation. The body is a direct algebraic formula.
Claim. For a finite 3D triangulation $K$, a vertex conformal potential $\eta$, a tetrahedron index $\tau$, and an edge index $f\in\{0,\ldots,5\}$, the directional derivative of the local conformal squared-edge coordinate at the flat potential is $\ell_f^2(\tau)\,(\eta(v_1)+\eta(v_2))$, where $v_1,v_2$ are the two vertices of edge $f$ inside tetrahedron $\tau$ and $\ell_f^2(\tau)$ is that edge's squared length.
background
The 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 differentiate local edge and angle data along conformal deformations and feed those derivatives into the closed-form local Schläfli identities.
A vertex conformal potential on triangulation $K$ is a real assignment to each vertex (VertexPotential). The zero potential is the flat background. Edges of a reference tetrahedron are indexed by Fin 6, with endpoint pairs given by the standard map edge $0\mapsto(0,1)$, $1\mapsto(0,2)$, ..., $5\mapsto(2,3)$. Each tetrahedron of $K$ carries squared edge lengths sqEdge and a vertex lookup tetVerts.
Under a conformal deformation driven by $\eta$, squared edge lengths pick up a multiplicative factor built from the endpoint potentials. Differentiating that factor at the flat point yields exactly the linear form $\ell_f^2(\eta(v_1)+\eta(v_2))$ recorded here.
proof idea
Pure definitional abbreviation. Resolve the two endpoints of edge $f$ via the fixed tetrahedron edge-to-vertex table, then return the product of the tetrahedron's bare squared edge length with the sum of $\eta$ at those two vertices. No lemmas or tactics; the formula is the content.
why it matters
This scalar is the derivative value plugged into every local first-variation identity in the module. Immediately downstream, conformalLocalSqEdge_hasDerivAt_line_zero proves that the conformal squared-edge map along the line potential $t\mapsto t\eta$ has derivative equal to this quantity at $t=0$; the pi-version lifts that to all six edges of a tetrahedron. The same quantity is the edge factor inside localAngleSqEdgeChainDeriv, which contracts dihedral closed derivatives against these directional edge derivatives, and it appears in the flat-configuration chain-rule package that packages angle differentiability for the global first-variation argument.
In the broader Recognition geometry stack this is bookkeeping for the analytic half of Schläfli cancellation: once edge and angle derivatives are under control at the flat conformal potential, the first variation of the nonlinear Regge action vanishes by zero deficit. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is local 3D Regge calculus infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.