deficit_zero_off
plain-language theorem explainer
On the type-(1,3) Regge star, the deficit class kernel vanishes at every edge slot except four fixed indices. Anyone assembling the full-star deficit multiset or evaluating class contributions cites this vanishing lemma. The proof is a one-line Fin-10 case split: non-support indices reduce by definition, support indices are excluded by hypothesis.
Claim. Let $K:\{0,\ldots,9\}\to\mathbb{R}$ be the type-$(1,3)$ star deficit class kernel. If $e\notin\{4,6,7,9\}$, then $K(e)=0$.
background
This module builds 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 Freudenthal star in the origin unit cube. Exactly six Kuhn simplices contain the hinge; each has flat cosine $1/2$, so the star angle sum is exactly $2\pi$.
The upstream definition t13DeficitKernel packages the ten coordinate-class contributions to the star deficit. By definition it is nonzero only at four slots: $K(4)=-\sqrt{3}/6$, $K(6)=K(7)=\sqrt{3}/4$, $K(9)=-\sqrt{3}/2$, and zero elsewhere. The present lemma isolates that default-zero clause under explicit off-support hypotheses.
The local campaign is kernel-checked only: no sorry, no native_decide, no reverse-engineering of Einstein–Hilbert weights. Complementary type $(3,1)$ transport remains open.
proof idea
One-line wrapper: fin_cases e exhausts the ten values of Fin 10. On each branch, first | rfl | contradiction either matches the default _ => 0 clause of the kernel definition by reflexivity, or discharges the branch because the case is one of the four excluded indices $4,6,7,9$ forbidden by the hypotheses.
why it matters
The lemma is the off-support half of the full-star deficit class kernel 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})$. Downstream, member_eval rewrites each star-member assembly as a sum of at most four conditional kernel hits (slots $4,6,7,9$ only); vanishing off those slots justifies dropping the other six terms.
It sits inside deliverable A of the type-(1,3) campaign (star enumeration, flat cosine multiset, flatness gate, ten coordinate derivatives, full-star kernel, and the nonvacuity/transposition/homothety gates). It does not yet close flat Hessian assembly over all hinges, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.