planeWaveActionProfile_zero
plain-language theorem explainer
Along any plane-wave edge-length family on the periodic Freudenthal torus, the true nonlinear 3D Regge action is zero at amplitude zero. Gravity analysts cite this as the flat-point anchor of the action profile used to build the TT Bloch symbol. The proof is a two-rewrite term: zero amplitude lands on the flat field, and the action vanishes there.
Claim. For any polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$ and wavevector $k\in\mathbb{R}^3$, the plane-wave action profile of the true Regge action satisfies $S_{\mathrm{pw}}(E,k;0)=0$.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, then builds the plane-wave family and TT Bloch symbol object around that action.
The true action is $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum_{t\ni e}\theta)$, with dihedral angles from Cayley–Menger cofactors. The flat edge field is the Euclidean squared-length assignment; upstream, trueReggeAction_flatEdgeField proves $S$ vanishes there because every deficit is zero. The plane-wave edge field is the flat field plus an amplitude-$t$ modulation with polarization $E$ and momentum $k$. The action profile is simply $t\mapsto S$ along that family.
proof idea
One-line algebraic reduction after unfolding the profile definition. Rewrite with planeWaveEdgeField_zero_amplitude (at $t=0$ the family equals the flat field) and trueReggeAction_flatEdgeField (the action on the flat field is zero). No further casework.
why it matters
Feeds the protocol status record ReggeTTSymbolPreflightStatus, which certifies the true-action definition, its kernel-checked flat point, and the well-formedness of the TT Bloch symbol object. The zero-amplitude vanishing is the base point of the second-difference quadratic form used to extract the discrete TT symbol; without it the continuum isotropy target (ReggeTTContinuumIsotropyTarget, still open) has no anchored expansion. Numerics already report $K(0)=-(1/4)I_{\mathrm{TT}}$ matching linearized Einstein–Hilbert TT, but that remains NUMERICAL EVIDENCE, not a proved continuum limit. This lemma closes only the flat-point side of the preflight checklist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.