biquad_sym4
plain-language theorem explainer
On a symmetric 4×4 matrix H, the bi-quadratic form built from any rational six-index coefficient table C is unchanged if C is replaced by its average over the four swaps of the two H-index pairs. Gravity analysts working the exact midpoint Bloch m² TT identity in 4D Regge calculus cite this to freely pass to a partially symmetrized coefficient table. The proof flips the six-fold sums on those index pairs, restores H-entries by symmetry, expands the average, and cancels.
Claim. Let $C:\{0,1,2,3\}^6\to\mathbb{Q}$, let $H$ be a real $4\times 4$ matrix, and let $k\in\mathbb{R}^4$. Write $\mathrm{biquad}(C,H,k)=\sum_{a,b,c,d,i,j} C_{abcdij}\,H_{ab}H_{cd}k_i k_j$. Let $\mathrm{sym}_4 C$ be the average of $C$ over the four maps that independently swap $(a,b)$ and $(c,d)$. If $H$ is symmetric ($H_{ij}=H_{ji}$ for all $i,j$), then $\mathrm{biquad}(\mathrm{sym}_4 C,H,k)=\mathrm{biquad}(C,H,k)$.
background
The module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis. The mass-squared contribution is rewritten as a bi-quadratic form: quadratic in the edge-length Hessian entries $H_{ab}$ and quadratic in the Bloch wave components $k_i$. Concretely,
$$\mathrm{biquad}(C,H,k)=\sum_{a,b,c,d,i,j}C_{abcdij},H_{ab}H_{cd}k_ik_j,$$
with $H$ a real $4\times 4$ matrix and $k\in\mathbb{R}^4$. The coefficient table $C$ is assembled from the 1208 Regge couplings via m2Coeff.
Symmetry of $H$ means $H_{ij}=H_{ji}$ for all indices (the matrix-level IsSymmetric used throughout the edge TT decomposition). The operator sym4C replaces $C$ by the average of the four tables obtained by swapping the first pair and/or the second pair of $H$-indices. Two private sum-relabeling lemmas (sum6_flip_ab, sum6_flip_cd) implement pure index commutation of the six-fold finite sums.
proof idea
Three auxiliary identities are proved first. For the $(a,b)$-swap: apply sum6_flip_ab to move the coefficient indices, then use $H_{ba}=H_{ab}$ pointwise under the symmetry hypothesis to restore the original monomials. The $(c,d)$-swap is identical via sum6_flip_cd. The double swap composes both flips and both symmetry rewrites.
Unfold biquad and sym4C. Distribute the factor $1/4$ through the sum (cast and ring on each term), split the sum of four tables by Finset.sum_add_distrib, and rewrite each of the three non-identity summands by the identities above. The four identical copies cancel against the denominator, leaving the original bi-quadratic.
why it matters
Parent theorem biquad_symFull chains this result with the exchange symmetrizer: it first reduces full symmetrization to sym4C via biquad_sym2ex, then applies the present lemma. That full invariance lets the exact midpoint $m^2$ TT identity work with a fully symmetrized coefficient table without changing the value on physical (symmetric) Hessians.
In the broader Recognition gravity stack this is pure algebraic hygiene inside the 4D Regge midpoint analysis that closes exact_midpoint_m2_tt_identity (scripts regge_4d_m2_tt_identity_20260721.py and the kernel cert upgrade). It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure that keeps the Bloch $m^2$ quadratic form well-defined under the index symmetries forced by a real symmetric edge Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.