edgeSqrtDeriv
plain-language theorem explainer
Closed-form factor for the t-derivative of the square-root hinge on each periodic edge under a plane-wave edge field: L'_e(t) = c_e/(2√l_e(t)). Anyone assembling the first variation of the Regge action profile cites it as the explicit L' term. The body is a one-line quotient of the affine edge slope by twice the edge square root.
Claim. For a polarization $E$, wavevector $k$, periodic edge $e$, and amplitude $t$, define $$L'_e(t) := \frac{c_e}{2\sqrt{l_e(t)}},$$ where $c_e$ is the affine slope of the plane-wave edge value along $e$ and $l_e(t)$ is that edge value at amplitude $t$.
background
Module Gate A2 (Normalization-Gated Schläfli Two-Jet) studies the plane-wave action profile $S(t)$ of the true Regge action on the $N^3$ periodic lattice. Edge lengths deform affinely in the amplitude $t$: each periodic edge $e$ carries a value $l_e(t)$ (the plane-wave edge field) with constant slope $c_e$ (the edge coefficient built from $E$ and $k$).
The Regge hinge contribution involves $\sqrt{l_e}$. Differentiating that square root in $t$ produces the classical factor $l'_e/(2\sqrt{l_e})$. Because $l_e$ is affine, $l'_e=c_e$ is constant, so the factor collapses to the closed form $c_e/(2\sqrt{l_e(t)})$.
The first-derivative structure at flat is already locked in the upstream derivative gate; this definition only names the explicit $L'$ summand used when writing $S'(t)=\sum_e\bigl(L'_e\delta_e+\sqrt{l_e},\delta'_e\bigr)$.
proof idea
Pure definition: the right-hand side is the quotient of the in-module edge coefficient by twice the real square root of the plane-wave edge field at $(t,e)$. No tactic proof; downstream lemmas unfold this name and apply the chain rule for $\sqrt{\cdot}$ once positivity of the edge field is known.
why it matters
This is the explicit $L'_e$ factor in the profile derivative theorem: at every good amplitude, $S'(t)$ equals the first-variation integrand built from edgeSqrtDeriv and the deficit derivative. It feeds the integrand definition, the vanishing of that integrand at flat (Gate A2(a)), differentiability of the factor at $t=0$, matching to the flat slot sqrt-derivative, and the reduced first-variation derivative used for Gate A2(b).
Gate A2(b) rewrites the flat second variation as $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with no second derivative of $\arccos$; the pathwise Schläfli kill deletes the $\sqrt{l},\delta'$ group, so only products of this $L'$ against angle derivatives survive. In the QG continuum-symbol campaign this is the hinge half of the Schläfli-reduced two-jet at flat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.