member_eval
plain-language theorem explainer
For each of the six Kuhn simplices in the type-(1,3) Freudenthal star and each of the fifteen edge classes, the assembled star-member contribution collapses to a sum of at most four indicator terms on the support slots {4,6,7,9}. Anyone writing the closed per-member class formulas cites this reduction. The proof unfolds the sum definition and applies a four-support collapse that uses vanishing of the local deficit kernel off those slots.
Claim. For every star member $m\in\{0,\ldots,5\}$ and every edge class $d\in\{0,\ldots,14\}$, the assembled contribution of member $m$ to class $d$ equals $\sum_{e\in\{4,6,7,9\}}\mathbf{1}_{\mathrm{slot}(m,e)=d}\,\kappa_{13}(e)$, where $\kappa_{13}$ is the type-$(1,3)$ local deficit kernel and $\mathrm{slot}$ maps member-edge pairs into the fifteen global classes.
background
This module is the QG full-theory kernel for the type-(1,3) triangle hinge on the 4D periodic Freudenthal lattice. The hinge has absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Exactly six Kuhn simplices in the origin unit cube contain the hinge; the complementary type $(3,1)$ is related by mask complement but transport of this kernel remains open.
Star assembly packages, for each of the six members $m$ and each global edge class $d$, a sum over the ten local edge slots $e$: if the member-slot map sends $(m,e)$ to $d$, contribute the local deficit kernel value at $e$, else zero. In this type-(1,3) file the local kernel is the fixed map $\kappa_{13}$ (independent of $m$), and a prior lemma records that $\kappa_{13}(e)=0$ whenever $e\notin{4,6,7,9}$.
The fifteen-class stencil and the Freudenthal incidence layer are imported, not redefined. The flat cosine multiset is constantly $1/2$, so the star angle sum is exactly $2\pi$ before any class-kernel work begins.
proof idea
One-line structural reduction. Unfold the definition of the assembled member (the sum over ten local slots of the indicator-times-kernel). Apply the four-support sum lemma that collapses a sum over $\mathrm{Fin},10$ to the four indices ${4,6,7,9}$ once the summand vanishes off that set. The vanishing hypothesis is discharged by the already-proved off-support lemma for $\kappa_{13}$, via a short simp on each of the six complementary indices.
why it matters
This is the bridge from the raw ten-slot assembly to the six closed member formulas that feed the full-star deficit class kernel. Downstream, each of member0_closed through member5_closed specializes the four-term sum at a fixed $m$, substituting the concrete slot-to-class table and the known $\kappa_{13}$ values, and obtains explicit linear combinations of $\pm\sqrt{3}/6$, $\pm\sqrt{3}/4$, $\pm\sqrt{3}/2$ on classes in ${1,3,5,7,9,11,13}$. Those closed forms are then summed in the type-(2,2) companion to produce the full-star class kernel equality.
In the module deliverable list this sits under item 5 (full-star deficit class kernel with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$ on classes $(1,3,5,7,9,11,13)$). It does not touch the Einstein-Hilbert convergence claim, the gap-action recovery flag, or reverse-engineered continuum weights. The $(3,1)$ transport remains open by design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.