swap12Class_eq_table
plain-language theorem explainer
The axis-1↔2 transposition on the fifteen Freudenthal edge-class indices agrees pointwise with an explicit fifteen-entry lookup table. Anyone proving hinge-fixing invariance of the type-(1,3) full-star deficit kernel cites this equality. The proof is a one-line finite case split with kernel-decidable equality on each residue.
Claim. For every class index $d\in\{0,\ldots,14\}$, the class obtained by swapping coordinate axes $1$ and $2$ in the mask of $d$ equals the explicit table value $T(d)$, where $T(0)=0$, $T(1)=3$, $T(2)=4$, $T(3)=1$, $T(4)=2$, $T(5)=5$, $T(6)=6$, $T(7)=7$, $T(8)=8$, $T(9)=11$, $T(10)=12$, $T(11)=9$, $T(12)=10$, $T(13)=13$, $T(14)=14$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-(1,1) star kernel and the orbit classification layer. It treats the type-(1,3) triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the origin unit cube.
Edge classes live in a fixed $15$-class stencil. The map that swaps axes $1$ and $2$ acts on masks and therefore induces a permutation of class indices: apply the mask swap, subtract one, and land back in $\mathrm{Fin},15$. An explicit table records that permutation so later kernel equalities can be discharged by simp rather than by unfolding the mask arithmetic.
The surrounding deliverable already enumerates the six Kuhn simplices containing the hinge, proves their flat cosines are all $1/2$, and closes the flatness gate $6\cdot\arccos(1/2)=2\pi$. The swap table is the discrete bookkeeping step needed for the hinge-fixing gate on the full-star deficit class kernel.
proof idea
One-line wrapper: case-split on the fifteen values of $d:\mathrm{Fin},15$, then run kernel-decidable equality on each concrete numeral. No algebraic lemmas are invoked; both sides reduce to closed numerals once the table and the mask-swap definition are unfolded.
why it matters
The equality is the rewrite step inside fullStarClassKernel_swap12, which states that the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ is invariant under the hinge-fixing transposition $1\leftrightarrow 2$ of the spatial axes ${1,2,3}$. That invariance is one of the six named gates listed in the module deliverable (nonvacuity, hinge-fixing, uniform-scaling decoy, homothety stationarity, flatness, star enumeration).
Downstream status flags record the kernel as closed while leaving type-$(3,1)$ transport and flat Hessian assembly open. The result therefore sits strictly inside the type-$(1,3)$ star kernel; it does not touch the Einstein–Hilbert recovery gap or the global $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence claim. In the broader Recognition gravity stack it is pure discrete geometry bookkeeping that lets the deficit multiset $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$ be reused after axis swap without recomputing Gram projections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.