fullStarClassKernel_eq
plain-language theorem explainer
The six-member assembled star sum of single-simplex deficit class kernels equals the closed-form full-star deficit class kernel on the fifteen edge classes. Analysts in the Regge 4D Bloch and local-incidence layer cite it to replace the sum by the sparse values (-1,-1,+1,-1,+1,+1,-1) on classes (2,3,6,7,10,11,14). The proof unfolds the sum, applies the six member evaluations, and checks all fifteen classes by cases with arithmetic.
Claim. For every edge-class index $d\in\{0,\ldots,14\}$, the sum over the six star members of the assembled single-simplex deficit kernel at $d$ equals the closed-form full-star class kernel value at $d$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the dihedral cosine calculus. It treats the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and exactly six incident 4-simplices. Edge data live in the fixed 15-class stencil; the kernel is a real-valued function on those classes.
The closed-form full-star class kernel is the sparse map sending classes $(2,3,6,7,10,11,14)$ to $(-1,-1,+1,-1,+1,+1,-1)$ and all other classes to zero. The assembled version is the literal sum, over the six star members, of each member's contribution obtained by transporting the single-simplex deficit kernel through the Freudenthal incidence data.
Upstream private lemmas evaluate each of the six members as a short linear combination of indicator terms on a few classes (fractions $\pm1/2$ and $\pm1/4$). Those evaluations are the only arithmetic input needed to identify the sum with the closed form.
proof idea
Unfold the assembled definition to a sum over Fin 6. Rewrite that sum via the six-term summation identity, then replace each summand by its closed evaluation (member0_eval through member5_eval). The resulting expression is a finite combination of indicators. Case-split on the fifteen values of $d$ and simplify each case against the piecewise closed-form kernel, finishing with numerical normalization. No geometric argument remains; the identity is pure finite arithmetic on the stencil.
why it matters
Deliverable A of the module is the full-star deficit class kernel itself; this theorem is the identification that makes the closed form interchangeable with the geometric assembly. Downstream, the Bloch local-incidence layer uses it to equate the $t_{11}$ orbit-mean local kernel with a normalized assembled mean, and to rewrite the six-member sum as the closed full-star kernel. Parallel star-kernel modules (orbits 12, 13, 22) copy the same equality pattern, and the status-flag theorem for orbit 13 records fullStarClassKernelClosed = true once the identity is in hand.
In the broader Recognition gravity stack this is a lattice-level kernel check on the seed hinge orbit only. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or continuum limits such as $S_{RS}\to$ Einstein–Hilbert. It supplies the sparse class weights that later Hessian and gap-action arguments will consume once every hinge orbit is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.