member1_eval
plain-language theorem explainer
For each of the fifteen edge classes, the second star member (simplex index 1) contributes one-quarter on class 11, minus one-half on class 3, and zero elsewhere to the assembled deficit class kernel. Lattice-gravity workers summing the six-member star kernel cite this closed form. The proof rewrites through the two-slot assembly identity, decides the local edge-class map on slots 8 and 9, and finishes by arithmetic.
Claim. For every edge class $d \in \{0,\ldots,14\}$, the assembled contribution of star member $1$ at $d$ equals $\tfrac14$ when $d=11$, equals $-\tfrac12$ when $d=3$, and equals $0$ otherwise.
background
The 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. Exactly six (cube translate, Kuhn simplex) pairs contain that hinge; each member is pushed from a local Fin-10 angle kernel onto the global 15 edge classes of the Freudenthal stencil.
The single-simplex deficit kernel is the per-simplex contribution $-\theta'$ to the deficit gradient $\delta=2\pi-\sum\theta$. Only local slots 8 and 9 are nonzero: they evaluate to $1/4$ and (by the companion evaluation) $-1/2$. Assembly through one simplex $s$ sums those local values onto whichever global classes the local edge table of $s$ hits.
Upstream, the assembly evaluation theorem reduces the Fin-10 sum to exactly those two active slots. The present lemma specialises that identity to star member 1.
proof idea
Rewrite the left-hand side as the class assembly of the single-simplex deficit kernel at simplex 1. Apply the two-slot assembly evaluation theorem, which leaves only the contributions of local edges 8 and 9. Decide (by finite enumeration) that the local edge-class map of simplex 1 sends slot 8 to global class 11 and slot 9 to global class 3. Substitute the already-proved constants for the deficit kernel at those two slots, then close the resulting if-then arithmetic with aesop.
why it matters
The six member evaluations are the summands of the assembled full-star class kernel. The parent equality fullStarClassKernel_eq rewrites that sum against the closed target multiset on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, which is deliverable A.4 of the module. A parallel twelve-member orbit module reuses the same pattern.
In the broader QG campaign this is the next kernel-checked increment after the two-simplex dihedral cosine calculus. It supplies the flat Hessian seed for the seed-hinge orbit only. It does not finish flat Hessian assembly over all hinge orbits, does not prove continuum recovery of Einstein–Hilbert, and does not flip the gap-action recovery flag. Those remain open module-level gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.