trueReggeAction_secondVariation_flat_schlaefli
plain-language theorem explainer
At flat background the second variation of the true Regge plane-wave action equals minus the double sum over tetrahedra and slots of length-sqrt derivatives times angle derivatives. Gravity analysts cite this as Gate A2(b): the Schläfli-reduced kernel equation that removes every arccos second derivative from the critical path. The proof rewrites the second iterated derivative as the derivative of the reduced first variation, then applies the flat edge-sqrt/deficit contraction identity.
Claim. For any edge-polarization matrix $E$ and wavevector $k$, the second derivative at amplitude zero of the plane-wave Regge action profile equals $-\sum_{\tau}\sum_{f=1}^{6} L'_{\tau f}(0)\,\theta'_{\tau f}(0)$, where $L'_{\tau f}(0)=v_{\tau f}/(2\sqrt{a^*_f})$ is the flat slot length-sqrt derivative and $\theta'_{\tau f}(0)=\sum_g v_{\tau g} J_{fg}$ is the flat angle-Jacobian contraction. No second derivative of $\arccos$ appears.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program (Crux-1(c)). Gate A0 audited the symbol specification; Gate A1 established local symbol existence. The first-derivative structure at flat is imported from the derivative-gate module and never re-proved here.
The true Regge action along a plane-wave edge-length path is $S(t)=\sum_e\sqrt{l_e(t)},\delta_e(t)$. Differentiating at a good amplitude yields two groups: a length-sqrt times deficit term and a length times deficit-derivative term. The pathwise Schläfli kill states that the entire second group vanishes identically near flat: regrouped per tetrahedron it is $-\sum_\tau\sum_g v_g(\sum_f\sqrt{a_f}\partial\theta_f/\partial a_g)=0$ by the closed-form six-edge tetrahedral Schläfli identity. Consequently $S'$ near zero equals the deficit group alone.
Gate A2(a) already shows $S'(0)=0$ (flat deficits vanish and Schläfli kills the rest). Gate A2(b) differentiates that reduced first variation once more at flat.
proof idea
Term-mode rewrite chain. First expand iteratedDeriv 2 as successive first derivatives via iteratedDeriv_succ and iteratedDeriv_one. Replace the outer derivative of the action profile by the derivative of the reduced first-variation expression, using eventual equality of the profile derivative with its Schläfli-reduced form (deriv_actionProfile_eventuallyEq_reduced). Evaluate that derivative at zero by the hasDerivAt certificate for the reduced first variation at flat (hasDerivAt_reducedFirstVariation_flat). The resulting sum is exactly the flat edge-sqrt/deficit contraction identity (sum_edgeSqrtDeriv_deficitDeriv_flat), which is the displayed double sum over tets and slots.
why it matters
This is the headline kernel equation of Gate A2(b). It deletes the explicit-G Hessian stage from the critical path: near flat, pathwise Schläfli already killed the arccos-second-derivative group, so the second variation is only the first-jet contraction of length-sqrt derivatives against angle Jacobians.
Downstream, axisReducedSecondVariation_applies instantiates the formula on the preregistered axis $+$-polarization at $N=3$ (Gate A2(c) cross-check hook, no numeric value claimed). The combined corollary planeWave_TTBlochSymbolIs_reduced equates the fixed-$N$ TT Bloch symbol of Gate A1 to $(2/N^3)$ times this Schläfli-reduced contraction. The 4D sibling module references the same pattern for an independent nonlinear flat second variation via 4D pathwise Schläfli elevation (still marked open there).
In the broader RS gravity lane this supplies the discrete second-variation kernel needed before any continuum or continuum-symbol limit is attempted; it does not itself assert a continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.