kernel12Sign
plain-language theorem explainer
Integer sign table on the fifteen edge-difference classes for the type-(1,2) Regge star deficit kernel. Orbit-level M2 certificates for the (1,2) and (2,1) S4 types multiply this table against area-slot and kernel-push factors when building the zero-momentum flat Hessian. The body is a pure Fin-15 case split to ±1.
Claim. For each edge-class index $d \in \{0,\ldots,14\}$, the integer $\mathrm{sgn}_{12}(d)\in\{\pm 1\}$ is the committed sign of the type-$(1,2)$ star-class deficit kernel on that class: $(-1,+1,+1,+1,+1,-1,-1,+1,+1,-1,-1,-1,-1,+1,+1)$ in index order.
background
The ambient module assembles the zero-momentum per-cell Hessian of the 4D Regge action from committed star-deficit kernels and Heron area gradients on flat triangle representatives. Edge lengths live in difference-mask classes indexed by Fin 15; the type-(1,2) hinge star contributes a fixed integer kernel on those classes (imported from the hinge-kernel modules).
Complement transport identifies the type-(2,1) kernel with the type-(1,2) kernel on the same fifteen classes, so a single sign table serves both orbits. The module replaces the provisional weight-1 aggregate by true orbit-count weights (72/48/48/24/24/24) and records that pure-gauge and pure-trace decoys evaluate to zero at zero momentum.
Finite-momentum Bloch phase folding across hinge translates remains open; this table is the static, zero-momentum sign pattern only.
proof idea
Definition by exhaustive match on Fin 15: each constructor is assigned a literal ±1. No lemmas, no computation, no axioms. Downstream code treats the resulting function as the integer coefficient vector of the type-(1,2)/(2,1) star kernel.
why it matters
Parent consumers are the integer orbit certificates m2OrbitCertZ12, m2OrbitCertZ21 and their E0 variants in ReggeBlochTransportedAllOrbitM2Eval4D, together with the private kernel-push lemmas that fold the same signs under S4 permutations. Those certificates assemble the true-weight second-variation quadratic that the module advertises as deliverable A (zero-momentum Hessian with gauge-killing weights).
In the QG campaign this is scaffolding data, not a dynamical claim: it locks the discrete sign pattern so later evaluations on axisTTPlus, decoyGauge, and decoyTrace can be certified without re-deriving the kernel. It does not touch the open Bloch-phase problem, nor S_RS_converges_EH_4d or gap_action_recovery. Framework landmarks T0–T8 and the RCL are upstream of the whole Regge stack; this table sits at the gravity-analysis leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.