kernel11Sign
plain-language theorem explainer
Integer sign pattern of the type-(1,1) star deficit kernel on the fifteen edge classes of a 4-simplex. Nonzero only on seven classes (values ±1); zero elsewhere. Downstream Bloch-fold and M2-symbol slots cite it as the fixed kernel weight in every transported kernel-dot sum. The body is a pure match table, no proof obligations.
Claim. The type-$(1,1)$ star-deficit kernel sign on edge class $d \in \{0,\ldots,14\}$ is the integer $s_{11}(d) \in \{-1,0,1\}$ with $s_{11}(2)=s_{11}(3)=s_{11}(7)=s_{11}(14)=-1$, $s_{11}(6)=s_{11}(10)=s_{11}(11)=1$, and $s_{11}(d)=0$ for all other $d$.
background
The ambient module assembles the zero-momentum flat Hessian of the 4D Regge action from committed per-orbit star deficit kernels and Heron area gradients. Edge lengths live in fifteen classes indexed by Fin 15 (unordered pairs among five simplex vertices). The type-(1,1) orbit is one of the six $S_4$ hinge-orbit types whose orbit counts weight the true-weight Hessian sum.
The star deficit kernel for a fixed orbit type is an integer vector on those fifteen classes: it records how a unit length perturbation on class $d$ contributes to the angular deficit at the hinge. Only the sign pattern of the type-(1,1) kernel is packaged here; companion modules supply the other orbit kernels and the area gradients $\partial A/\partial a$, $\partial A/\partial b$, $\partial A/\partial c$ at the four flat triangle representatives.
Scope of the module is strictly zero-momentum (constant edge-class perturbation) per-cell Hessian. Finite-momentum Bloch phase folding across hinge translates remains open.
proof idea
Pure definition by pattern match on the Fin 15 representative. Seven explicit constructors receive $\pm 1$; the catch-all branch returns $0$. No lemmas, no tactics, no computational certificate beyond the match itself.
why it matters
Every phased transported-kernel integer symbol in the Bloch-fold and M2-symbol layers multiplies by this sign table. Downstream consumers include the integer and $\sqrt{2}/2$ slot symbols, the plain kernel-dot integer symbol, the phase-squared slot symbols (including the E0 variant), and the orbit-level kernel-dot evaluations that certify vanishing on axisTTCross and related decoy modes.
In the QG full-theory campaign this table is the committed geometric weight for type-(1,1) inside the true-weight Hessian that replaces the provisional weight-1 aggregate. True weights are what kill pure gauge at zero momentum (the decoy evaluations go to $0$ rather than the provisional $32$). The definition does not itself close continuum recovery or the gap-action flag; it only supplies the fixed kernel factor those later arguments sum against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.