opp_kernel_zero_off
plain-language theorem explainer
For any of the ten edge slots except indices 2 and 9, the opposite-face deficit kernel vanishes. Star-assembly lemmas cite this to drop all off-support terms when summing local contributions over a star member. The proof is a one-line Fin-case split: each concrete index is either definitionally zero or ruled out by the hypotheses.
Claim. Let $K_{\mathrm{opp}}:\{0,\ldots,9\}\to\mathbb{R}$ be the opposite-deficit kernel with $K_{\mathrm{opp}}(2)=1/4$, $K_{\mathrm{opp}}(9)=-1/2$, and $K_{\mathrm{opp}}(e)=0$ otherwise. Then for every edge index $e$ with $e\neq 2$ and $e\neq 9$, one has $K_{\mathrm{opp}}(e)=0$.
background
This module builds the full periodic-lattice star deficit class kernel for a seed triangle hinge in 4D Regge calculus on the integer lattice. The star consists of six incident 4-simplices (four containing unit cubes). Edge slots are indexed by Fin 10, matching the local edge stencil of a 4-simplex pair.
The opposite-deficit kernel is the sparse map that places weight $1/4$ on slot 2, weight $-1/2$ on slot 9, and zero elsewhere. It encodes the opposite-face contribution to the local deficit class before assembly over star members. Sibling kernels (orthogonal flat-square edges, Gram determinants, apex dots) play analogous roles for other geometric channels.
The surrounding campaign is kernel-checked only: no sorry, no native_decide, and no reverse-engineering of Einstein–Hilbert weights. Flatness of the star (angle sum $2\pi$) and the seven-class full-star deficit pattern are already established upstream in the same file.
proof idea
One-line wrapper on fin_cases e. Each of the ten concrete values of $e:\mathrm{Fin},10$ is discharged by either rfl (the default branch of oppDeficitKernel is definitionally $0$) or contradiction (the cases $e=2$ and $e=9$ are excluded by the two inequality hypotheses). No arithmetic or external lemmas are needed.
why it matters
Star-member evaluation lemmas member4_eval and member5_eval rewrite the assembled local deficit as a two-term sum supported only on the opposite-kernel slots. They invoke this vanishing lemma (via a support-sum helper) so that every off-support edge contributes nothing, leaving only the explicit $1/4$ and $-1/2$ pieces on the relevant class indices.
That reduction is part of deliverable A.4 of the module: the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$. The work sits in the QG full-theory campaign after the dihedral cosine kernel, still short of flat Hessian assembly over all hinges and of the convergence statement $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.