deriv_actionProfile_eventuallyEq_reduced
plain-language theorem explainer
Near the flat background (amplitude t = 0), the ordinary derivative of the plane-wave Regge action profile equals the Schläfli-reduced first variation: only the edge-length times deficit group survives. Anyone proving the flat second variation (Gate A2(b)) cites this to replace S' by the reduced integrand before differentiating again. The proof is a short filter-upwards argument: on the path-good neighborhood, HasDerivAt gives the full first variation, which then equals the reduced form.
Claim. For edge polarization $E:\mathrm{Fin}\,3\to\mathrm{Fin}\,3\to\mathbb{R}$ and wavevector $k:\mathrm{Fin}\,3\to\mathbb{R}$, the derivative of the plane-wave Regge action profile $S(t)$ is eventually equal, in a neighborhood of the flat amplitude $t=0$, to the reduced first-variation integrand (the $\sum_e (\ell_e'/(2\sqrt{\ell_e}))\delta_e$ group alone).
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 the true Regge action evaluated along a one-parameter family of edge lengths that is flat at $t=0$ and modulated by polarization $E$ and wavevector $k$.
A path point $t$ is path-good when every edge length is positive and every tetrahedron is nondegenerate with interior dihedral cosines. On that set, the full first variation is $S'(t)=\sum_e\bigl[(\ell_e'/(2\sqrt{\ell_e}))\delta_e+\sqrt{\ell_e},\delta_e'\bigr]$ with closed-form edge, deficit, and angle derivatives from the derivative gate.
The pathwise Schläfli identity kills the entire second group $\sum_e\sqrt{\ell_e},\delta_e'$ at every good amplitude, not only at flat. The reduced first variation is therefore the deficit group alone. This lemma records that $S'$ and that reduced integrand agree as germs at $0$.
proof idea
Term-mode, three steps. First filter_upwards on eventually_pathGoodAt N E k, so it is enough to work at a good amplitude $t$ near $0$. At such $t$, hasDerivAt_planeWaveActionProfile supplies a HasDerivAt witness for the full first-variation integrand; rewriting with .deriv replaces deriv S t by that integrand. Finally firstVariationIntegrand_eq_reduced identifies the full integrand with the reduced (deficit-only) form at the same good $t$, using the pathwise Schläfli kill already proved in-module.
why it matters
Gate A2(b) needs $S''(0)$ without any second derivative of $\arccos$. The headline theorem trueReggeAction_secondVariation_flat_schlaefli obtains
$S''(0)=-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$
by writing the second iterated derivative as the derivative of $S'$ at $0$. This lemma is the bridge: near flat, $S'$ equals the reduced first variation, so one differentiates only the deficit group and never the Schläfli-vanishing angle-derivative group.
Together with Gate A2(a) (first variation vanishes at flat) and the derivative-gate flat angle Jacobian, it closes the Schläfli-reduced two-jet at flat for the continuum TT symbol. In the broader RS gravity lane this is continuum Regge calculus infrastructure, not a forcing-chain (T0–T8) step, but it is required before any continuum TT propagator or symbol can be extracted from the discrete action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.