assembleClassKernel_eval
plain-language theorem explainer
Assembling the single-simplex deficit kernel onto the fifteen edge classes collapses to the two active local slots (8 and 9). Anyone evaluating partial-deficit class kernels or star-member contributions cites this reduction. The proof unfolds the class-sum definition and applies the Fin-10 split for kernels supported only on those two slots.
Claim. For every simplex index $s\in\{0,\ldots,23\}$ and every edge class $d\in\{0,\ldots,14\}$, the assembly of the single-simplex deficit kernel onto class $d$ equals $(\mathbf{1}_{c_s(8)=d}\,K(8))+(\mathbf{1}_{c_s(9)=d}\,K(9))$, where $K$ is the single-simplex deficit kernel and $c_s$ is the local edge-class map of simplex $s$.
background
This module is the next kernel-checked increment in the 4D Regge seed-hinge campaign after the flat kernel. Scope is the seed triangle hinge inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum remains open.
The single-simplex deficit kernel is $K(k)=-\theta'(k)$, the per-simplex contribution to the deficit gradient $\delta=2\pi-\sum\theta$. From the arccos chain at flat, the angle kernel (hence $K$) vanishes on local slots $0$–$7$ and is nonzero only on slots $8$ and $9$.
Assembly pushes a Fin-10 local kernel onto the fifteen global edge classes by summing, for each class $d$, the local values whose localEdgeClass table entry equals $d$. The lemma sum_fin10_split states that any Fin-10 sum supported only on slots $8$ and $9$ equals $f(8)+f(9)$.
proof idea
One-line term proof after unfolding. Unfold the assembly definition to expose $\sum_{e:\mathrm{Fin},10}\mathbf{1}_{c_s(e)=d},K(e)$. Feed that summand into sum_fin10_split, whose vanishing hypothesis is discharged by singleSimplexDeficitKernel_le_seven: for every slot with value $\le 7$, $K(e)=0$, so the indicator-gated term is identically zero (via ite_self). The split leaves exactly the two gated contributions from slots $8$ and $9$.
why it matters
This is the algebraic bottleneck that turns the ten-slot local deficit kernel into explicit class-supported values. Downstream, the four partial-deficit class theorems (partialDeficitClassKernel_three, _seven, _eleven, and _zero_off) each rewrite with two applications of this evaluation and then decide the local-class equalities, obtaining support on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. The star-kernel lemmas member0_eval and member1_eval likewise reduce each seed simplex's star member to a two-term class expression by rewriting through this theorem.
It sits inside deliverable A of the Regge 4D dihedral campaign: angle and two-simplex partial deficit kernels at flat. It does not close the flat Hessian, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery; those remain open per the module charter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.