axisMask
plain-language theorem explainer
Assigns to each of the four coordinate axes the bit mask of its standard basis vector: axis i maps to 2^i. Anyone encoding Freudenthal 4-cube vertices as subsets of {0,1,2,3} cites this. The body is the literal power-of-two formula on the underlying natural number of a Fin 4 index.
Claim. For each axis index $i \in \{0,1,2,3\}$, the axis mask is the natural number $2^i$, i.e. the bit mask of the standard basis vector $e_i$ in the 4-cube.
background
The module builds the combinatorial skeleton of 4D Regge hinge incidence on the Freudenthal (Kuhn) triangulation of the 4-cube. Vertices of each 4-simplex are nested partial sums of a permutation of the four axes; each vertex is stored as a bit mask in ${0,\ldots,15}$.
An axis mask is the one-hot encoding of a single coordinate direction. The four values are therefore $1,2,4,8$. Upstream bit maps booleans to ${0,1}$ and is the atomic building block of the same mask arithmetic on the periodic Freudenthal torus; here the power-of-two form is written directly.
The 15-class edge stencil from ReggeEdgeStencil4D is imported unchanged. Axis masks feed the five nested vertex masks of each of the 24 monotone 4-simplices.
proof idea
Pure definition: evaluate $2$ raised to the underlying natural number of the Fin 4 index. No lemmas, no tactics.
why it matters
Supplies the one-hot generators used by vertexMask, which builds the five nested Freudenthal vertices along each of the 24 simplices (masks in ${0,\ldots,15}$). Those vertex masks determine local edge pairs, edge-class incidence, and the seed-hinge orbit (triangle masks $0,1,3$).
The module is deliverable B of the QG flat-Hessian campaign: combinatorial support and incidence multiplicities only. Axis masks are the atomic coordinate labels that make the 24-permutation enumeration and the three decoy classes well-defined. They do not touch the still-OPEN per-hinge deficit or area kernels, nor the convergence claim $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.