kernel13Sign
plain-language theorem explainer
Integer sign pattern on the fifteen edge classes that multiplies the type-(1,3) star deficit kernel in the zero-momentum 4D Regge Hessian. Anyone assembling orbit-weighted second variations of the flat Regge action cites it when evaluating (1,3) and (3,1) slots. The body is a pure case table: seven nonzero entries, rest zero.
Claim. Define an integer-valued sign map on edge classes $d \in \{0,\ldots,14\}$ by $\mathrm{sgn}_{13}(d) = -1$ for $d \in \{1,3,7,13\}$, $\mathrm{sgn}_{13}(d) = +1$ for $d \in \{5,9,11\}$, and $\mathrm{sgn}_{13}(d) = 0$ otherwise. This is the committed sign factor for the type-$(1,3)$ (equivalently type-$(3,1)$) star-class kernel on $\mathrm{Fin}\,15$.
background
The module assembles the flat second-variation quadratic of the 4D Regge action at zero momentum. Per-orbit star deficit kernels (imported from the hinge-star kernel modules) are combined with Heron area gradients of the four committed flat triangle shapes, then weighted by $S_4$ orbit counts $72/48/48/24/24/24$.
Edge classes live on $\mathrm{Fin},15$. Complement transport $m \mapsto m \oplus 15$ preserves difference masks, so the type-$(3,1)$ star kernel equals the type-$(1,3)$ kernel on those fifteen indices. The present map supplies the integer signs that sit in front of that shared kernel when forming orbit slot coefficients.
Scope is strictly the constant (zero-momentum) edge-class perturbation per cell. Finite-momentum Bloch phase folding across hinge translates remains open.
proof idea
Definition by exhaustive match on the $\mathrm{Fin},15$ representative. Seven indices receive a fixed $\pm 1$; the remaining eight (including $0,2,4,6,8,10,12,14$) receive $0$. No lemmas are invoked; the table is the committed geometric content.
why it matters
Downstream orbit certificates for the transported $M_2$ evaluation thread this sign through every type-$(1,3)$ and type-$(3,1)$ slot: m2OrbitCertZ13, m2OrbitCertZ31 and their $E_0$ variants multiply area-slot factors by slotKppOrbit kernel13Sign. Private push lemmas (ker_push_sqrt3, ker_push_sqrt3_e0) likewise insert it when summing the full star-class kernel against permuted class coefficients.
That wiring is part of deliverable A of the QG full-theory campaign: the zero-momentum true-weight Hessian that kills pure gauge (evaluations on axis TT-plus, decoy gauge, and decoy trace all vanish). It does not reverse-engineer weights from Einstein–Hilbert; signs come from the committed geometry modules. Finite-momentum Bloch folding and the global claims S_RS_converges_EH_4d / gap_action_recovery stay out of scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.