member5_eval
plain-language theorem explainer
Star member 5 (one of the six simplices in the Freudenthal star of the seed hinge) contributes only on edge classes 11 and 7, with values 1/4 and -1/2. Anyone assembling the full-star deficit class kernel cites this closed form. The proof collapses the ten-edge sum to the two-point support of the opposite-face deficit kernel, then evaluates the slot-to-class map by case split.
Claim. For every edge class $d\in\{0,\ldots,14\}$, the assembled contribution of star member $5$ equals $\tfrac14$ if $d=11$, equals $-\tfrac12$ if $d=7$, and equals $0$ otherwise (equivalently the sum of those two indicator terms).
background
This module builds the full periodic-lattice star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in 4D Regge calculus on the integer lattice. Exactly six (cube translate, Kuhn simplex) pairs contain the hinge; each is a star member indexed by $m\in\mathrm{Fin},6$. Edge degrees of freedom are reduced to a 15-class stencil.
Member assembly maps a member index and a class $d$ to a real by summing, over the ten local edges of the simplex, the local deficit kernel entry whenever the slot-to-class map hits $d$. Members 4 and 5 use the opposite-face deficit kernel, which is nonzero only on two edges: value $1/4$ on edge 2 and $-1/2$ on edge 9.
A support lemma reduces any sum over $\mathrm{Fin},10$ that vanishes off ${2,9}$ to the two surviving terms. That is the algebraic setup for evaluating member 5.
proof idea
Unfold the member assembly and the local deficit table so member 5 is the sum of opposite-face kernel values on slots whose class equals $d$. Apply the two-point support lemma with the off-support vanishing fact for the opposite-face kernel, collapsing the sum to the $e=2$ and $e=9$ contributions. Unfold the slot-to-class table for member 5 and the opposite-face kernel values; aesop finishes the finite case split, yielding the indicators on classes 11 and 7.
why it matters
Deliverable A of the module is the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$. The parent theorem equates the assembled six-member sum to that closed kernel by rewriting with the six member evaluations; this lemma is the last of those six. Without the closed form for member 5, the assembly identity does not fire.
The result sits in the QG full-theory campaign after the dihedral cosine kernel: star enumeration, flat cosine multiset, flatness gate (angle sum $2\pi$), then this class kernel and its gates. It does not yet complete flat Hessian assembly over all hinge orbits, nor prove continuum EH recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.