fullStarClassKernel_swap23
plain-language theorem explainer
The full-star deficit class kernel on the 15 edge-length classes is invariant under the axis swap that exchanges coordinates 2 and 3. Anyone assembling the seed-hinge Regge star Hessian or checking lattice symmetry gates cites this. The proof is a finite case split on the seven support classes, using that the swap is an involution and that the kernel vanishes off-support.
Claim. For every edge-length class $d \in \{0,\ldots,14\}$, the full-star deficit class kernel evaluated at the image of $d$ under the coordinate swap $2 \leftrightarrow 3$ equals the kernel at $d$: $K_{\star}(\sigma_{23}(d)) = K_{\star}(d)$.
background
This module sits in the QG full-theory campaign for 4D Regge calculus on the integer lattice. The seed triangle hinge is ${0, e_0, e_0+e_1}$; its full periodic Freudenthal star comprises four unit cubes and six incident 4-simplices. Edge-length variations are organized into a 15-class stencil.
The full-star deficit class kernel $K_{\star}:\mathrm{Fin},15\to\mathbb{R}$ is the sparse map supported on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$. Off those classes it is zero (fullStarClassKernel_zero_off). The map swap23Class is the induced action on the 15 classes of the lattice isometry that swaps axes 2 and 3; it is an involution on $\mathrm{Fin},15$.
The module already records star enumeration, the flat cosine multiset, and the flatness gate (star angle sum exactly $2\pi$). Swap-$2\leftrightarrow 3$ invariance is one of the named symmetry gates on the kernel.
proof idea
First record by decide that swap23Class is an involution and compute its action on the seven support indices: $2\mapsto 2$, $3\leftrightarrow 7$, $6\leftrightarrow 10$, $11\mapsto 11$, $14\mapsto 14$.
Case-split on whether $d$ equals each support index. On support, rewrite by the tabulated swap and reduce by definitional equality of kernel values (pairs that swap carry matching signs). Off support, the involution identity pushes the inequalities forward: $\sigma_{23}(d)$ misses every support index as well. Apply fullStarClassKernel_zero_off on both sides to get $0=0$.
why it matters
Module deliverable A lists five gates on the full-star deficit class kernel; this theorem discharges the swap-$2\leftrightarrow 3$ symmetry gate for the seed-hinge star. Downstream, ReggeHinge4DStarKernel22.fullStarClassKernel_swap23 reuses the same statement in a sibling kernel variant (there proved by exhaustive fin_cases).
In the broader Recognition gravity stack this is a lattice-symmetry check on the discrete curvature kernel before Hessian assembly, not yet Einstein–Hilbert recovery. The module doc is explicit that other hinge orbits remain open and that this does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D. It is the next kernel-checked increment after the dihedral cosine calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.