planeWaveEdgeField_neg_polarization
plain-language theorem explainer
Negating the polarization tensor of a plane-wave edge-length perturbation is identical to flipping the amplitude sign. Anyone building the TT Bloch symbol or checking quadratic-form symmetries of the true Regge action cites this. The proof is a short term argument: unfold the plane-wave field, apply the linear sign flip of the polarization coefficient, and finish by ring.
Claim. For any polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wavevector $k$, and amplitude $t\in\mathbb{R}$, the plane-wave edge-squared-length field built from $-E$ at amplitude $t$ equals the field built from $E$ at amplitude $-t$: $\ell^{(-E)}(t)=\ell^{(E)}(-t)$.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it defines the true nonlinear 3D Regge action on the periodic Freudenthal torus as a function of an arbitrary edge squared-length field, then builds the TT Bloch symbol object from plane-wave perturbations of the flat background.
The plane-wave edge field is the one-parameter family $\ell_e(t)=\ell^2_{\mathrm{flat}}(e)+t,c_d(E),\cos(k\cdot(x+D_d/2))$, where $c_d(E)$ is the polarization coefficient on displacement class $d$ and the cosine is evaluated at the edge midpoint phase. Polarization $E$ is a $3\times 3$ real matrix of mode amplitudes; the coefficient map is linear in $E$, so $c_d(-E)=-c_d(E)$ (the sibling fact polEdgeCoeff_neg).
The local setting is preflight for the open continuum isotropy target: numerical probes report an isotropic TT symbol $K(0)=-(1/4)I_{TT}$, matching linearized Einstein-Hilbert, but that continuum claim remains open.
proof idea
Pointwise on edges via funext. Unfold the plane-wave field definition so each edge value is flat squared length plus $t$ times the polarization coefficient times a cosine. Rewrite the coefficient of $-E$ by the linear identity polEdgeCoeff_neg, which supplies a minus sign. The remaining algebraic identity $t\cdot(-c)=(-t)\cdot c$ is discharged by ring. No geometric lemmas are needed.
why it matters
Feeds directly into ttSecondDifference_neg_polarization, which states that the second-difference quadratic form of the plane-wave action profile is invariant under $E\mapsto -E$, "as a quadratic form must be." That sign symmetry is part of the TT Bloch symbol object's structural hygiene before continuum limits are taken.
In the QG full-theory campaign this sits under the Regge TT continuum-symbol program (Stage 1, unlocked after C10 probe sign-off). It does not touch the open target ReggeTTContinuumIsotropyTarget itself, but clears an algebraic prerequisite so later symbol identities can treat polarization orientation as a pure quadratic degree of freedom. Framework-wise it is lattice gravity bookkeeping on the Freudenthal torus, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.