reducedFirstVariation
plain-language theorem explainer
Defines the Schläfli-reduced first variation of the plane-wave Regge action: sum over periodic edges of the sqrt-hinge slope times the edge deficit of the deformed field. Gravity analysts cite it when replacing the full two-group first-variation integrand by the deficit group alone near flat. It is a pure closed-form sum, not a proved identity; equality to S' is established downstream.
Claim. For a $3\times 3$ strain matrix $E$, wavevector $k\in\mathbb{R}^3$, and amplitude $t\in\mathbb{R}$, the reduced first variation is $$\sum_{e}\, L'_e(t)\,\delta_e\bigl(\ell(t)\bigr),$$ where the sum runs over positive-displacement periodic edges of the $N^3$ Freudenthal torus, $L'_e(t)=c_e/(2\sqrt{\ell_e(t)})$ is the closed-form derivative of the sqrt hinge length, and $\delta_e$ is the angular deficit of the plane-wave edge field at amplitude $t$.
background
This module sits in the QG full-theory campaign (ReggeTT continuum symbol, Crux-1(c), Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol). Gate A1 supplies local symbol existence; the first-derivative structure at flat is reused from the derivative gate and never re-proved here.
The full pathwise first variation of the plane-wave action profile splits as $\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\delta_e + \sqrt{l_e},\delta'_e\bigr]$. The second summand is the Schläfli group. Pathwise Schläfli kill shows that group vanishes identically on every good amplitude (positive edge lengths, nondegenerate tets with interior cosines), by regrouping per tetrahedron and applying the closed-form six-edge Schläfli identity.
Upstream ingredients: edgeSqrtDeriv is the closed form $c_e/(2\sqrt{l_e(t)})$; deficits are $2\pi-\sum\theta$ on hinges (DihedralAngle/Schlaefli); edges are PeriodicEdge base-plus-positive-displacement data on the periodic Freudenthal torus.
proof idea
Definition only: expand as a finite sum over PeriodicEdge N N N of the product edgeSqrtDeriv N E k e t * deficitOfField N (planeWaveEdgeField N E k t) e. No tactics, no lemmas applied at the definition site. Downstream theorems unfold this name and cancel the Schläfli summand via sum_sqrt_deficitDeriv_eq_zero.
why it matters
Gate A2 needs a clean object for the first jet of the Regge action after the Schläfli group is deleted. This definition is that object: the deficit-group-only integrand that $S'$ equals near flat.
It feeds three local parents. firstVariationIntegrand_eq_reduced proves the full integrand equals this reduced form on every good path point (add the Schläfli kill and drop the zero). deriv_actionProfile_eventuallyEq_reduced lifts that equality to filter equality of derivatives in a neighborhood of amplitude zero. hasDerivAt_reducedFirstVariation_flat differentiates the reduced form at flat, retaining only the $L'_e(0)\delta'_e(0)$ product-rule term because flat deficits vanish.
Together these close Gate A2(a) (first variation at flat is zero) and set up Gate A2(b) (second variation as a pure first-jet angle Jacobian contraction, with no second derivatives of arccos). In the broader RS gravity lane this is the algebraic cleanup that makes the continuum TT symbol computable from first derivatives alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.