far_kernel_zero_off
plain-language theorem explainer
On the 10-class edge stencil, the far deficit kernel vanishes at every index outside {0,1,3,5,7,9}. Star-member evaluators for the type-(1,2) Regge hinge cite this to drop off-support terms. Proof is exhaustive Fin 10 case split: each case is definitional zero or contradicts the off-support hypotheses.
Claim. Let $e\in\{0,\ldots,9\}$. If $e\notin\{0,1,3,5,7,9\}$, then the far deficit class kernel (the far cosine kernel on the 10-edge stencil) evaluates to $0$ at $e$.
background
This module builds the full periodic-lattice star deficit class kernel for the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ in 4D Regge calculus on the integer Freudenthal lattice. Scope is two containing unit cubes and four incident 4-simplices; the complement orbit (2,1) and other hinge orbits stay open.
The far deficit kernel is definitionally the far cosine kernel on a 10-index edge stencil (the far squared-length orbit of flat edges). Sibling near/far flat-edge lists and Gram-projection cosine calculus supply the numerical support pattern; only six stencil slots can carry nonzero far-orbit weight.
Local deliverables already include star enumeration (four cube-translate/Kuhn pairs), flat cosine multiset all zero, and the flatness gate $4\cdot\arccos 0=2\pi$. This lemma isolates the complementary vanishing statement on the far kernel.
proof idea
One-line wrapper: fin_cases e exhausts the ten indices in Fin 10. On each branch the tactic closes by rfl when the kernel definition yields zero at that index, or by contradiction when the branch index is one of $0,1,3,5,7,9$ and therefore violates an off-support hypothesis. No external lemmas beyond the definitional equality farDeficitKernel = farCosKernel.
why it matters
Feeds the private star-member evaluators member2_eval and member3_eval, which assemble per-simplex contributions to the full-star deficit class kernel on the 15-class stencil (values $\pm\sqrt{2}/2$). Those assemblies are part of deliverable A in the QG full-theory campaign: the type-(1,2) full-star kernel after the type-(1,1) seed orbit in ReggeHinge4DStarKernel.
Without off-support vanishing, the member sums would retain spurious stencil classes. The lemma does not itself close flat Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery; it is a local support fact inside the (1,2) kernel check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.