trueReggeAction_firstVariation_flat_eq_zero
plain-language theorem explainer
At the flat background, the first derivative of the plane-wave Regge action profile vanishes for every polarization matrix and wavevector. Gravity analysts in the Regge TT continuum-symbol program cite this as Gate A2(a) of the Normalization-Gated Schläfli Two-Jet protocol. The proof is a short term argument: differentiability at amplitude zero identifies the derivative with the first-variation integrand, which is zero at flat by vanishing deficits plus the pathwise Schläfli identity.
Claim. For every real $3\times 3$ polarization matrix $E$ and every wavevector $k\in\mathbb{R}^3$, the derivative of the plane-wave Regge action profile at amplitude zero vanishes: $\frac{d}{dt}\big|_{t=0} S_{N,E,k}(t)=0$.
background
This module sits in the QG full-theory campaign under the Regge TT continuum-symbol program (Crux-1(c), Gate A2 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol). Gate A0 audits the symbol specification; Gate A1 gives local symbol existence; the first-derivative structure at flat is already proved in the derivative-gate module and is reused, not re-proved.
The plane-wave action profile is the true Regge action evaluated along a one-parameter family that deforms edge lengths by a plane-wave polarization $E$ with wavevector $k$. A path amplitude $t$ is "good" when every edge length is positive and every tetrahedron is nondegenerate with interior face cosines. At every good $t$, the profile derivative equals the first-variation integrand $\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\delta_e+\sqrt{l_e},\delta'_e\bigr]$, with each primed factor in closed form.
Upstream, the flat amplitude $t=0$ is good (edge values are positive displacement classes; every tet is the Freudenthal tet with $c_{m3}=8>0$). The first-variation integrand itself vanishes at flat: the deficit group dies by the Stage-1 kernel theorem (flat deficits are zero), and the Schläfli group dies by the pathwise kill that regroups per tetrahedron and applies the closed-form six-edge Schläfli identity.
proof idea
Three-line term proof. First apply the profile-derivative theorem at $t_0=0$, feeding the flat-path-goodness lemma, to obtain HasDerivAt of the plane-wave action profile with derivative equal to the first-variation integrand at zero. Rewrite the ordinary deriv via the HasDerivAt.deriv identity. Conclude by the sibling theorem that the first-variation integrand vanishes at the flat point (deficit group zero by flat deficits; Schläfli group zero by the pathwise kill).
why it matters
Gate A2(a) is the first half of the Schläfli-reduced two-jet at flat: it clears the linear term so that the continuum symbol is controlled by the second variation alone. The module immediately continues to Gate A2(b), which identifies the second derivative at zero with a pure first-jet expression $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ involving only flat slot sqrt-edge derivatives and the flat angle Jacobian; no second derivative of $\arccos$ survives, because the pathwise Schläfli kill already deleted that sector from $S'$ near zero.
In the broader Recognition gravity stack this is continuum-symbol hygiene for the Regge TT sector on the periodic lattice, not a direct citation of the T0–T8 forcing chain. It closes the first-variation half of Crux-1(c) so that subsequent symbol and positivity arguments can work entirely with the Schläfli-reduced quadratic form. No downstream consumers are wired yet in the graph; the natural parent is the A2(b) second-variation theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.