planeWave_TTBlochSymbol_exists
plain-language theorem explainer
For every polarization matrix and integer wave vector on the fixed-N lattice, a real TT Bloch symbol value exists: the plane-wave amplitude second difference of the nonlinear Regge action converges as amplitude tends to zero. Anyone citing Gate A1 existence in the ReggeTT continuum-symbol program needs this non-vacuity form. The proof is a one-line existential wrapper around the constructive second-variation identification.
Claim. Fix lattice side $N$. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$ and every integer wave vector $m\in\mathbb{Z}^3$, there exists a real number $H$ such that the TT Bloch symbol predicate holds at $(N,E,m,H)$: the amplitude second-difference of the plane-wave Regge action tends to $H$ as the amplitude tends to $0$ in the punctured neighborhood of the origin.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the ReggeTT continuum-symbol campaign (Crux-1(c)). It works at fixed lattice side $N$ and studies the true nonlinear Regge action along a one-parameter plane-wave family of edge lengths, polarized by a $3\times 3$ matrix $E$ and driven by a commensurate momentum built from an integer wave vector $m$.
The preflight predicate TTBlochSymbolIs asserts only that the amplitude second difference converges to a named real $H$ on the punctured neighborhood filter at $0$; it does not claim existence. Upstream smoothness work shows the plane-wave action profile $S(t)$ is $C^\infty$ at $t=0$ (affine squared-edge paths through the flat Freudenthal tetrahedron, safe square roots, finite edge/tet sums), and a reusable local L'Hôpital bridge identifies the centered second difference limit with $S''(0)$.
The constructive sibling then pins a concrete value: $H=(2/N^3)\cdot S''(0)$. The present declaration is the pure existence packaging of that identification.
proof idea
One-line term-mode existential wrapper. Instantiate the witness by the constructive headline theorem planeWave_TTBlochSymbolIs_secondVariation, which already proves
$$\mathrm{TTBlochSymbolIs},N,E,m\bigl((2/N^3)\cdot S''(0)\bigr)$$
with $S$ the plane-wave action profile at the commensurate momentum of $m$. The anonymous existential pair is exactly that real and that proof; no extra analysis is performed here.
why it matters
Gate A1 must show the fixed-$N$ TT Bloch symbol object is non-vacuous for every polarization and wave vector before any continuum or dispersion analysis can treat $H$ as a defined quantity. The constructive sibling supplies the value $(2/N^3)S''(0)$; this companion form is the clean $\exists H$ interface that downstream consumers can cite without unpacking the second-variation bookkeeping.
In the QG full-theory campaign this closes the existence half of Crux-1(c) at fixed $N$. It does not yet evaluate the symbol, pass to the continuum limit, or connect to Recognition landmarks (phi-ladder masses, eight-tick octave, $D=3$); those sit further down the ReggeTT continuum-symbol stack. No used_by edges are recorded yet, so this is presently a leaf existence API for later symbol-value and continuum gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.