coordPermOf
plain-language theorem explainer
Turns a lexicographic index in {0,...,23} into the corresponding coordinate permutation of the four axes of the unit 4-cube. Anyone transporting triangle-hinge data under the S₄ lattice symmetry cites this map. The body is a thin unpack of the existing four-tuple enumeration of permutations.
Claim. For each index $p \in \{0,\ldots,23\}$, return the map $\sigma_p:\{0,1,2,3\}\to\{0,1,2,3\}$ equal to the $p$-th lexicographic permutation of the four coordinate axes (same order as the axis four-tuple enumeration).
background
The ambient module classifies triangle hinges in one unit 4-cube Kuhn triangulation up to lattice translation and triangulation-preserving symmetry. Combinatorics only: difference-mask types, cell counts, and S₄ orbits of hinges. It does not evaluate star kernels or assemble the flat Hessian.
The upstream axis enumeration lists all 24 permutations of Fin 4 as four-tuples $(\sigma(0),\sigma(1),\sigma(2),\sigma(3))$ in lexicographic order. Many downstream constructions need the same data as a function Fin 4 → Fin 4 (axis-to-axis map), not a product type.
Coordinate permutation is the lattice action that preserves hinge type (popcount pairs of disjoint difference masks) and is transitive on each realizable type. That action is the combinatorial engine for orbit transport of star kernels and Bloch-folded incidence data.
proof idea
Definitional adapter, not a proof. On input index $p$, call the upstream four-tuple enumeration, then pattern-match the domain axis $i\in{0,1,2,3}$ and project the matching component of the tuple. No lemmas, no tactics: pure structural unpack so callers can write $\sigma(i)$ instead of tuple projections.
why it matters
This is the shared S₄ handle for the whole 4D Regge orbit-transport stack. Downstream, offset transport rewrites lattice offsets by $\mathrm{off}'(\sigma(j))=\mathrm{off}(j)$; local incidence applies the same map to seed-frame offsets; Bloch fold permutes 15-class masks; orbit covering tests whether a candidate perm sends a type representative difference pair to a given slot's masks; star-edge origin transport uses it likewise.
In the module's deliverable list it supports item 3 (lattice orbits under coordinate permutation) and the later merge to four orbits under $S_4\rtimes{\mathrm{id},\mathrm{complement}}$. It is pure scaffolding for the QG campaign's combinatorial prerequisite: assembling the flat Hessian from per-orbit star kernels. It does not itself close gap_action_recovery or S_RS → EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.