hasDerivAt_reducedFirstVariation_flat
plain-language theorem explainer
At the flat background the reduced first variation of the plane-wave Regge action is differentiable, and its derivative equals the edge sum of edge-length-sqrt speed times deficit speed. Only that product-rule term survives because every flat deficit vanishes. Gate A2(b) cites this to identify the Schläfli-reduced second variation without arccos second derivatives. The proof is a finite product-rule sum plus the flat-deficit identity.
Claim. For any edge-amplitude matrix $E:\{0,1,2\}^2\to\mathbb{R}$ and wavevector $k\in\mathbb{R}^3$, the reduced first variation $t\mapsto\sum_e L'_e(t)\,\delta_e(t)$ (edge sum of length-sqrt speed times deficit along the plane-wave path) is differentiable at the flat point $t=0$, with derivative $\sum_e L'_e(0)\,\delta'_e(0)$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign. It studies the true Regge action along a plane-wave edge-length path $t\mapsto$ planeWaveEdgeField$(E,k,t)$ on the periodic lattice of period $N$, and reduces the second variation at flat by killing every arccos second derivative.
The full first variation splits as $\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\delta_e+\sqrt{l_e},\delta'_e\bigr]$. Pathwise Schläfli kill shows the second group vanishes identically on a neighborhood of good amplitudes (via the closed tetrahedral Schläfli identity). What remains is the reduced first variation: the deficit group alone, written here as the edge sum of edgeSqrtDeriv times the field deficit.
At $t=0$ the configuration is flat, so every edge deficit vanishes (Stage-1 kernel / deficit_planeWave_zero). Differentiating the reduced first variation at that point is therefore a pure product-rule computation with one vanishing factor. Upstream derivative infrastructure (hasDerivAt_deficit, edgeSqrtDeriv_differentiableAt, pathGoodAt_zero) is reused from the derivative-gate module and never re-proved.
proof idea
For each periodic edge $e$, form the scalar product $t\mapsto$ edgeSqrtDeriv$(e,t)\cdot$deficitOfField(planeWave path at $t$, $e$). Differentiability of the first factor at $0$ comes from edgeSqrtDeriv_differentiableAt.hasDerivAt; the second factor from hasDerivAt_deficit at amplitude $0$ under pathGoodAt_zero. The product rule yields two terms. Flatness deficit_planeWave_zero sets the deficit factor to $0$ at $t=0$, so mul_zero and zero_add erase the term that would involve the derivative of edgeSqrtDeriv, leaving only edgeSqrtDeriv$(e,0)\cdot$deficitDeriv$(e,0)$.
HasDerivAt.fun_sum lifts the pointwise statement over the finite set of all periodic edges. Unfolding reducedFirstVariation identifies that sum with the claimed derivative.
why it matters
This is the analytic hinge between Gate A2(a) (first variation vanishes at flat) and the Gate A2(b) headline trueReggeAction_secondVariation_flat_schlaefli. That parent theorem rewrites $S''(0)$ as $-\sum_\tau\sum_f L'{\tau f}(0)\cdot\theta'{\tau f}(0)$ with $L'$ the flat slot length-sqrt speed and $\theta'$ the flat angle-Jacobian contraction from the derivative gate.
Because the reduced first variation already equals $S'$ near flat (pathwise Schläfli kill), differentiating it at $0$ and using $\delta_e(0)=0$ produces exactly the displayed contraction. No second derivative of arccos enters, so the explicit-$G$ Hessian stage is deleted from the critical path of the continuum-symbol program. In the broader RS gravity lane this is pure discrete GR analysis on the eight-tick / $D=3$ lattice scaffolding; it does not itself invoke the $J$-cost or $\phi$-ladder mass formula, but it clears the second-variation kernel needed for TT symbol existence downstream of Gates A0–A1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.