sym4Z
plain-language theorem explainer
Integer order-4 flip average of a six-index table C on Fin 4: average the four swaps of the first two index pairs (a↔b and c↔d). Gravity analysts cite it when building the midpoint m² TT kernel certificates in 4D Regge calculus. The body is a pure definition: sum four permutations and divide by 4 in Int.
Claim. Given an integer map $C$ on six indices in $\{0,1,2,3\}$ and indices $a,b,c,d,i,j$, set $$\mathrm{sym}_4(C)_{abcdij}=\frac{1}{4}\bigl(C_{abcdij}+C_{bacdij}+C_{abdc ij}+C_{badc ij}\bigr)\in\mathbb{Z}.$$
background
The ambient module holds generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge analysis. Certificates are built from integer fold tables (scale-32) so that kernel membership can be decided by decide alone, without native evaluation.
The six-index integer array $C$ packages local Hessian or Bloch-type contributions on a 4-simplex edge/face labeling. Indices $a,b$ and $c,d$ label the two pairs that are flipped under the discrete residual symmetries of the midpoint TT projector; $i,j$ are spectator indices.
sym4Z is the first layer of that discrete symmetrization: the order-4 average over the Klein four-group generated by swapping within each pair. The next layer, symFullZ, averages that result with the swapped-pair copy to reach the full order-8 symmetrizer used in the glue lemmas.
proof idea
Definition only: evaluate $C$ at the four index tuples obtained by independently swapping $a$ with $b$ and $c$ with $d$, add the four integers, and divide by 4 in Int. No lemmas are invoked.
why it matters
Parent consumers are symFullZ (full order-8 average built from two sym4Z calls) and the glue scaling theorems sym4_scale and symFull_scale. Those theorems move the factor $1/32$ through the average so that rational kernel identities match the integer certificate tables. In the Regge midpoint $m^2$ TT pipeline this is bookkeeping that keeps the discrete residual symmetry exact before the kernel decide step. It does not itself encode a Recognition forcing step (T0–T8); it is infrastructure inside the 4D gravity analysis layer that certifies the TT mass-squared identity on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.