hasDerivAt_edgeValue
plain-language theorem explainer
Every plane-wave edge length-squared on the periodic 3-torus is an affine function of the amplitude t, hence differentiable everywhere with constant derivative equal to its edge coefficient. Anyone building the first or second variation of the Regge TT action along a plane-wave path cites this. The proof rewrites the field as constant plus t times slope, then applies the product and sum rules for HasDerivAt.
Claim. For any polarization matrix $E:\mathbb{R}^3\to\mathbb{R}^3$, wavevector $k\in\mathbb{R}^3$, periodic edge $e$ on the $N$-torus, and amplitude $t_0\in\mathbb{R}$, the map $t\mapsto \ell_e(t)$ given by the plane-wave edge field is differentiable at $t_0$ with derivative equal to the edge coefficient $c_e(E,k)$.
background
This module sits in Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol for the Regge TT continuum symbol. The ambient setting is a plane-wave deformation of flat edge lengths on the periodic Freudenthal 3-torus: each edge value is a real-valued function of a single amplitude parameter $t$, built from a fixed polarization $E$ and wavevector $k$.
The plane-wave edge field is the squared length assigned to a periodic edge under that deformation. By construction it is affine in $t$: a background squared displacement (from periodicDispSqEdge) plus $t$ times an edge coefficient that packages the linear response of that edge. Differentiability of this affine profile is the first rung of the derivative ladder used later for square-root hinge factors, dihedral angles, and the full action profile.
Upstream geometry supplies the periodic edge type and the squared-displacement functional; the coefficient itself is the explicit slope extracted from the same plane-wave ansatz. No curvature or deficit data enters yet.
proof idea
Unfold the plane-wave edge field and the edge coefficient definitions; a short ring identity shows that the field equals the constant periodicDispSqEdge e.disp plus $t$ times edgeCoeff. Rewrite the target function by that equality. The derivative is then the standard calculus fact that $t\mapsto a + t\cdot c$ has derivative $c$ at every $t_0$, obtained from hasDerivAt_id, multiplication by the constant coefficient, and addition of the constant background term (mul_const, const_add), cleaned up with simpa.
why it matters
Gate A2 needs a closed-form first derivative of the Regge action profile along every good plane-wave path, and ultimately the Schläfli-reduced second variation at flat. The immediate parent is hasDerivAt_sqrtEdge, which differentiates the square-root hinge factor $\sqrt{\ell_e(t)}$ wherever the edge value is nonzero; that hinge derivative feeds edgeSqrtDeriv, the slot-angle and deficit derivatives, and finally hasDerivAt_planeWaveActionProfile.
Without a global, everywhere-valid derivative of the raw edge field, the pathwise Schläfli kill and the two Gate A2 claims (first variation vanishes at flat; second variation equals the explicit angle-Jacobian contraction with no arccos second derivatives) cannot even be stated. This lemma is pure calculus scaffolding inside the gravity analysis lane; it does not itself invoke Recognition forcing landmarks (T5–T8, RCL, $\phi$), but it is required infrastructure for the continuum TT symbol program those landmarks motivate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.