fullStarClassKernel_swap01
plain-language theorem explainer
The type-(2,2) full-star deficit class kernel on the 15-class edge stencil is invariant under the axis swap 0↔1. Lattice-gravity and Regge-calculus workers checking residual hinge symmetries cite this gate. Proof is a one-line exhaustive split on Fin 15 with definitional equality on each case.
Claim. For every edge-stencil class $d\in\{0,\ldots,14\}$, the type-(2,2) full-star class kernel satisfies $K(\mathrm{swap}_{0\leftrightarrow 1}(d))=K(d)$, where $\mathrm{swap}_{0\leftrightarrow 1}$ is the class map induced by exchanging coordinate axes 0 and 1.
background
The module closes the full periodic Freudenthal star for the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) inside the 4D axis-aligned unit-cube triangulation. Exactly four (cube translate, Kuhn simplex) pairs meet the hinge; each carries flat cosine 0, so the star angle sum is exactly $2\pi$.
The full-star class kernel is the closed-form map $\mathrm{Fin},15\to\mathbb{R}$ that records the linearized deficit contribution of that complete star on each of the 15 stencil classes. In this module its nonzero values are $\pm 1$ on five classes. The companion map $\mathrm{swap}_{01}$ sends a class to the class of the edge mask obtained by exchanging axes 0 and 1; that swap fixes the hinge vertex set.
Analogous kernels already exist for the (1,1), (1,2) and (1,3) orbits. The present statement is the (2,2) instance of the swap-symmetry gate listed among the module deliverables.
proof idea
One-line wrapper: fin_cases d expands the goal into fifteen concrete instances of Fin 15. On each instance both sides of the equality reduce by rfl to the same real literal, because the kernel table is invariant under the permutation of classes induced by the axis swap. No lemmas beyond the definitions of the kernel and of swap01Class are required.
why it matters
Among the five explicit gates of the type-(2,2) star-kernel deliverable, this discharges swap-$0\leftrightarrow 1$ symmetry. The module sits in the QG full-theory campaign immediately after the (1,1) seed orbit (ReggeHinge4DStarKernel); confirming that the closed-form kernel respects the residual lattice symmetry of the hinge is a local consistency check before any global Hessian assembly.
No downstream consumers are wired yet (used_by is empty). The result does not touch the still-open targets S_RS_converges_EH_4d or gap_action_recovery, nor does it reverse-engineer continuum weights. It simply certifies one symmetry gate on the (2,2) orbit so later assembly steps can treat the kernel as equivariant under that residual action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.