permAxes
plain-language theorem explainer
Explicit table of all 24 permutations of the four coordinate axes, indexed by Fin 24 in lexicographic order. Each entry is the 4-tuple (σ(0),σ(1),σ(2),σ(3)). Gravity analysts cite it as the combinatorial spine of the Freudenthal 4-cube triangulation: the 24 monotone 4-simplices. The body is a pure case table plus an absurdity clause for out-of-range indices.
Claim. The map $\mathrm{permAxes}\colon\{0,\ldots,23\}\to(\mathbb{Z}/4\mathbb{Z})^4$ sends each index $s$ to the ordered 4-tuple $(\sigma(0),\sigma(1),\sigma(2),\sigma(3))$ of the $s$-th permutation of $\{0,1,2,3\}$ in lexicographic order. Indices outside $0..23$ are unreachable and yield a contradiction.
background
This module builds the combinatorial skeleton for the flat Hessian of the 4D Regge action on a Freudenthal (Kuhn) triangulation of the 4-cube. The 24 monotone 4-simplices are exactly the permutations of the four axes; each simplex is a nested chain of five vertices obtained by successively adding the permuted basis vectors.
The imported 15-class edge stencil (ReggeEdgeStencil4D) labels edges by bitmasks on the four axes. Incidence of a hinge (triangle) in a simplex is read off by asking which local edge masks appear after the axis permutation is applied. The present table is the raw enumeration that later definitions project to single-axis images and to mask-level actions.
Local setting (module doc): deliverable B of the QG campaign. Combinatorial support and incidence multiplicities are proved; per-hinge deficit and area kernels remain OPEN parameters. Nothing here evaluates the flat second variation or recovers Einstein–Hilbert weights.
proof idea
Definition by exhaustive pattern match on Fin 24. Cases 0 through 23 list the 24 ordered 4-tuples in lex order, starting from $(0,1,2,3)$ and ending at $(3,2,1,0)$. The residual constructor ⟨n+24, h⟩ is discharged by absurd plus omega, since no inhabitant of Fin 24 can carry a value $\ge 24$. No lemmas are invoked; the table is the content.
why it matters
Parent consumers are permOf (axis image $\sigma(i)$ for simplex $s$), coordPermOf (same table as a function Fin 4\to Fin 4), and permMask (push a bit-mask forward under a coordinate permutation). Together they feed the seed-hinge orbit count, the 15-class incidence multiplicities, and the nonvacuity/symmetry/decoy statements of the Freudenthal hinge analysis.
In the Recognition gravity stack this is the discrete geometry layer beneath any later claim that the RS action converges to Einstein–Hilbert in 4D. The module doc is explicit: the table does not complete the flat Hessian, does not prove $S_{\mathrm{RS}}$ converges to EH, and does not flip gap_action_recovery. It only locks the combinatorial support on which those OPEN kernels will later sit. Framework landmark: $D=3$ spatial plus time gives the 4-cube whose $4!=24$ ordered simplices appear here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.