member_eval
plain-language theorem explainer
For each of the four star members and each of the fifteen edge-orbit classes, the assembled class-kernel value equals the explicit ten-term sum that retains the type-(2,2) local deficit precisely when a star slot maps to that class. Analysts closing the (2,2) Regge full-star kernel cite this to expand the sum definition into case form. The proof unfolds the assembly definition and applies the Fin-10 sum expansion.
Claim. For every star-member index $m\in\{0,1,2,3\}$ and every stencil class $d\in\{0,\ldots,14\}$, the assembled star-member contribution at $d$ equals $\sum_{e=0}^{9}\mathbf{1}_{\mathrm{slot}(m,e)=d}\,\kappa_{22}(e)$, where $\kappa_{22}$ is the type-(2,2) local deficit kernel on the ten hinge-ordered edges and $\mathrm{slot}(m,e)$ is the star slot-to-class map into the fifteen-class stencil.
background
This module treats the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) and its full periodic Freudenthal star in the 4D Regge lattice. Exactly four (cube-translate, Kuhn-simplex) pairs contain the hinge; each simplex carries a ten-edge local stencil projected into the global fifteen-class edge orbit.
The assembly map for a star member $m$ at class $d$ is the sum over the ten local edges $e$ of the type-(2,2) deficit kernel entry whenever the slot-class map sends $(m,e)$ to $d$, and zero otherwise. The same pattern appears for the (1,1) and (1,2)/(1,3) orbits in sibling modules; here the kernel is the (2,2)-specific table and there are four members rather than six.
Upstream, the slot-class tables and the sum-shaped assembly definition are already fixed; this lemma only expands that sum into an explicit ten-term indicator form so later closed-form evaluations can case-split on $d$.
proof idea
One-line term proof. Unfold the definition of the assembly map (the sum over Fin 10 of the indicator times the local deficit kernel). The goal is then exactly the statement of the Fin-10 sum-expansion lemma, which rewrites a ten-fold sum of terms $f,e$ as the concrete sum $f,0+\cdots+f,9$. Apply that lemma and finish.
why it matters
Delivers the expanded evaluation form needed to obtain the full-star deficit class kernel on all fifteen stencil classes for the (2,2) orbit (deliverable A.4 of the module). The immediate parent in this file is the equality that identifies the summed star kernel with its closed class-by-class expression.
In the QG full-theory campaign this is the next kernel-checked increment after the (1,1) seed orbit: flat cosine multiset all zero, star angle sum exactly $2\pi$, and the usual gates (nonvacuity, swap symmetries fixing the hinge vertex set, uniform-scaling decoy, homothety stationarity). It does not yet assemble the flat Hessian over all hinge orbits, nor prove continuum EH recovery.
Sibling (1,3) closed-member lemmas follow the same expand-then-case pattern; this lemma is the (2,2) instance of that pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.