firstVariationIntegrand_eq_reduced
plain-language theorem explainer
At every good amplitude, the full first-variation integrand of the plane-wave Regge action equals the reduced form that keeps only the deficit-weighted edge-length derivatives. Gate A2 authors cite this to drop the Schläfli group before differentiating again at flat. The proof unfolds both sides, splits the edge sum, and kills the second group by the pathwise Schläfli identity.
Claim. Fix amplitudes $E:\mathrm{Fin}\,3\to\mathrm{Fin}\,3\to\mathbb{R}$, wavevectors $k$, and a time $t$ at which the path is good: every edge length is positive and every tetrahedron is nondegenerate with strictly interior dihedral cosines. Then the full first-variation integrand equals the reduced first variation (the deficit-group-only form).
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The plane-wave action profile $S(t)$ is differentiated along a path of edge lengths; at every good amplitude one has $$S'(t)=\sum_e\Bigl(\frac{l'_e}{2\sqrt{l_e}}\delta_e+\sqrt{l_e},\delta'_e\Bigr)$$ with every primed object in closed form.
PathGoodAt packages the open set where that formula is valid: positive edge values, positive Cayley-Menger volume, and dihedral cosines strictly in $(-1,1)$. The second summand group is the pathwise Schläfli contribution. Upstream, sum_sqrt_deficitDeriv_eq_zero shows it vanishes identically on the good set by regrouping per tetrahedron and applying the closed-form six-edge Schläfli identity. The reduced first variation is what remains after that kill.
proof idea
Term-mode identity proof. Unfold both firstVariationIntegrand and reducedFirstVariation to expose the two-group edge sum versus the single (deficit-weighted) group. Apply Finset.sum_add_distrib to split the full sum, then rewrite the second group to zero by sum_sqrt_deficitDeriv_eq_zero at the given good amplitude, and finish with add_zero.
why it matters
This is the algebraic bridge from the full first-variation formula to the Schläfli-reduced integrand used throughout Gate A2. Downstream, deriv_actionProfile_eventuallyEq_reduced lifts the pointwise equality to an eventual equality of deriv S with the reduced first variation on a neighborhood of flat, via hasDerivAt_planeWaveActionProfile and eventually_pathGoodAt.
That neighborhood agreement is what lets Gate A2(a) conclude $S'(0)=0$ and Gate A2(b) compute the second variation at flat as $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with no second derivative of $\arccos$ anywhere. It is the concrete realization of the module's pathwise Schläfli kill: the second group dies identically near zero, not only at the flat point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.