swap12ClassTable
plain-language theorem explainer
Explicit 15-entry lookup table for how the Regge edge-stencil classes transform under the coordinate transposition that swaps axes 1 and 2. Cited when checking that the type-(1,3) full-star deficit class kernel is invariant under this hinge-fixing symmetry. The definition is pure case enumeration on Fin 15, written for kernel-decidable rewriting.
Claim. The map $\tau_{12}:\{0,\ldots,14\}\to\{0,\ldots,14\}$ with values $0\mapsto 0$, $1\mapsto 3$, $2\mapsto 4$, $3\mapsto 1$, $4\mapsto 2$, $5\mapsto 5$, $6\mapsto 6$, $7\mapsto 7$, $8\mapsto 8$, $9\mapsto 11$, $10\mapsto 12$, $11\mapsto 9$, $12\mapsto 10$, $13\mapsto 13$, $14\mapsto 14$, encoding the action of swapping axes $1$ and $2$ on the fifteen Regge edge-stencil classes.
background
This module builds the type-(1,3) periodic-lattice star deficit class kernel for 4D Regge calculus: the triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full Freudenthal star in the origin unit cube. The ambient classification layer supplies a 15-class edge stencil; classes label orbit types of edges under the lattice symmetry used to assemble the star deficit.
Among the module gates is invariance of the full-star deficit class kernel under the hinge-fixing transposition $1\leftrightarrow 2$ of the three free axes ${1,2,3}$. The abstract class map for that transposition is named separately; the present definition is its fully expanded lookup table, written so that kernel tactics (decide, simp, fin_cases) can discharge equalities without unfolding a more abstract permutation construction.
Downstream, the table is identified with the abstract swap map and then used to prove that the seven-class full-star kernel values on classes $(1,3,5,7,9,11,13)$ are unchanged under the swap.
proof idea
Pure definition by pattern match: fifteen clauses on Fin 15, no proof body. Each input class index is sent to the class index of its image under axis swap $1\leftrightarrow 2$. The companion theorem swap12Class_eq_table later certifies agreement with the abstract swap12Class by fin_cases and decide.
why it matters
Sits inside deliverable A of the type-(1,3) star kernel campaign: the hinge-fixing transposition gate. Parent theorems are swap12Class_eq_table (table equals abstract swap) and fullStarClassKernel_swap12 (full-star class kernel is invariant under the swap). That invariance is one of the six listed gates (nonvacuity, $1\leftrightarrow 2$ transposition, uniform-scaling decoy, homothety stationarity, flatness, derivative package).
In the broader QG path it is a small but load-bearing kernel artifact: without a decidable class action, the star deficit symmetry under lattice axis permutation cannot be machine-checked. It does not itself touch Einstein–Hilbert recovery, S_RS_converges_EH_4d, or gap_action_recovery; those remain explicitly open per the module doc. Transport of the whole kernel to the complementary type-(3,1) hinge is also still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.