swap12Class
plain-language theorem explainer
Axis swap 1↔2 acting on the 15 edge-stencil classes of the 4D Regge lattice, as a permutation of class indices. Cited by anyone checking hinge-fixing symmetry of the type-(1,2) full-star deficit kernel. Built by bit-swapping the class mask and re-indexing; the Fin bounds come from the companion inequality via omega.
Claim. For each stencil class index $d \in \{0,\ldots,14\}$, map $d$ to the unique class index whose bit-mask is obtained by exchanging bits $1$ and $2$ of the mask of $d$ (the integer $d+1$), then subtracting one.
background
The module builds the full periodic-lattice star deficit class kernel for the type-(1,2) triangle hinge ${0, e_0, e_0+e_1+e_2}$ (masks $0,1,7$) in 4D Regge calculus on the integer lattice. The 15 nonzero edge displacements of the 4-cube form the stencil classes; each class $d$ has bit-mask $\mathrm{maskOf}(d)=d+1\in{1,\ldots,15}$.
The companion map on masks exchanges bits 1 and 2 (axes $1\leftrightarrow 2$), leaving bits 0 and 3 fixed. That is an $S_3$ generator that preserves the hinge vertex set. A separate bounds lemma states that the swapped mask of any class still lies in ${1,\ldots,15}$.
This definition packages that mask permutation back into a map on $\mathrm{Fin},15$, so downstream kernel identities can be stated purely in class indices.
proof idea
Definitional construction, not a tactic proof. Form the subtype element whose value is $\mathrm{swap12Mask}(\mathrm{maskOf},d)-1$. The proof obligation that this lies in ${0,\ldots,14}$ is discharged by invoking the bounds lemma (strict positivity and upper bound $\le 15$ of the swapped mask) and closing with omega.
why it matters
Supplies the class-level action of the hinge-fixing axis swap used by the swap-symmetry gate on the full-star deficit kernel. The immediate parent is the theorem that the type-(1,2) full-star class kernel is invariant under this map (proved by fin_cases and rfl). The same pattern is mirrored in the type-(1,3) kernel module, which also equates the map to an explicit lookup table.
In the module's deliverable list this is the combinatorial half of gate (5): nonvacuity, swap-$1\leftrightarrow 2$ hinge-fixing symmetry, uniform-scaling decoy, and homothety stationarity. It does not itself evaluate deficits; it only renames classes so the kernel table can be checked for invariance. Complements the type-(1,1) seed orbit already treated in the prior star-kernel module; type-(2,1) and the remaining hinge orbits stay open, as does flat Hessian assembly and $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.