fullStarClassKernel_zero_off
plain-language theorem explainer
On the type-(1,3) Regge hinge star, the full-star deficit class kernel vanishes on every edge class outside the seven active indices {1,3,5,7,9,11,13}. Anyone assembling directional sums or homothety stationarity for this orbit cites it to collapse the Fin-15 sum to those seven slots. The proof is exhaustive case analysis on Fin 15 with rfl or contradiction.
Claim. Let $K:\mathrm{Fin}\,15\to\mathbb{R}$ be the type-$(1,3)$ full-star deficit class kernel. If $d\in\mathrm{Fin}\,15$ satisfies $d\notin\{1,3,5,7,9,11,13\}$, then $K(d)=0$.
background
This module treats the Regge 4D type-(1,3) periodic-lattice star deficit class kernel: the triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star. The deliverable is a kernel-checked increment after the type-(1,1) seed orbit, importing the 15-class stencil and Gram-projection cosine calculus without redefining their API.
The full-star class kernel $K$ is the piecewise real function on the 15 edge classes that records the star's first-order deficit response. In this module it is nonzero only on classes $1,3,5,7,9,11,13$, with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. Parallel kernels exist for other orbit types (e.g. type $(1,1)$ supported on ${2,3,6,7,10,11,14}$).
The zero-off statement is the support lemma: outside those seven classes the kernel is identically zero, so any weighted sum over all fifteen classes reduces to the active support.
proof idea
Term-mode proof by exhaustive case split: fin_cases d enumerates all fifteen values of $d:\mathrm{Fin},15$. On each branch, first | rfl | contradiction either closes by definitional equality (the default arm of $K$ returns $0$) or discharges the branch as impossible because $d$ equals one of the seven excluded active indices. No external lemmas are required beyond the definition of the kernel.
why it matters
This is the support gate for every directional identity on the type-(1,3) star. Downstream, fullStar_homothety_stationary and fullStar_uniformScale_decoy rewrite the Fin-15 sum via sum15_support by feeding exactly these seven inequalities, collapsing off-support terms with mul_zero. The same pattern appears in the parent type-(1,1) module and in status flags (hinge4DStarKernel13Status_flags).
Within the QG full-theory campaign it is deliverable A.5 of the module doc: the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$. It does not finish flat Hessian assembly over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. Transport of this kernel to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.