swap12Class
plain-language theorem explainer
The map on the fifteen edge-displacement classes that swaps spatial axes 1 and 2 inside each class bit-mask. Gravity analysts cite it when proving the type-(1,3) full-star deficit kernel is invariant under the hinge-fixing transposition 1↔2. Construction is mask-of, bit-swap, reindex by minus one, with the Fin-15 bound discharged by omega from the mask bounds lemma.
Claim. For each class index $d \in \{0,\ldots,14\}$, let $m=d+1$ be its bit-mask in $\{1,\ldots,15\}$. The axis-$1\leftrightarrow 2$ image of $d$ is the unique class whose mask is obtained from $m$ by exchanging bits 1 and 2 (the $e_1$ and $e_2$ axes), i.e. the integer $\mathrm{swapMask}_{12}(m)-1$ viewed in $\{0,\ldots,14\}$.
background
This module is the QG full-theory kernel for the type-(1,3) triangle hinge on the 4D periodic Freudenthal lattice. Absolute masks are ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Edge displacements are classified by the 15 nonzero bit-masks in ${1,\ldots,15}$, indexed as Fin 15 via the stencil map that sends class $d$ to mask $d+1$.
The hinge-fixing gate in the module brief is the transposition of axes ${1,2,3}$ that swaps coordinates 1 and 2. At the mask level that swap is the bit permutation exchanging bits 1 and 2 while fixing bits 0 and 3. The same construction already appears in the type-(1,2) star-kernel sibling; this definition is the type-(1,3) copy, wired to the local mask and bounds lemmas.
Upstream, the mask-of map is pure reindexing ($d \mapsto d+1$). The mask-level swap rebuilds the integer from the four tested bits with weights $1,4,2,8$ in bit order $0,1,2,3$, which is exactly the $1\leftrightarrow 2$ exchange. Bounds guarantee the result stays in ${1,\ldots,15}$.
proof idea
Definitional construction, not a tactic proof. Apply the stencil mask-of map to $d$, feed the resulting natural into the bit-level $1\leftrightarrow 2$ swap, subtract one to recover a class index, and pack into Fin 15. The subtype bound is a one-line have from the local mask-bounds lemma, closed by omega. No case split and no table lookup at this layer; equality to the explicit fifteen-entry table is a separate decidable theorem.
why it matters
The module deliverable list includes the hinge-fixing transposition $1\leftrightarrow 2$ among the gates on the full-star deficit class kernel (values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$ on classes $(1,3,5,7,9,11,13)$). This map is the class-level action of that transposition.
Downstream, the invariance theorem states that the full-star class kernel is unchanged under the map, proved by rewriting through the table equality and finite case analysis. The same pattern is mirrored in the type-(1,2) star-kernel module. The construction does not itself evaluate deficits; it only supplies the symmetry action those gates consume.
In the broader campaign this is one kernel-checked increment after the type-(1,1) seed orbit and the orbit classification layer. It does not close flat Hessian assembly, $S_{RS}\to$ Einstein–Hilbert convergence, or gap-action recovery, and transport of the kernel to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.