edgeSqrtDeriv_localEdge_zero
plain-language theorem explainer
At the flat background, the square-root edge-length derivative along a plane-wave path, evaluated on a tetrahedron's matched local edge, equals the corresponding flat slot derivative. Anyone regrouping edge-sum first-variation terms into tet-slot form cites this identification. The proof unfolds both sides, kills the linear plane-wave shift at amplitude zero, and rewrites via the Freudenthal local-edge square-length match.
Claim. Fix plane-wave data $E:\{0,1,2\}^2\to\mathbb{R}$, wavevector $k$, a periodic tetrahedron $\tau$, and a slot index $f\in\{0,\ldots,5\}$. Then the edge square-root derivative at amplitude $t=0$ on the local edge of $\tau$ corresponding to slot $f$ equals the flat slot square-root derivative of $(\tau,f)$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign. The object of study is the plane-wave action profile $S(t)$ on a periodic 3-torus triangulation: edge lengths are deformed by a plane-wave displacement field with amplitude $t$, and $S$ is the true Regge action (edge lengths times angle deficits).
The first derivative of $S$ splits into two groups, $\sum_e (\ell'_e/(2\sqrt{\ell_e}))\delta_e + \sum_e \sqrt{\ell_e},\delta'e$. The coefficient $\ell'e/(2\sqrt{\ell_e})$ is packaged as the edge square-root derivative. On a tetrahedron, each of the six local edges is a slot; the flat-background specialization of that coefficient on slot $f$ is the flat slot square-root derivative $L'{\tau f}(0)=v{\tau f}/(2\sqrt{a^*_f})$.
Matching a global periodic edge to a tet slot uses the local-edge map of the Freudenthal tetrahedron. The first-derivative gate already supplies closed forms for edge and angle derivatives; this lemma only identifies the two presentations of the square-root factor at $t=0$.
proof idea
Term-mode proof by definition chase. Unfold the edge square-root derivative, the flat slot square-root derivative, the edge coefficient, and the plane-wave tet velocity. Simplify with the plane-wave edge field at amplitude zero: the linear shift term vanishes by zero_mul and add_zero, so both sides reduce to the same algebraic expression in the squared edge lengths. Finish by rewriting the periodic displacement squared length of the matched local edge into the Freudenthal tet squared-edge table via the already-proved identity that those two squared lengths agree (applied symmetrically).
why it matters
Parent consumer is sum_edgeSqrtDeriv_deficitDeriv_flat: the deficit-group first variation at flat, $\sum_e L'e(0),\delta'e(0)$, is rewritten as $-\sum\tau\sum_f L'{\tau f}(0),\theta'_{\tau f}(0)$. That regrouping needs exactly this pointwise equality so every edge-side $L'_e(0)$ on a matched local edge can be replaced by the flat slot factor.
Downstream that identity feeds Gate A2(b): the second variation of the plane-wave Regge action at flat collapses to $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$, with no second derivatives of $\arccos$. Together with the pathwise Schläfli kill and the Stage-1 kernel (flat deficits vanish), this closes the first-variation vanishing at flat (Gate A2(a)) and the Schläfli-reduced two-jet formula. In the broader RS gravity lane this is continuum-symbol bookkeeping on the discrete action, not a new forcing-chain step (T5–T8 stay upstream).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.