hasDerivAt_planeWaveActionProfile
plain-language theorem explainer
At every amplitude where edge lengths stay positive and every tetrahedron is nondegenerate with interior dihedral cosines, the plane-wave Regge action profile is differentiable, and its derivative equals the explicit first-variation sum over edges of (L' δ + √l δ'). Anyone proving Gate A2(a) (vanishing first variation at flat) or the neighborhood agreement of S' with the reduced integrand cites this. The proof is termwise product rule plus finite sum of derivatives.
Claim. Fix a $3\times 3$ polarization matrix $E$, wavevector $k$, and amplitude $t_0$. If at $t_0$ every periodic edge length of the plane-wave field is positive and every periodic tetrahedron is nondegenerate with strictly interior dihedral cosines, then the plane-wave action profile $S(t)=\sum_e \sqrt{l_e(t)}\,\delta_e(t)$ is differentiable at $t_0$, and $S'(t_0)=\sum_e\bigl(L'_e(t_0)\,\delta_e(t_0)+\sqrt{l_e(t_0)}\,\delta'_e(t_0)\bigr)$, with $L'_e$ and $\delta'_e$ the closed-form hinge and deficit derivatives.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. It studies the true Regge action along plane-wave edge deformations on the periodic Freudenthal torus, with edges indexed by PeriodicEdge (base vertex plus one of seven positive cube displacements).
The action profile is $S(t)=\sum_e \sqrt{l_e(t)},\delta_e(t)$, where $l_e(t)$ is the plane-wave edge field and $\delta_e$ the angle deficit at edge $e$. The goodness predicate at amplitude $t$ requires every edge value positive and every tetrahedron nondegenerate with dihedral cosines strictly in $(-1,1)$. Under that hypothesis the closed forms $L'_e(t)=c_e/(2\sqrt{l_e(t)})$ (hinge sqrt derivative) and $\delta'e(t)=-\sum\tau \theta'$-matched contributions (deficit derivative) are well-defined.
The target derivative is packaged as the first-variation integrand $T(t)=\sum_e\bigl(L'_e(t),\delta_e(t)+\sqrt{l_e(t)},\delta'_e(t)\bigr)$. Upstream, the derivative gate already supplies differentiability of sqrt-hinges and deficits; this theorem only assembles them into $S'$.
proof idea
Unfold the action profile as the finite sum over periodic edges of $\sqrt{l_e(t)},\delta_e(t)$ (definitional equality via funext). For each edge, apply the product rule: differentiability of the sqrt factor comes from hasDerivAt_sqrtEdge (using positivity from the goodness hypothesis), and differentiability of the deficit from hasDerivAt_deficit (using the full goodness package). The resulting pointwise derivative is exactly $L'_e\delta_e+\sqrt{l_e}\delta'_e$. Conclude by HasDerivAt.fun_sum over the finite edge set, matching the unfolded first-variation integrand.
why it matters
This is the profile-derivative theorem listed in the module's proved inventory: it puts $S'(t)$ in closed form at every good amplitude, not merely at flat. Downstream, Gate A2(a) (trueReggeAction_firstVariation_flat_eq_zero) instantiates it at $t=0$ (via path-goodness at zero) and shows the integrand vanishes: flat deficits kill the first group, and the pathwise Schläfli identity kills $\sum_e\sqrt{l_e}\delta'_e$. The neighborhood theorem deriv_actionProfile_eventuallyEq_reduced rewrites deriv S via this HasDerivAt on a punctured neighborhood of flat, feeding the Schläfli-reduced second variation (Gate A2(b)), where no second derivative of arccos survives.
In the broader QG campaign this is the analytic hinge between the first-derivative gate and the two-jet at flat geometry. It does not itself invoke Recognition landmarks (T5–T8, RCL, phi), but it is infrastructure for the continuum TT symbol that those continuum limits will read.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.