symFullZ
plain-language theorem explainer
Integer full (order-8) symmetrization of a six-index 4D kernel table: average the order-4 pair-swap symmetrizer on blocks (a,b;c,d) and (c,d;a,b). Analysts of the midpoint m^{2} TT identity in 4D Regge calculus cite it to keep exact scale-32 integer arithmetic before casting to rationals. The body is a one-line average of two order-4 integer symmetrizers.
Claim. For an integer six-index array $C$ on $\mathrm{Fin}\,4$ and indices $a,b,c,d,i,j\in\mathrm{Fin}\,4$, the full integer symmetrization is $\frac12\bigl(S_4(C;a,b,c,d,i,j)+S_4(C;c,d,a,b,i,j)\bigr)$, where $S_4$ is the order-4 average of the four pair-swaps of the first two index pairs (leaving $i,j$ fixed).
background
The ambient module holds kernel certificates for the midpoint $m^2$ transverse-traceless (TT) identity in 4D Regge analysis. Tables are stored as integer arrays at scale 32; certificates use only decide on finite Fin 4 domains (no native evaluation).
The upstream order-4 integer symmetrizer averages four rearrangements of the first two index pairs: $S_4(C;a,b,c,d,i,j)=\frac14\bigl(C_{abcdij}+C_{bacdij}+C_{abdcji}+C_{badcij}\bigr)$ (with $i,j$ fixed). The full symmetrizer then averages that quantity with the same quantity after swapping the two blocks $(a,b)\leftrightarrow(c,d)$, producing the order-8 integer kernel used before dividing by 32 into rationals.
proof idea
Pure definition: return half the sum of the order-4 integer symmetrizer on $(a,b,c,d,i,j)$ and on the block-swapped arguments $(c,d,a,b,i,j)$. No lemmas or tactics; integer division by 2 is part of the defining expression.
why it matters
Keeps the full order-8 symmetrization inside exact integer arithmetic so downstream glue can relate rational and integer kernels by a uniform factor of 32. Parents include the private bridge that the rational full symmetrizer equals this integer version cast to $\mathbb{Q}$ and divided by 32; the kernel certificate that the explicit and closed scale-32 tables agree after full integer symmetrization (decide over all Fin 4 indices); the scaling lemma for order-8 symmetrization in the glue module; and the pointwise rational equality of explicit vs closed tables after dividing the integer full symmetrizer by 32. In the RS gravity stack this is bookkeeping infrastructure for the 4D Regge midpoint $m^2$ TT identity, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.