member1_eval
plain-language theorem explainer
Evaluates star-member 1 of the type-(1,2) Freudenthal star: its contribution to each of the 15 edge-class slots is a five-term sparse sum of cleared-denominator cosine entries. Cited when equating the assembled full-star class kernel to the closed form with values ±√2/2. Proof unfolds the assembly sum, restricts to the near-support edges via a zero-off lemma, then finishes by finite case split.
Claim. For every stencil class $d\in\{0,\ldots,14\}$, the assembled contribution of star member $1$ equals $\mathbf{1}_{d=5}\frac{-4}{8\sqrt{2}}+\mathbf{1}_{d=13}\frac{4}{8\sqrt{2}}+\mathbf{1}_{d=1}\frac{8}{8\sqrt{2}}+\mathbf{1}_{d=7}\frac{4}{8\sqrt{2}}+\mathbf{1}_{d=9}\frac{-8}{8\sqrt{2}}$.
background
This module treats the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$) and its full periodic Freudenthal star in the integer lattice: two containing unit cubes and four incident 4-simplices. It is the next kernel-checked increment after the type-(1,1) seed orbit; the complement type (2,1) remains open.
assembleStarMember m sums, over the ten local edges of member $m$, the local deficit kernel whenever the edge lands in stencil class $d$. For the near orbit (members 0 and 1), that local kernel is the near deficit kernel, whose nonzero values are exactly the five cleared-denominator cosines in nearCosKernel (edges 4,6,7,8,9). Slot classification starSlotClass maps those local edges into the global 15-class stencil.
The upstream type-(1,1) module has an analogous private evaluation lemma with a different sparse support; here the support and coefficients are recomputed from the (1,2) Gram orbits.
proof idea
Unfold assembleStarMember and starLocalDeficitKernel so the claim is a sum over ten edges of a gated near-deficit kernel. Rewrite that sum by sum_support_near, using near_kernel_zero_off to kill every edge outside the near support. The remaining finite expression is then simplified against starSlotClass, nearDeficitKernel, and nearCosKernel, after which aesop discharges the case split on the class index $d$.
why it matters
Feeds the local theorem fullStarClassKernel_eq, which equates the four-member assembled star kernel to the closed-form full-star class kernel (values $\pm\sqrt{2}/2$ on the active classes). That equality is deliverable A.4 of the type-(1,2) campaign: full-star deficit class kernel on all 15 stencil classes, together with the flatness gate (star angle sum $2\pi$) and the nonvacuity / swap-symmetry / scaling / homothety gates.
In the broader QG full-theory track this is one hinge-orbit kernel check toward discrete Einstein–Hilbert recovery. It does not yet close the flat Hessian over all orbits, nor S_RS_converges_EH_4d, nor gap_action_recovery. The type-(2,1) complement and the remaining hinge orbits stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.