planeWaveEdgeField
plain-language theorem explainer
Defines the plane-wave family of edge squared-length fields on the side-N periodic Freudenthal torus: flat background plus amplitude t times a polarized cosine at the edge midpoint. Gravity analysts cite it as the one-parameter path through configuration space for the true nonlinear Regge action. The body is a pure pointwise formula, not a proof.
Claim. Given a polarization matrix $E\colon\{0,1,2\}^2\to\mathbb{R}$, a wavevector $k\in\mathbb{R}^3$, and an amplitude $t\in\mathbb{R}$, the plane-wave edge field on the side-$N$ periodic Freudenthal torus is the map sending each positive-displacement periodic edge $e$ to $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t\,c_d\,\cos\bigl(k\cdot(x+D_d/2)\bigr)$, where $c_d$ is the polarization coefficient for the displacement class of $e$ and the phase is evaluated at the edge midpoint.
background
This module is Stage 1 of the Regge TT continuum-symbol program: the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, its flat point, and the TT Bloch-symbol object. An edge field is one real (squared length) per positive-displacement periodic edge. The flat background assigns to each edge the squared length of its displacement class (values in ${1,1,1,2,2,2,3}$ via periodicDispSqEdge).
The true Regge action is $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum\theta)$ with dihedral angles from Cayley–Menger on local squared-edge tuples. The plane-wave family is the standard one-parameter probe through that configuration space: modulate the flat lengths by a polarized standing wave so that second variation, first-variation integrands, and Bloch symbols can be read off as functions of amplitude $t$ and momentum $k$.
proof idea
Definitional, not a theorem. Pointwise on each periodic edge $e$, add the flat squared length of the displacement class to $t$ times the polarization coefficient of that class times the cosine of the edge-midpoint phase for wavevector $k$. No lemmas are applied; the formula is the content.
why it matters
This is the configuration-space path that the entire flat second-variation and derivative-gate stack rides on. Downstream, the action profile along the family is definitionally the true Regge action of this field; deficits vanish at $t=0$; edge sqrt-derivatives and path-goodness neighborhoods are stated relative to it; first-variation integrands are built from it. In the QG campaign it is the concrete family whose continuum TT Bloch symbol is the open target ReggeTTContinuumIsotropyTarget (numerical evidence points to isotropic $K(0)=-(1/4)I_{TT}$, matching linearized Einstein–Hilbert TT). Without a named plane-wave edge field, the Stage-1 preflight cannot connect the nonlinear action to the symbol object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.