firstVariationIntegrand_zero
plain-language theorem explainer
At the flat background the first-variation integrand of the plane-wave Regge action is identically zero for every polarization matrix and wavevector. Gravity analysts cite it when reducing Gate A2(a) of the Normalization-Gated Schläfli Two-Jet protocol. The proof splits the integrand into deficit and Schläfli groups, kills the first by vanishing flat deficits, and kills the second by the pathwise Schläfli identity at amplitude zero.
Claim. For every real $3\times 3$ polarization matrix $E$ and every wavevector $k\in\mathbb{R}^3$, the first-variation integrand of the plane-wave Regge action profile, evaluated at amplitude $t=0$ (the flat point), equals zero.
background
This module sits in the QG full-theory campaign under the ReggeTTContinuumSymbol program, Crux-1(c) lane. Gate A2 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol studies the true Regge action along plane-wave edge deformations of a flat periodic triangulation. Gate A0 audits the symbol specification; Gate A1 establishes local symbol existence; the first-derivative structure at flat is imported from the derivative gate and never re-proved here.
The action profile $S(t)$ is the sum over periodic edges of $\sqrt{\ell_e(t)},\delta_e(t)$, where $\ell_e$ are squared edge lengths of a plane-wave field and $\delta_e$ are deficit angles. Differentiating under the sum at a good amplitude yields the first-variation integrand $\sum_e\bigl(\ell'_e/(2\sqrt{\ell_e})\bigr)\delta_e + \sum_e\sqrt{\ell_e},\delta'_e$. The first group is the deficit contribution; the second is the Schläfli contribution.
At $t=0$ the background is flat, so every deficit vanishes (Stage-1 kernel theorem). Independently, the pathwise Schläfli kill states that $\sum_e\sqrt{\ell_e},\delta'_e=0$ at every good amplitude, by regrouping per tetrahedron and applying the closed-form tetrahedral Schläfli identity. Amplitude zero is good: all edges stay positive and all tets stay nondegenerate.
proof idea
Unfold the integrand definition and split the edge sum into two summands via additivity of finite sums.
For the deficit group, each summand is a product of an edge-length square-root derivative with the deficit of the plane-wave field at amplitude zero. The Stage-1 kernel fact that every flat deficit vanishes, together with multiplication by zero, makes every term zero, so the whole sum is zero.
For the Schläfli group, invoke the already-proved pathwise identity that the sum of $\sqrt{\ell_e},\delta'_e$ vanishes at every good amplitude, specialized to amplitude zero via the lemma that the zero path is good for every polarization and wavevector.
Adding the two vanishing sums finishes the argument.
why it matters
This lemma is the algebraic core of Gate A2(a): the first variation of the true Regge action vanishes at the flat point along every plane-wave direction. The parent theorem obtains $S'(0)=0$ by evaluating the derivative of the plane-wave action profile at zero (via the has-derivative-at statement for good amplitudes) and substituting this vanishing integrand.
In the broader protocol, Gate A2(a) clears the linear term so that Gate A2(b) can read the second variation at flat as a pure first-jet expression $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with no second derivatives of arccos. That Schläfli-reduced two-jet is the continuum symbol input for the Regge TT analysis. The result is fully proved (no sorry), and sits downstream of the pathwise Schläfli kill and the flat-deficit kernel, both already closed in this module family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.