symFull
plain-language theorem explainer
Defines the full order-8 bi-quadratic symmetrization of a six-index rational coefficient table on Fin 4: average first over the two pair flips, then over pair exchange. Gravity analysts cite it when reducing midpoint Bloch m² identities to closed forms on symmetric 4×4 matrices. The body is the composition of the flip average with the exchange average.
Claim. For a six-index rational table $C$ on $(\mathrm{Fin}\,4)^6$ and indices $a,b,c,d,i,j$, the full bi-quadratic symmetrization is the composition of the four-term average over flips of $(a,b)$ and $(c,d)$ with the two-term average over the pair exchange $(a,b)\leftrightarrow(c,d)$. Explicitly it is the mean of $C$ over the order-8 group generated by those two flips and the exchange.
background
This module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis: the midpoint Bloch mass-squared form on a 4×4 matrix $H$ and wave $k$ is to match a closed bi-quadratic expression. Coefficient tables are six-index maps $C:(\mathrm{Fin},4)^6\to\mathbb{Q}$ feeding a bi-quadratic form in the entries of $H$ and $k$.
Two partial symmetrizers sit upstream. The flip average replaces $C$ by the mean of the four values obtained by swapping within $(a,b)$ and within $(c,d)$. The pair-exchange average then means $C$ with the table after $(a,b)\leftrightarrow(c,d)$. Their composition is the full order-8 orbit average needed so that the bi-quadratic depends only on the symmetric part of $H$.
The local setting is discrete 4D gravity on the torus with TT (transverse-traceless) hinge data; the identity equates an explicit midpoint $m^2$ coefficient table to a closed-form table after this symmetrization.
proof idea
Pure definitional composition: apply the four-term flip average to $C$, then feed that table into the two-term pair-exchange average, evaluated at $(a,b,c,d,i,j)$. No tactics or lemmas; the order-8 group action is encoded by nesting those two averages (factors $1/4$ then $1/2$).
why it matters
This is the coefficient-level projector that makes the midpoint Bloch $m^2$ bi-quadratic invariant under the residual discrete symmetries of the 4D TT sector. Downstream, the bi-quadratic of the fully symmetrized table equals the bi-quadratic of the raw table on every symmetric $H$, which is the bridge from the explicit $m^2$ assembly to the closed form under the symmetry hypothesis.
It also underwrites the pointwise certificate that the full symmetrization of the explicit $m^2$ table agrees with that of the closed-form coefficient table (4096 rational identities), and the integer-scaling comparison that moves factors of $1/32$ through the same orbit average. In the kernel-glue layer, a scaling lemma for this full symmetrization packages those rational identities for the certified kernel upgrade of the Regge 4D $m^2$ TT identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.