partialDeficitClassKernel_swap23
plain-language theorem explainer
The two-simplex partial deficit class kernel at flat is invariant under the incidence-layer axis swap that exchanges coordinates 2 and 3. Anyone assembling hinge gradients on the 15 edge classes of the Freudenthal seed can cite this to move support freely between the swapped classes. The proof is a finite case split on the three active classes (3, 7, 11), using the known kernel values and the involution property of the swap.
Claim. For every edge class $d \in \{0,\ldots,14\}$, the two-simplex partial deficit class kernel satisfies $K(\sigma_{2\leftrightarrow 3}(d)) = K(d)$, where $\sigma_{2\leftrightarrow 3}$ is the class map induced by swapping axes $2$ and $3$ in the incidence mask, and $K$ is the flat gradient $\partial(2\pi - \theta_0 - \theta_1)/\partial\ell^2$ assembled over the two seed simplices.
background
This module sits in the QG full-theory campaign as the next kernel-checked increment after the flat hinge kernel. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum remains open.
The partial deficit class kernel $K:\mathrm{Fin},15\to\mathbb{R}$ is the sum of the two single-simplex deficit kernels assembled onto the 15 global edge classes via each simplex's local-edge-class table. At flat it is supported only on classes $3$, $7$, and $11$, with values $(-1/2,-1/2,+1/2)$ respectively, and vanishes elsewhere.
The map $\sigma_{2\leftrightarrow 3}$ (swap23Class) is the class image of the axis swap $2\leftrightarrow 3$ on the incidence mask. It is an involution on $\mathrm{Fin},15$ and swaps classes $3$ and $7$ while fixing $11$.
proof idea
First record by decide that $\sigma$ is an involution and that $\sigma(3)=7$, $\sigma(7)=3$, $\sigma(11)=11$. Case-split on whether $d$ equals $3$, $7$, or $11$.
If $d=3$, rewrite with $\sigma(3)=7$ and apply the known evaluations $K(7)=-1/2$ and $K(3)=-1/2$. The $d=7$ case is symmetric. If $d=11$, $\sigma$ fixes the class so equality is immediate.
Off those three classes, the involution plus the fixed-point facts imply $\sigma(d)$ is also off ${3,7,11}$. Both sides therefore vanish by the off-support vanishing lemma, so they agree.
why it matters
The module's deliverable list explicitly flags "symmetry" of the partial deficit kernel under the hinge-fixing axis swap as part of the checked package (alongside nonvacuity and decoy). This theorem discharges that item: $K$ is unchanged when axes $2$ and $3$ are exchanged at the incidence layer.
No downstream consumers are wired yet (used_by is empty). The result is infrastructure for later orbit sums and Hessian assembly on the full lattice, where one must know that class-level gradients transform consistently under the residual symmetry of the seed hinge.
It does not close the open items named in the module doc: the full lattice orbit sum, the flat Hessian of the 4D Regge action, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery. Those remain separate campaign steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.