polEdgeCoeff_neg
plain-language theorem explainer
Negating a polarization matrix E flips the sign of every edge-class coefficient c_d. Lattice gravity and TT Bloch-symbol constructions cite this oddness when relating polarization sign to plane-wave amplitude. The proof unfolds the double-sum definition and pushes the minus through both Finset sums by ring arithmetic.
Claim. For every real $3\times 3$ matrix $E$ and every displacement class $d\in\{0,\ldots,6\}$, the edge-class coefficient satisfies $c_d(-E)=-c_d(E)$, where $c_d(E)=\sum_{i,j} E_{ij}\,D_d^i\,D_d^j$ and $D_d$ is the real displacement vector of class $d$.
background
The Regge TT symbol preflight module studies the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, as a function of an arbitrary edge squared-length field. Polarization matrices enter when one builds plane-wave edge fields for the TT Bloch symbol object used in the continuum-symbol program.
The edge-class coefficient of a polarization is the quadratic form $c_d(E)=\sum_{i,j} E_{ij},D_d^i,D_d^j$. It records how the metric perturbation $E$ loads the squared length of displacement class $d$ among the seven edge classes of the lattice. The seven classes index the distinct edge directions in the Freudenthal triangulation.
This lemma is pure bilinearity of that double sum: the map $E\mapsto c_d(E)$ is odd. It is the algebraic step needed before identifying a sign flip of $E$ with a sign flip of the plane-wave amplitude.
proof idea
Unfold the edge-class coefficient to the double sum over $i,j\in\mathrm{Fin},3$. Rewrite the outer sum via Finset.sum_neg_distrib, then the inner sum the same way, reducing to termwise equality $(-E_{ij}),D_d^i,D_d^j=-(E_{ij},D_d^i,D_d^j)$. Close each term by ring. No external lemmas beyond Finset sum distributivity are required.
why it matters
The sole direct consumer is the theorem that negating the polarization equals negating the amplitude of the plane-wave edge field. That identity sits in Stage 1 of the Regge TT continuum symbol program: constructing the TT Bloch symbol of the true nonlinear Regge action on this lattice and preparing the open continuum isotropy target.
In the broader gravity analysis, these preflight sign lemmas remove bookkeeping ambiguity in the polarization sector before any continuum comparison with the linearized Einstein-Hilbert TT coefficient $K(0)=-(1/4),I_{TT}$. The continuum isotropy claim itself remains open (ReggeTTContinuumIsotropyTarget); nothing here closes that target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.