sum6_flip_ab
plain-language theorem explainer
Six-fold sums of a real function on (Fin 4)^6 are invariant under swapping the first two indices. Index-bookkeeping lemma in the 4D Regge exact-midpoint Bloch m² TT identity module. Cited when symmetrizing bi-quadratic coefficient tables against a symmetric Hessian. Proof is a one-line wrapper of Finset.sum_comm.
Claim. For every real-valued $F$ on six copies of $\{0,1,2,3\}$, $\sum_{a,b,c,d,i,j} F(a,b,c,d,i,j) = \sum_{a,b,c,d,i,j} F(b,a,c,d,i,j)$.
background
The ambient module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis (script-backed kernel upgrade). Local types are Mat4 (real $4\times 4$ matrices) and Wave4 (real 4-vectors), used to expand the 1208-coupling midpoint $m^2$ sum as a bi-quadratic form with coefficient table m2Coeff.
This declaration sits in the pure index-bookkeeping subsection that precedes the symmetry lemmas for that bi-quadratic. The six summed indices run over edge/vertex labels in the 4D coupling expansion; the first two slots are the pair contracted against the Hessian entries $H_{ab}$.
No physics content is encoded here: only the elementary fact that finite sums over a product of finite index sets commute under a transposition of two summation variables.
proof idea
One-line wrapper: apply Finset.sum_comm to the outermost pair of sums (the $a$ and $b$ summations). The remaining four nested sums are left untouched; Mathlib's sum-commute lemma supplies the equality of the two six-fold sums with $F(a,b,\ldots)$ versus $F(b,a,\ldots)$.
why it matters
Feeds biquad_sym4, which shows that replacing a six-index coefficient table $C$ by its $(a\leftrightarrow b)$-symmetrization leaves the bi-quadratic form unchanged whenever the Hessian $H$ is symmetric. That symmetry step is part of the chain that rewrites exactMidpointBlochM2 as biquad m2Coeff and ultimately closes exact_midpoint_m2_tt_identity in 4D Regge calculus.
Within Recognition Science gravity analysis this is scaffolding hygiene, not a forcing-chain landmark: it keeps the TT-sector $m^2$ identity proof free of ad-hoc index gymnastics when the coefficient table is averaged under the residual discrete symmetries of the midpoint kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.