planeWave_TTBlochSymbolIs_reduced
plain-language theorem explainer
The fixed-N TT Bloch symbol of the true Regge action equals (2/N³) times the Schläfli-reduced flat second-variation contraction. Continuum-closer and zero-mode arguments cite this as the combined Gate A1+A2 existence form. Proof is a one-line rewrite of the Gate A1 second-variation witness by the Gate A2(b) Schläfli identity at commensurate momentum.
Claim. For every polarization matrix $E:\mathbb{R}^{3\times 3}$ and integer mode $m\in\mathbb{Z}^3$, the fixed-$N$ TT Bloch symbol equals $\frac{2}{N^3}\bigl(-\sum_{\tau}\sum_{f=1}^{6} L'_{\tau f}(0)\,\theta'_{\tau f}(0)\bigr)$, where $L'_{\tau f}(0)=v_{\tau f}/(2\sqrt{a^*_f})$ and $\theta'_{\tau f}(0)=\sum_g v_{\tau g} J_{fg}$ are the flat slot sqrt-edge and angle derivatives at the commensurate momentum of $m$.
background
Module setting is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the ReggeTT continuum-symbol program (Crux-1(c)). Gate A0 audits the symbol specification; Gate A1 (ReggeTTLocalSymbolExistence) produces a fixed-$N$ TT Bloch symbol as the second variation of the plane-wave action profile at flat. The first-derivative structure at flat is imported from ReggeTTDerivativeGate and never re-proved.
The Schläfli kill is the structural fact that near flat the pathwise second group $\sum_e \sqrt{l_e},\delta'e$ vanishes identically by the tetrahedral Schläfli identity, so no second derivative of $\arccos$ enters $S''(0)$. Gate A2(b) therefore states $S''(0)=-\sum\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with $L'=\mathrm{flatSlotSqrtDeriv}$ and $\theta'=\mathrm{flatSlotAngleDeriv}$ (flat angle Jacobian contraction). Periodic Freudenthal tets index the six local edges per cubic cell; commensurate momentum maps the integer mode $m$ to the Bloch wavevector $k$.
proof idea
One-line rewrite wrapper. Start from the Gate A1 existence theorem planeWave_TTBlochSymbolIs_secondVariation, which already asserts that the TT Bloch symbol equals $(2/N^3)$ times the raw second variation of the plane-wave action profile at flat. Rewrite that second-variation factor by trueReggeAction_secondVariation_flat_schlaefli evaluated at commensurateMomentum N m, which replaces $S''(0)$ by the Schläfli-reduced double sum $-\sum_\tau\sum_f L'\theta'$. The rwa closes the goal.
why it matters
Combined corollary of Gates A1 and A2(b): existence of the fixed-$N$ TT Bloch symbol together with its Schläfli-reduced closed form, still without numerical evaluation or continuum passage. Downstream, canonicalFiniteH_TTBlochSymbolIs restates this on the canonical finite symbol $H_N$, and is the entry point to the 3D continuum closer. The zero-mode corollary zeroMomentum_symbol_is_zero specializes $m=0$ and obtains symbol value $0$ for every $N$ and every polarization, establishing the lattice flat zero mode of the true nonlinear Regge action. Hinge-aware zero-mode assembly also consumes the reduced form. In the panel-locked protocol this is the last pure finite-$N$ identity before continuum and isotropy targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.