fullStarClassKernel_zero_off
plain-language theorem explainer
The full-star deficit class kernel on the 15 edge classes of the 4D Regge lattice vanishes outside the seven classes {2,3,6,7,10,11,14}. Anyone reducing a star directional sum, or checking the homothety-stationarity and uniform-scale decoy gates, cites this support lemma. Proof is exhaustive case split on Fin 15 against the piecewise definition.
Claim. For every edge-class index $d \in \{0,\ldots,14\}$, if $d \notin \{2,3,6,7,10,11,14\}$, then the full-star class kernel evaluates to zero at $d$.
background
This module builds the full periodic-lattice star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in 4D Regge calculus on the integer lattice. The star comprises four containing unit cubes and six incident 4-simplices (Freudenthal incidence). Edge lengths are organized by a fixed 15-class stencil; the kernel is a real-valued function on those classes that encodes the first variation of the star deficit.
The local definition fullStarClassKernel is piecewise: it returns the nonzero values $(-1,-1,+1,-1,+1,+1,-1)$ on classes $(2,3,6,7,10,11,14)$ and defaults to zero elsewhere. Parallel kernels exist for other hinge orbits (e.g. the 1-3 and 2-2 families) with different supports and algebraic values involving $\sqrt{2}$ or $\sqrt{3}$. The present lemma is the support statement for this particular orbit.
Module scope is deliberately narrow: only the seed hinge orbit is treated; other lattice hinge orbits remain open, and the flat Hessian over all hinges is not assembled here.
proof idea
One-line tactic proof. fin_cases d splits on the fifteen possible values of $d : \mathrm{Fin},15$. On each branch, first | rfl | contradiction either closes by reflexivity (the default arm of the piecewise definition returns $0$) or discharges the branch by contradicting one of the seven hypotheses $d \neq 2,3,6,7,10,11,14$. No external lemmas are required.
why it matters
This is the support gate for deliverable A of the Regge 4D full-star campaign (module doc items 4-5). Downstream, fullStar_homothety_stationary and fullStar_uniformScale_decoy both rewrite the 15-term directional sum via sum15_support, feeding this lemma to kill every off-support summand and reduce to the seven nonzero classes. The swap-$2\leftrightarrow 3$ symmetry theorem likewise relies on knowing the kernel vanishes off its listed support.
In the broader Recognition gravity stack this is a kernel-checked increment after the dihedral cosine calculus: it does not yet flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, but it supplies the sparse class weights needed for those later assemblies. Parallel zero-off lemmas exist for the 1-3 and other orbit kernels, forming a uniform pattern across hinge families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.