conformalLocalSqEdge_hasDerivAt_line_zero
plain-language theorem explainer
Along a linear ray of vertex potentials, the conformal rescaling of one squared edge length is differentiable at the origin, with derivative equal to the squared length times the sum of the endpoint potentials. First-variation calculations for the nonlinear Regge action under conformal deformations cite this edge-level fact. The proof is a short chain rule: differentiate the linear form in the exponent, compose with exp, and scale by the fixed squared edge length.
Claim. Let $K$ be a 3D triangulation, $\eta$ a real potential on its vertices, $\tau$ a tetrahedron of $K$, and $e$ one of the six edges of $\tau$. Write $\ell_e^2$ for the squared length of $e$ and $v_1,v_2$ for its endpoints. The scalar map $t\mapsto \ell_e^2\cdot\exp\bigl(t\eta(v_1)+t\eta(v_2)\bigr)$ is differentiable at $t=0$, and its derivative equals $\ell_e^2\cdot\bigl(\eta(v_1)+\eta(v_2)\bigr)$.
background
This module develops the analytic side of the first variation of the nonlinear Regge action on a 3D triangulation. The geometric target is vanishing of that variation at the flat conformal potential, via Schläfli cancellation plus zero deficit; the present file records the exact derivative statements needed before the full expansion from closed-form local Schläfli identities.
A vertex potential $\eta$ assigns a real number to each vertex. The line potential is the ray $t\mapsto t\eta$ through that assignment. Conformal rescaling of a local squared edge multiplies the bare squared length by the exponential of the sum of the potentials at the two endpoints. The named directional derivative is the candidate first-order coefficient of that rescaled length along the ray, evaluated at $t=0$.
Differentiability is the Mathlib HasDerivAt predicate: the difference quotient converges to the stated slope. The six edges of each tetrahedron are indexed by Fin 6, with endpoint pairs recovered from the fixed edge-vertex table of the Regge foundation.
proof idea
Unfold the conformal squared-edge map, the directional-derivative formula, and the line potential. Let $v_1,v_2$ be the endpoints of the chosen edge.
First, the linear map $t\mapsto t\eta(v_1)+t\eta(v_2)$ has derivative $\eta(v_1)+\eta(v_2)$ at $0$, by adding two constant multiples of the identity derivative.
Second, compose with $\exp$: Mathlib's Real.hasDerivAt_exp at the zero argument, chained with the linear step, yields derivative $\eta(v_1)+\eta(v_2)$ for $t\mapsto\exp(t\eta(v_1)+t\eta(v_2))$ at $0$ (using $\exp 0=1$).
Third, multiply by the constant bare squared edge length via const_mul, and tidy the multiplicative reassociations. The resulting slope is exactly the named directional derivative.
why it matters
Edge-level differentiability is the atomic analytic input for the first variation of the nonlinear Regge action under conformal deformations. The immediate parent is the tetrahedron-level lift: differentiability of the full six-edge squared-length tuple along the same ray, obtained by packaging this theorem under hasDerivAt_pi.
That tetrahedron statement feeds the module's target: 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; without a rigorous derivative of each conformally rescaled edge length, the analytic side of that cancellation cannot be stated.
In the broader Recognition geometry stack this sits under the discrete curvature and deficit calculus that eventually interfaces with the forcing chain's $D=3$ spatial claim (T8) and the eight-tick discrete time structure, though the present lemma itself is pure real analysis on a fixed triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.