fullStarClassKernel_eq
plain-language theorem explainer
For the type-(1,2) Regge hinge orbit, the four-member assembled star sum equals the closed-form 15-class deficit kernel on every stencil class. Gravity analysts building flat Hessians or Bloch orbit means for this hinge cite it. The proof expands the four member evaluations, case-splits on Fin 15, and clears √2 denominators by ring.
Claim. For every edge-stencil class $d \in \{0,\ldots,14\}$, the sum of the four Freudenthal star-member class-kernel contributions on the type-$(1,2)$ hinge equals the closed-form full-star deficit class kernel $K_{(1,2)}(d)$ (values in $\{0,\pm\sqrt{2}/2\}$).
background
This module treats the Regge 4D full periodic-lattice star for the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$). The star consists of exactly four incident 4-simplices in two containing unit cubes of the integer lattice (Freudenthal–Kuhn triangulation). The ambient API is the committed 15-class edge stencil, Gram-projection cosine calculus, and single-simplex deficit kernels; nothing is redefined here.
The assembled kernel is the sum, over the four star members, of each member's contribution to stencil class $d$. The closed form is the piecewise constant map on $\mathrm{Fin},15$ whose nonzero values are $\pm\sqrt{2}/2$, matching the module deliverable that the full-star deficit class kernel takes those values. Upstream, the type-(1,1) seed orbit proved the same assembled-versus-closed identity with six members and integer values; this is the next kernel-checked increment for the four-member $(1,2)$ orbit.
Flatness of the star (angle sum $4\cdot\arccos 0=2\pi$) is already gated in-module, so the kernel identity is the remaining algebraic closure step for this orbit's class weights.
proof idea
Unfold the assembled definition, then rewrite by the four-term sum identity and the four private member-evaluation lemmas (each reducing a star member to a sparse combination of indicator terms on stencil classes). After that, the two sides are explicit rational expressions in $\sqrt{2}$. Record $\sqrt{2}\neq 0$ and $\sqrt{2}\cdot\sqrt{2}=2$, case-split on all fifteen values of $d$, and finish each case by field_simp, ring_nf, and substitution of the squared-root identity. No external analytic lemmas beyond those member evaluations are required.
why it matters
Closes deliverable A.4 of the type-(1,2) star-kernel module in the QG full-theory campaign: the full-star deficit class kernel is identified with its assembled four-member sum on every stencil class. Downstream, sibling orbit modules (type (1,3) and (2,2)) mirror the same equality pattern, and status-flag theorems mark fullStarClassKernelClosed once the identity is in hand. Bloch local-incidence results that rewrite orbit-mean kernels through assembled star sums rely on the same assembled-equals-closed bridge (seeded first on type (1,1)).
In the broader Recognition gravity stack this is a discrete curvature weight on the eight-tick / $D=3$ lattice geometry, not yet the continuum Einstein–Hilbert limit. The module doc is explicit that the complement type $(2,1)$ remains open, flat Hessian assembly over all hinges remains open, and neither S_RS_converges_EH_4d nor gap_action_recovery is flipped here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.