fullStarClassKernel_swap12
plain-language theorem explainer
The type-(1,3) full-star deficit class kernel is invariant under the hinge-fixing transposition that swaps axes 1 and 2 in the edge-class mask. Anyone auditing the (1,3) star gates or the status flags cites this equality. The proof rewrites the swap through its explicit table, then exhausts Fin 15 by cases and simplifies against the kernel definition.
Claim. For every edge-class index $d\in\{0,\ldots,14\}$, the type-$(1,3)$ full-star deficit class kernel satisfies $K(\sigma_{1\leftrightarrow 2}(d))=K(d)$, where $\sigma_{1\leftrightarrow 2}$ is the class map induced by swapping coordinate axes $1$ and $2$ in the underlying mask of $d$.
background
This module is the next kernel-checked increment in the Regge 4D QG campaign after the type-(1,1) seed orbit. 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 in the origin unit cube.
The full-star deficit class kernel $K:\mathrm{Fin},15\to\mathbb{R}$ assigns to the seven active classes $(1,3,5,7,9,11,13)$ the values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$ (and zero elsewhere). The map $\sigma_{1\leftrightarrow 2}$ is the induced action on class indices of the coordinate transposition that swaps axes $1$ and $2$ inside the three spatial axes ${1,2,3}$ of the hinge; it is realized by applying the mask-level swap and renormalizing to a $\mathrm{Fin},15$ index, with an explicit lookup table for decidability.
Parallel kernels exist for the type-(1,1) and type-(1,2) orbits; each carries its own swap-invariance statement. The module imports the Freudenthal incidence layer, the 15-class stencil, and the Gram-projection cosine calculus without redefining their APIs.
proof idea
Rewrite the swap map through its explicit table equality swap12Class_eq_table. Then case-split on the fifteen values of $d$ via fin_cases and discharge each goal by simp against the piecewise definition of the type-(1,3) kernel and the swap table. No analytic identities are needed: both sides are concrete real constants on each class.
why it matters
This equality is gate 5 of deliverable A in the module doc: the hinge-fixing transposition $1\leftrightarrow 2$ on axes ${1,2,3}$. It is recorded in hinge4DStarKernel13Status_flags, which packages the closed star-enumeration, flatness, and full-star-kernel flags for the type-(1,3) orbit. The same pattern appears for the type-(1,2) kernel; the two statements sit side-by-side in the campaign ledger.
In the broader Recognition gravity stack the kernel feeds the flat Hessian assembly over hinges, which remains open, as does transport of this kernel to the complementary type-(3,1) orbit by mask complement. The result does not touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence or gap-action recovery; it only certifies that the discrete deficit class data are symmetric under the residual hinge automorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.