planeWave_TTBlochSymbolIs_secondVariation
plain-language theorem explainer
For every lattice side N, polarization matrix E, and integer wave vector m, the fixed-N TT Bloch symbol exists and equals (2/N³) times the second derivative at zero of the plane-wave Regge action profile. Gravity analysts cite this as Gate A1 existence in the Normalization-Gated Schläfli Two-Jet protocol. The proof multiplies the local C² centered-second-difference bridge by the constant 2/N³ and matches the preflight difference quotient.
Claim. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$ and every integer wave vector $m\in\mathbb{Z}^3$, the fixed-$N$ TT Bloch symbol predicate holds at the real number $(2/N^3)\,S''(0)$, where $S(t)$ is the plane-wave action profile of the true nonlinear Regge action at the commensurate momentum of $m$, and $S''(0)$ is the second iterated derivative of $S$ at $0$.
background
This module is Gate A1 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the ReggeTTContinuumSymbol program (Crux-1(c)). Earlier items establish that along a plane-wave family every tetrahedron's squared-edge tuple is an affine path through the flat Freudenthal configuration, dihedral angles are $C^\infty$ at $t=0$, and the full nonlinear Regge action profile $S(t)$ is $\mathrm{ContDiffAt},\mathbb{R},n$ at $0$ for every finite $n$.
The predicate TTBlochSymbolIs packages the fixed-$N$ Bloch symbol as the limit of the preflight second-difference quotient ttSecondDifference. That quotient is exactly $(2/N^3)\cdot[(S(t)-2S(0)+S(-t))/t^2]$. The reusable local bridge states: if $f$ is $C^2$ at $0$, then $(f(t)-2f(0)+f(-t))/t^2$ tends to the second iterated derivative at $0$ on the punctured neighborhood filter (one L'Hôpital pass, no global $C^4$ hypothesis).
Commensurate momenta label the discrete Brillouin modes on the $N$-periodic lattice; the polarization $E$ fixes the TT strain pattern on edges.
proof idea
Set $k$ to the commensurate momentum of $m$ and $S$ to the plane-wave action profile at $(N,E,k)$. Invoke planeWaveActionProfile_contDiffAt to obtain $\mathrm{ContDiffAt},\mathbb{R},2,S,0$. Apply the reusable bridge tendsto_centeredSecondDifference_of_contDiffAt to get convergence of the centered second difference to $S''(0)$. Unfold the symbol predicate, multiply the filter limit by the constant $2/N^3$, and congruence-rewrite the difference quotient against ttSecondDifference (clearing the $N$-scaling and restoring the named $k$ and $S$). No evaluation of $S''(0)$ is attempted.
why it matters
This is the headline existence theorem of Gate A1: the fixed-$N$ TT Bloch symbol object is non-vacuous for every polarization and wave vector, identified as $(2/N^3)S''(0)$ with exact bookkeeping and no stray $1/2$. Downstream, planeWave_TTBlochSymbol_exists is the pure $\exists H$ packaging, and planeWave_TTBlochSymbolIs_reduced combines this with the Schläfli-reduced contraction so the same symbol equals $(2/N^3)$ times a flat-slot edge-angle sum, still without continuum evaluation.
In the QG campaign this closes the local-symbol existence gate before any continuum or numerical target. The continuum $-(1/4)$ TT symbol target remains explicitly open; the theorem only pins the limit object, not its value. Framework contact is through the discrete Regge action on the eight-tick / $D=3$ lattice scaffolding, not through T5–T8 forcing directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.