axisReducedSecondVariation_applies
plain-language theorem explainer
At lattice size N=3, the second derivative at zero of the plane-wave Regge action along the preregistered axis TT polarization equals the named Schläfli-reduced Finset sum. Gate A2(c) of the Normalization-Gated Schläfli Two-Jet protocol; cited by anyone wiring the axis instance into numerics cross-checks. Proof is a one-line specialization of the general flat second-variation identity.
Claim. For the preregistered axis transverse-traceless polarization and its commensurate axis momentum at lattice size $N=3$, $$\frac{d^{2}}{dt^{2}}\Big|_{t=0} S_{\mathrm{pw}}(t) = -\sum_{\tau}\sum_{f=1}^{6} L'_{\tau f}(0)\,\theta'_{\tau f}(0),$$ where the right-hand side is the named reduced second-variation sum built from flat slot length-sqrt derivatives and flat slot angle derivatives.
background
This module is Gate A2 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the Regge TT continuum-symbol program (Crux-1(c)). Gate A0 audits the symbol specification; Gate A1 supplies local symbol existence; the first-derivative structure at flat is reused from the derivative gate and never re-proved here.
The plane-wave action profile is the true Regge action evaluated along a one-parameter family of edge-length perturbations driven by a fixed TT polarization and Bloch momentum. At every good amplitude the first derivative splits into an edge-sqrt term times deficit plus a sqrt-edge times deficit-derivative term. The pathwise Schläfli kill shows the entire second group vanishes identically near flat by the tetrahedral Schläfli identity, so no arccos second derivatives enter the two-jet.
Gate A2(b) already states that for general $N$, polarization $E$, and momentum $k$, the second derivative at zero equals the Schläfli-reduced double sum over periodic tets and six local slots. The named axis reduced second variation is that same double sum specialized to $N=3$, the axis TT-plus polarization, and the commensurate axis wave vector; its numerical value is deliberately not computed.
proof idea
One-line term proof: instantiate the general Gate A2(b) theorem (flat second variation equals the Schläfli-reduced contraction) at lattice size 3, the axis TT-plus polarization, and the commensurate momentum built from the axis wave vector. Unification matches the left-hand side to the iterated second derivative of the axis plane-wave profile at zero, and the right-hand side to the named axis reduced second-variation definition. No extra algebraic work.
why it matters
Closes Gate A2(c): the reduced formula applies verbatim to the preregistered axis instance, so $S''(0)$ is exactly the named Finset sum. That gives a cross-check hook for the non-proof numerics lane without claiming any evaluated value or continuum limit.
Together with Gate A2(a) (first variation vanishes at flat) and A2(b) (general Schläfli reduction), this pins the discrete two-jet for the axis TT mode that the continuum-symbol campaign needs. The immediately following combined corollary pairs this reduced form with Gate A1's fixed-$N$ TT Bloch symbol, equating the symbol value to $(2/N^3)$ times the Schläfli-reduced contraction, still without evaluation.
No downstream Lean dependents are recorded yet; the declaration is an instance anchor rather than a general lemma. Framework role is discrete gravity analysis on the Regge side of the QG full-theory campaign, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.