permDiffPair
plain-language theorem explainer
Applies a coordinate permutation of the four axes to a pair of difference masks, returning the permuted pair. Used throughout the 4D Regge hinge orbit machinery to test S₄-transitivity on realizable (a,b) types and to match slots to canonical orbit representatives. The body is a one-line pair of mask permutations.
Claim. Given a coordinate map $\sigma:\{0,1,2,3\}\to\{0,1,2,3\}$ and two natural numbers $a,b$ (read as 4-bit masks), return the pair $(\sigma\cdot a,\,\sigma\cdot b)$, where each mask is rewritten by sending bit position $i$ to bit position $\sigma(i)$.
background
This module classifies triangle hinges in one unit 4-cube Kuhn triangulation up to lattice translation and triangulation-preserving symmetry. Every index-triple triangle is a monotone mask chain whose type is the popcount pair $(|a|,|b|)$ of its disjoint nonzero difference masks.
Masks live in ${0,\ldots,15}$. The Hamming weight maskPop counts set bits among the four low bits. A coordinate permutation $\sigma$ acts on a mask by relocating each set bit $i$ to position $\sigma(i)$ (the map permMask). Difference pairs $(a,b)$ label hinge geometry after translation is quotiented out.
The ambient $S_4$ action on bit positions is the combinatorial symmetry used to prove that each realizable type forms a single lattice orbit (six orbits before complement, four after).
proof idea
Pure definition: return the ordered pair obtained by applying permMask to each of $a$ and $b$ under the same $\sigma$. No proof obligations.
why it matters
This is the atomic $S_4$ action on difference pairs that the orbit-classification and Bloch-transport layers call repeatedly. Downstream, inOrbitOfRep decides whether $(a,b)$ lies in the orbit of a type's canonical representative by searching for a $p$ with permDiffPair (coordPermOf p) rep = (a,b). The covering test coversOrbitSlot and the packaging theorem orbitCoveringPerm_spec use the same equality to certify that a chosen coordinate permutation sends the orbit seed to a concrete cell slot $(s,t)$.
In the QG campaign this is pure combinatorics: a prerequisite for assembling the flat Hessian from per-orbit star kernels. It does not evaluate kernels or prove Einstein–Hilbert recovery; it only makes the six (resp. four) hinge orbits transportable under coordinate permutation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.