assembleClassKernel
plain-language theorem explainer
Assembles a ten-slot local squared-edge kernel onto the fifteen global edge classes of the Freudenthal lattice by summing slots whose local edge class matches the target class. Gravity analysts working the 4D Regge seed-hinge Hessian cite it when pushing single-simplex angle derivatives onto the shared class stencil. The body is a one-line indicator sum over Fin 10.
Claim. Given a simplex index $s \in \{0,\ldots,23\}$ and a local kernel $K:\{0,\ldots,9\}\to\mathbb{R}$ on the ten squared-edge slots of that simplex, the assembled class kernel at class $d\in\{0,\ldots,14\}$ equals $\sum_{e=0}^{9} K(e)\,\mathbf{1}_{\mathrm{class}(s,e)=d}$.
background
This module sits in the QG full-theory campaign for the 4D Regge seed-hinge dihedral cosine kernel at the flat Freudenthal point. Scope is the seed triangle hinge inside its two seed-cell 4-simplices only; the full lattice orbit sum remains open. The ten local squared-edge slots of a simplex are the coordinates of the local edge vector; the fifteen edge classes are the global stencil labels shared across simplices.
The map localEdgeClass (from the flat-kernel layer) sends each pair (simplex $s$, local slot $e$) to a class in $\mathrm{Fin},15$ via the incidence mask. A local kernel is any real function on the ten slots, typically a coordinate gradient of a dihedral angle or partial deficit at flat. The geometric deficit at a hinge is $2\pi-\sum\theta$; here one only needs the local assembly step that pushes slot derivatives onto classes.
The definition never redefines the incidence API: it only folds a Fin-10 vector through one simplex's class table.
proof idea
Pure definition, not a proof. For each target class $d$, sum the local kernel over the ten slots, retaining $K(e)$ exactly when the local edge class of $(s,e)$ equals $d$, else zero. No lemmas are applied; the indicator sum is the entire body.
why it matters
This is the glue between single-simplex angle kernels and the 15-class stencil used by the two-simplex partial deficit. Downstream, partialDeficitClassKernel adds the assemblies for the two seed simplices $s=0,1$, yielding the flat gradient $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2$ supported on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. The evaluation theorem assembleClassKernel_eval collapses the sum to the two active local slots (8 and 9). Star-kernel members reuse the same assembly to read off class supports for orbit bookkeeping.
In the module deliverable list this is step 4 of the kernel-checked increment after the flat cosine kernel: angle kernels via the arccos factor $-\sqrt{2}$ at flat, then class assembly. It does not close the full Hessian, EH recovery, or the lattice orbit sum; those remain open campaign items.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.