permTriple
plain-language theorem explainer
Applies an S₄ coordinate permutation (indexed by Fin 24) componentwise to an absolute vertex-mask triple in the Kuhn 4-cube. Used wherever absolute triangle hinges must be moved under lattice coordinate relabeling, notably to separate S₄-orbits of type-(1,1) hinges. The body is a three-component application of mask permutation along the lexicographic axis map.
Claim. Given a coordinate permutation $\sigma$ of $\{0,1,2,3\}$ (one of the $24$ elements of $S_4$) and an absolute triple of vertex masks $(m_0,m_1,m_2)$, return $(\sigma\cdot m_0,\,\sigma\cdot m_1,\,\sigma\cdot m_2)$, where $\sigma$ acts on a mask by sending each set bit $i$ to bit $\sigma(i)$.
background
This module classifies triangle hinges in one unit 4-cube under the Kuhn/Freudenthal triangulation. Scope is pure combinatorics of absolute and difference-mask triples: no star kernels, no flat Hessian, no continuum limit. Vertex sets are encoded as 4-bit masks; a triangle is a monotone chain of three masks.
Coordinate permutations are the $S_4$ action on the four axis bits. The helper that lists all $24$ permutations in lexicographic order supplies a map $\mathrm{Fin},4\to\mathrm{Fin},4$; mask permutation rebuilds a mask by relocating each set bit under that map. Absolute triples live in the fixed cell (not quotiented by lattice translation), so the same difference type can still split into several absolute orbits.
The surrounding campaign enumerates $240$ oriented triangle slots, six difference-popcount types, and lattice orbits under $S_4$ and under $S_4\rtimes{\mathrm{id},\mathrm{complement}}$. Absolute (non-translated) orbits are a finer invariant needed for the honest refinement that $S_4$ is not transitive on type-$(1,1)$ hinges inside the cell.
proof idea
Definition only: unpack the input triple and apply mask permutation under the coordinate map of the given $S_4$ index to each of the three components. No lemmas, no tactics.
why it matters
Feeds the honest-refinement theorem that coordinate permutation does not act transitively on absolute type-$(1,1)$ triangles: the seed ${0,1,3}$ and the interior chain ${1,3,7}$ share difference type $(1,1)$ yet no $p\in\mathrm{Fin},24$ sends one absolute triple to the other. That statement is written as a universal quantification over this map.
In the QG full-theory campaign this is a combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels. Difference-mask orbits collapse under lattice translation; absolute orbits keep cell-internal distinctions that star-kernel assembly must not identify. The module explicitly does not evaluate those kernels or close gap_action_recovery; this definition only supplies the $S_4$ action used to certify the split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.