axisReducedSecondVariation
plain-language theorem explainer
Named real equal to the Schläfli-reduced second variation of the true Regge action for the axis TT plane-wave instance on the N=3 periodic lattice. Citation target for the GATE A2(c) equality and for the non-proof numerics cross-check lane. Defined as a double Finset sum of products of flat slot sqrt-derivatives and angle-derivatives; no numerical value is evaluated or claimed.
Claim. For the axis transverse-traceless polarization at lattice size $N=3$ with commensurate axis momentum, define the reduced second-variation scalar $$ -\sum_{\tau}\sum_{f=1}^{6} L'_{\tau f}(0)\,\theta'_{\tau f}(0), $$ where the outer sum runs over periodic Freudenthal tetrahedra $\tau$ in the $3\times 3\times 3$ cell, the inner sum runs over the six local edge slots $f$ of each tet, $L'_{\tau f}(0)$ is the flat slot square-root edge derivative, and $\theta'_{\tau f}(0)$ is the flat slot angle derivative. No numerical value is asserted.
background
This module is Gate A2 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the Regge TT continuum-symbol campaign. Gate A0 audits the symbol specification; Gate A1 gives local symbol existence; the first-derivative structure at flat is reused from the derivative gate and never re-proved here.
The true Regge action profile along a plane-wave amplitude $t$ has first derivative $S'(t)=\sum_e\bigl[(l'e/(2\sqrt{l_e}))\delta_e+\sqrt{l_e},\delta'e\bigr]$ at every good amplitude. The pathwise Schläfli kill deletes the entire second group identically near flat, so the second variation at $t=0$ collapses to $-\sum\tau\sum_f L'{\tau f}(0),\theta'_{\tau f}(0)$ with $L'=\mathrm{flatSlotSqrtDeriv}$ and $\theta'=\mathrm{flatSlotAngleDeriv}$ (Gate A2(b)).
PeriodicTet 3 3 3 indexes the six Freudenthal tetrahedra inside each cubic cell of the $N=3$ periodic torus. The axis instance fixes the plus TT polarization and the commensurate axis wave vector; this definition simply names the resulting scalar sum.
proof idea
Pure definition (no proof obligations). The body is the Gate A2(b) reduced formula specialized to $N=3$, the preregistered axis TT polarization, and the commensurate axis momentum: a negated double sum over PeriodicTet 3 3 3 and Fin 6 of the product flatSlotSqrtDeriv * flatSlotAngleDeriv at those parameters. No simplification, evaluation, or positivity argument is performed.
why it matters
Gives a stable, #eval-free name to the axis-instance second variation so that GATE A2(c) (axisReducedSecondVariation_applies) can state the equality
$$\partial_t^2 S_{\mathrm{axis}}(0)=\mathrm{axisReducedSecondVariation}$$
by a one-line application of the general Schläfli-reduced formula. Downstream doc-comment: "its $S''(0)$ IS the named Finset sum. Cross-check hook for the (non-proof) numerics lane; no value claimed."
In the broader QG campaign this is the concrete scalar that continuum-symbol and stability arguments read off for the axis mode after the Schläfli kill has removed every arccos second derivative. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is a gravity-analysis bookkeeping object inside Crux-1(c).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.