near_kernel_zero_off
plain-language theorem explainer
On the near-side 10-edge stencil of the type-(1,2) Regge hinge, the deficit class kernel vanishes at every index outside {4,6,7,8,9}. Gravity analysts cite it when collapsing star-member assemblies to the few nonzero support classes. The proof is exhaustive Fin-10 case split: each off-support case is either definitional zero or contradictory.
Claim. Let $K_{\mathrm{near}}:\{0,\ldots,9\}\to\mathbb{R}$ be the near-side deficit class kernel (equal to the near cosine kernel). If $e\in\{0,\ldots,9\}$ satisfies $e\notin\{4,6,7,8,9\}$, then $K_{\mathrm{near}}(e)=0$.
background
This module treats the full periodic Freudenthal star of the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$) in the 4D integer lattice: two containing unit cubes and four incident 4-simplices. The campaign goal is the full-star deficit class kernel on the 15-class edge stencil, with values in ${\pm\sqrt{2}/2}$, after flat cosine multiset and flatness-gate checks.
The near-side deficit kernel is defined by alias as the near cosine kernel on a 10-index edge list (the near flat squared-length orbit). Only five of those ten indices carry nonzero kernel weight; the rest are structural zeros used when assembling each star member's contribution over the 15 stencil classes.
Upstream, the kernel is just nearCosKernel renamed; no new analytic content is introduced here.
proof idea
One-line wrapper around fin_cases. Split on the ten possible values of $e$. For each concrete index, either the kernel definition reduces by rfl to $0$, or one of the five inequality hypotheses is contradicted. No arithmetic lemmas are needed.
why it matters
Feeds the private evaluations member0_eval and member1_eval, which expand assembleStarMember for the first two star members into sparse sums over stencil classes $d\in\mathrm{Fin},15$ with coefficients multiples of $1/(8\sqrt{2})$. Those expansions rely on killing every off-support near-kernel slot so only the classes tied to indices $4,6,7,8,9$ survive.
In the module deliverable list this is part of item 4 (full-star deficit class kernel on all 15 stencil classes). It does not touch the still-open complement orbit type $(2,1)$, the remaining hinge orbits, flat Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, or gap_action_recovery. Within RS gravity it is a local combinatorial gate inside the QG full-theory kernel-checked increment after the type-(1,1) seed orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.