firstVariationIntegrand
plain-language theorem explainer
Defines the explicit first-variation integrand of the plane-wave Regge action profile: the edge sum of hinge-length derivative times deficit plus sqrt-length times deficit derivative. Anyone proving Gate A2 (flat first variation vanishes, Schläfli-reduced second variation) cites it as the closed-form candidate for S'(t). The body is a pure sum of already-closed sibling derivatives; no proof content.
Claim. For a polarization matrix $E$, wavevector $k$, and amplitude $t\in\mathbb{R}$, the first-variation integrand is $$T(t)=\sum_{e}\Bigl(L'_e(t)\,\delta_e(t)+\sqrt{\ell_e(t)}\,\delta'_e(t)\Bigr),$$ summed over positive-displacement periodic edges of the side-$N$ Freudenthal torus, where $L'_e$ is the closed-form derivative of the sqrt hinge factor, $\delta_e$ is the Regge deficit of the plane-wave edge field at amplitude $t$, and $\delta'_e$ is the closed-form deficit derivative.
background
Module setting is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program: first- and second-variation structure of the true nonlinear 3D Regge action on the periodic Freudenthal torus, evaluated along plane-wave edge fields, with the derivative gate reused and never re-proved.
A PeriodicEdge is a positive-displacement edge on the torus (base vertex plus one of seven cube displacements). The plane-wave edge field at amplitude $t$ assigns squared lengths $\ell_e(t)$ along those edges. The Regge deficit $\delta_e$ is $2\pi$ minus the sum of incident dihedral angles. Sibling closed forms supply the primed objects: edgeSqrtDeriv is $L'_e(t)=c_e/(2\sqrt{\ell_e(t)})$, and deficitDeriv is $\delta'e(t)=-\sum\tau$(matched slot-angle derivatives).
The classical Regge first variation is the edge sum of those two product terms; this definition packages that sum as a named real-valued function of $t$, ready for differentiation and evaluation theorems.
proof idea
Definition only: expand as a finite sum over PeriodicEdge N N N of the product edgeSqrtDeriv * deficitOfField(planeWaveEdgeField) plus sqrt(planeWaveEdgeField) * deficitDeriv. No tactics, no lemmas applied at this site; the mathematical content is entirely in the named summands already proved differentiable elsewhere in the module.
why it matters
This is the explicit right-hand side that Gate A2 hangs on. Downstream, hasDerivAt_planeWaveActionProfile states that at every good amplitude the action profile has derivative exactly this integrand, with every primed object in closed form. firstVariationIntegrand_zero then shows the integrand vanishes at flat: the deficit group dies by the Stage-1 kernel (flat deficits zero) and the Schläfli group dies by the pathwise kill. firstVariationIntegrand_eq_reduced identifies it near flat with the reduced (deficit-group-only) form after sum_sqrt_deficitDeriv_eq_zero.
Together those feed Gate A2(a) (first variation at flat is zero) and Gate A2(b) (second variation equals the Schläfli-reduced angle-Jacobian contraction, with no arccos second derivatives). In the broader RS gravity lane this is the analytic hinge between the discrete Regge action and the continuum TT symbol at flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.