permMask
plain-language theorem explainer
Coordinate permutation acts on 4-bit vertex masks by sending each set bit i to bit σ(i). Orbit-classification and Bloch-fold code cite it whenever S₄ moves difference pairs or absolute triples inside the Kuhn 4-cube. The body is a four-term bit rebuild: test bits 0..3 of m and place powers of two at the permuted indices.
Claim. Given a map $\sigma:\{0,1,2,3\}\to\{0,1,2,3\}$ and a natural number $m$ read as a 4-bit mask, define the permuted mask by moving each set bit $i$ of $m$ to bit position $\sigma(i)$: $$\mathrm{perm}(\sigma,m)=\sum_{i=0}^{3}\mathbf{1}_{\mathrm{bit}\,i\,\mathrm{of}\,m}\,2^{\sigma(i)}.$$
background
The module classifies triangle hinges in one unit 4-cube Kuhn triangulation up to lattice translation and triangulation-preserving symmetry. Vertex sets are 4-bit masks in ${0,\ldots,15}$; a triangle is a monotone chain of three masks whose successive XOR differences $(a,b)$ are disjoint and nonzero. Hinge type is the popcount pair $(|a|,|b|)$ in ${(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$.
Coordinate permutations of the four axes act on these masks by relocating bits. Upstream, permAxes lists all 24 elements of $S_4$ in lexicographic order as 4-tuples $(\sigma(0),\sigma(1),\sigma(2),\sigma(3))$. The present definition is the bit-level action of any such $\sigma$ on a single mask, the primitive used to push difference pairs and absolute triples around the cell.
Scope is combinatorics only: no star kernels, no flat Hessian, no continuum limit of the 4D Regge action.
proof idea
Pure definition, not a theorem. For each source bit index $i\in{0,1,2,3}$, test whether bit $i$ of $m$ is set; if so add $2^{\sigma(i)}$, else add zero. Sum the four contributions. No lemmas are invoked; the expression is the explicit bit-permutation formula matching the permAxes convention.
why it matters
This is the $S_4$ action on masks that drives the lattice-orbit story in the module deliverable: every realizable disjoint difference pair appears, and coordinate permutation preserves type and is transitive on each type (six orbits before complement). Downstream, coordPerm_preserves_pop and coordPerm_preserves_type prove popcount (hence type) is invariant under this map; permDiffPair and permTriple lift it to pairs and absolute triples. Outside the module, permClass in the Bloch-fold pipeline uses it to conjugate the 15 nonzero edge masks under the 24 Kuhn permutations.
In the QG campaign this is pure scaffolding for assembling the flat Hessian from per-orbit star kernels. It does not itself evaluate kernels or close gap-action recovery; it only makes the $S_4$ symmetry of 4-bit masks a named, reusable operation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.