sum_sqrt_deficitDeriv_eq_zero
plain-language theorem explainer
Along any plane-wave edge family that stays good (positive lengths, nondegenerate tets, interior dihedral cosines), the weighted sum of deficit derivatives Σ_e √ℓ_e(t) δ'_e(t) vanishes identically. Anyone computing the first or second variation of the true Regge action on the TT continuum symbol cites this to delete the entire Schläfli group. The proof rewrites the sum as a double sum over tets and slots, then applies the closed-form tetrahedral Schläfli identity per cell.
Claim. Let $E:\{0,1,2\}^2\to\mathbb{R}$ and $k:\{0,1,2\}\to\mathbb{R}$. Fix $t\in\mathbb{R}$ such that every plane-wave edge length is positive and every periodic tetrahedron is nondegenerate with strictly interior dihedral cosines. Then $\sum_e \sqrt{\ell_e(t)}\,\delta'_e(t)=0$, where the sum runs over all periodic edges, $\ell_e(t)$ is the plane-wave edge field, and $\delta'_e(t)$ is the $t$-derivative of the angle deficit at edge $e$.
background
This module sits in the QG full-theory campaign, Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol. The true Regge action along a plane-wave family is $S(t)=\sum_e\sqrt{\ell_e(t)},\delta_e(t)$. Differentiating produces two groups: one with $\ell'_e\delta_e$ and one with $\sqrt{\ell_e}\delta'_e$. The second group is the object killed here.
PathGoodAt packages the open conditions needed for all derivatives to exist in closed form: every edge value of the plane-wave field is positive, every tet has positive Cayley-Menger volume, and every dihedral cosine lies in $(-1,1)$. Under that hypothesis the deficit derivative expands as a signed sum of slot-angle derivatives over incident tets, via the incidence map canonicalEdgeSlot?.
The local geometry is the periodic Freudenthal triangulation of the $N\times N\times N$ torus: each tet has six local edge slots, and localEdgeOf chooses the corresponding global edge. The regrouping bijection sum_edges_slotMatch converts an edge-sum of matched contributions into a pure slot-sum over those six edges.
proof idea
First, for each edge $e$, unfold deficitDeriv and push the factor $\sqrt{\ell_e}$ through the negative tet-sum, using mul_neg, Finset.mul_sum, and the match-identity slotMatch_mul. The global sum therefore equals $-\sum_e\sum_\tau$ of the matched slot contributions.
Commute the two finite sums (Finset.sum_comm), then replace the inner edge-sum by a pure six-slot sum via sum_edges_slotMatch. The expression collapses to $-\sum_\tau\sum_{f:0\ldots5}\sqrt{\ell_{\mathrm{local}(\tau,f)}},\partial_t\theta_{\tau f}$.
Each inner tet sum vanishes by the already-proved identity sum_sqrt_slotAngleDeriv_eq_zero (the closed-form tetrahedral Schläfli contraction at a nondegenerate path point), whose positivity/interior-cosine hypotheses are exactly the second conjunct of PathGoodAt. Negating zero finishes the proof.
why it matters
This is the pathwise Schläfli kill named in the module doc: it removes every arccos second derivative from the second variation of the true Regge action. Downstream, firstVariationIntegrand_eq_reduced rewrites the full first-variation integrand as the reduced (deficit-group-only) form by adding this identity and cancelling the second summand. firstVariationIntegrand_zero then obtains vanishing at flat by combining the Stage-1 kernel theorem (flat deficits vanish) with this kill at $t=0$.
Together those feed Gate A2(a) (trueReggeAction_firstVariation_flat_eq_zero) and Gate A2(b) (the Schläfli-reduced second variation formula). In the broader Recognition gravity lane this is the algebraic step that lets the continuum TT symbol be read off from first derivatives of lengths and angles alone, without residual curvature of the inverse-cosine chart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.