planeWaveActionProfile
plain-language theorem explainer
Defines the true nonlinear Regge action restricted to the one-parameter plane-wave edge-length family of amplitude t, polarization E, and wavevector k on the periodic Freudenthal torus. Anyone computing first or second variations of the TT Bloch symbol cites this profile as the scalar function of t. It is a one-line composition of the true action with the plane-wave edge field.
Claim. For torus size $N$, polarization matrix $E\in\mathbb{R}^{3\times 3}$, wavevector $k\in\mathbb{R}^3$, and amplitude $t\in\mathbb{R}$, the plane-wave action profile is $S_{E,k}(t):=S\bigl(\ell^{\mathrm{flat}}+t\,c\cdot\cos(k\cdot x_{\mathrm{mid}})\bigr)$, i.e. the true 3D Regge action evaluated on the plane-wave edge-squared-length field of amplitude $t$.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it packages the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus and the TT Bloch-symbol objects built from plane-wave probes. The true action is $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum_{\mathrm{tets}\ni e}\theta)$, with dihedral angles from Cayley–Menger cofactors on local squared-edge 6-tuples.
The plane-wave edge field (upstream) is the flat squared lengths plus a cosine modulation: $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t,c_d\cos(k\cdot(x+D_d/2))$, where $c_d$ comes from the polarization $E$ and the edge direction. Flat deficits vanish, so $S$ at $t=0$ is the flat background.
The profile simply freezes polarization and momentum and varies only the amplitude $t$, yielding a real scalar function whose derivatives at $0$ are the first and second variations along that TT mode.
proof idea
One-line definitional wrapper: apply the true Regge action to the plane-wave edge field at amplitude $t$. No lemmas, no tactics; the body is exactly trueReggeAction N (planeWaveEdgeField N E k t).
why it matters
This profile is the scalar path along which all Gate A2 variation theorems are stated. Downstream, hasDerivAt_planeWaveActionProfile gives $S'(t)$ in closed form at good amplitudes; trueReggeAction_firstVariation_flat_eq_zero proves $S'(0)=0$ (Gate A2(a)) by flat deficits plus Schläfli; trueReggeAction_secondVariation_flat_schlaefli identifies $S''(0)$ with the reduced hinge sum $-\sum_\tau\sum_f L'{\tau f}\theta'{\tau f}$ (Gate A2(b)).
Those second variations feed the TT Bloch symbol and the local-symbol existence theorems (planeWave_TTBlochSymbolIs_secondVariation, planeWaveActionProfile_contDiffAt). The open continuum target remains ReggeTTContinuumIsotropyTarget: isotropy of the continuum TT symbol with value $K(0)=-(1/4)I_{TT}$, matching linearized Einstein–Hilbert. The definition itself is pure scaffolding for that campaign, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.