planeWaveTetSqEdges_apply
plain-language theorem explainer
Along any plane-wave edge-length family, each of the six local squared-edge coordinates of a periodic Freudenthal tetrahedron is exactly the flat Freudenthal value plus amplitude times a fixed velocity. Anyone proving smoothness or second variation of the Regge action at the flat background cites this affine law. The proof unfolds the field and velocity definitions, rewrites the flat edge via the periodic-displacement identity, and closes by ring.
Claim. For every polarization matrix $E$, wave vector $k$, periodic tetrahedron $\tau$, amplitude $t\in\mathbb{R}$, and local edge slot $f\in\{0,\ldots,5\}$, the squared length of slot $f$ under the plane-wave edge field at amplitude $t$ equals the canonical Freudenthal squared edge of $f$ plus $t$ times the plane-wave velocity of that slot on $\tau$.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program: fixed lattice size $N$, plane-wave families of edge lengths, and existence of the TT Bloch symbol from the second derivative of the true nonlinear Regge action at the flat background.
A Freudenthal tetrahedron in the unit cube has a fixed local squared-edge 6-tuple: three unit steps (value 1), two face diagonals (value 2), and one body diagonal (value 3). The map localEdgeOf picks, for each tetrahedron orientation and each of the six slots, the corresponding global edge; on the periodic torus those edges are identified with periodic displacements whose squared lengths recover the Freudenthal tuple.
The plane-wave edge field deforms every global edge by an amplitude $t$ times a polarization-and-wavevector phase. The local squared-edge extractor reads the six slots of a chosen periodic tetrahedron from that field. The companion velocity coefficients package the linear response of each slot, so the claim is that the deformation is strictly affine through the flat Freudenthal point.
proof idea
Term-mode proof in three strokes. First simp only expands the local squared-edge extractor, the plane-wave edge field, and the named velocity, exposing an expression built from periodic displacement squared lengths plus a linear $t$ term. Second, rewrite the bare Freudenthal slot value as the periodic-displacement squared length of the local edge chosen by localEdgeOf, using the identity freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf. Third, ring identifies the two sides. No analysis or positivity is used; the equality is purely algebraic in $t$.
why it matters
Item (a) of the module's Gate A1 checklist: every local squared-edge path is the affine line flat + $t\cdot v$ through the canonical Freudenthal tuple. Immediate children are the $t=0$ specialization (tuple equals Freudenthal exactly) and the $C^n$ statement for every order (affine maps are smooth). Those feed dihedral-angle and action-profile smoothness at the flat point, which in turn license the centered-second-difference limit that produces the fixed-$N$ TT Bloch symbol $S''(0)$.
Downstream, the flat second-variation development re-bases the same affine path at an arbitrary amplitude $t_0$ to obtain derivatives of slot angles wherever the tetrahedron stays nondegenerate. Within the broader RS gravity lane this is bookkeeping infrastructure for continuum TT symbols on the eight-tick / $D=3$ lattice geometry, not a new dynamical law; it closes the algebraic half of Crux-1(c) so analytic gates can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.