kernel22Sign
plain-language theorem explainer
Integer sign table on the fifteen edge classes for the type-(2,2) Regge star deficit kernel in flat 4D. Gravity analysts cite it when assembling zero-momentum Hessian slot coefficients for the t22 orbit. The body is an exhaustive match on Fin 15 returning ±1.
Claim. The type-$(2,2)$ star-kernel sign is the function $\mathrm{sgn}_{22}:\{0,\ldots,14\}\to\{\pm 1\}$ with values $(+1,+1,-1,+1,-1,-1,+1,+1,-1,-1,+1,-1,+1,+1,-1)$ in edge-class order.
background
The module assembles the flat second variation of the 4D Regge action at zero momentum: orbit-count-weighted sums of products of Heron area gradients with committed star deficit kernels, over the six $S_4$ hinge types with multiplicities $72/48/48/24/24/24$. Edge classes live in $\mathrm{Fin},15$ (nonzero difference masks on the 4-cube vertex set).
Type $(2,2)$ is one of those six orbits. Its deficit kernel on edge classes is, up to a global positive scale fixed elsewhere, a pure $\pm 1$ pattern. This definition records that pattern as an integer-valued lookup, so later certificate arithmetic can stay in $\mathbb{Z}$ before dividing by the common denominator $32$.
Scope is strictly the constant (zero-momentum) edge-class perturbation per cell. Bloch phase folding across hinge translates remains open, and the assembly does not claim Einstein–Hilbert recovery or action-gap closure.
proof idea
Definition by exhaustive pattern match on the fifteen inhabitants of $\mathrm{Fin},15$. No lemmas, no tactics: each constructor returns a hard-coded $+1$ or $-1$. Downstream equalities such as kernel22_eq_sign identify the geometric kernel with this table (up to the fixed scale used in the Hessian).
why it matters
Feeds every t22 slot in the Bloch-transported $M_2$ evaluation pipeline: m2OrbitCertZ22, m2OrbitCertZ22E0, and the theorems equating transported slot coefficients to those certificates over $32$. Those certificates enter slotOrbitKerDot evaluations that show the true-weight Hessian kills pure-gauge and trace decoys at zero momentum (provisional weight-1 left a nonzero residue).
In the QG campaign this is the committed geometric input for the $(2,2)$ orbit inside deliverable A of the flat Hessian assembly. It does not touch the open finite-momentum Bloch fold, nor $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, nor the gap-action flag. Landmark contact is local to Regge discrete gravity on the 4-cube, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.