fullStarClassKernel_eq
plain-language theorem explainer
For the type-(2,2) Regge triangle hinge, the four-member star assembly of local edge contributions equals the closed-form 15-class deficit kernel on every stencil class. Gravity analysts cite it when collapsing star sums to the tabulated kernel before Bloch averaging or Hessian work. The proof unfolds the assembled sum, expands the four-term total, and discharges all fifteen classes by evaluation plus numeric simplification.
Claim. For every stencil class $d\in\{0,\ldots,14\}$, the sum of the four star-member contributions to class $d$ equals the closed-form full-star class kernel value at $d$: $\sum_{m=0}^{3}(\mathrm{assemble\,star\,member}\,m\,d)=K_{(2,2)}(d)$.
background
This module treats the type-(2,2) triangle hinge on the 4D Freudenthal–Kuhn lattice, with absolute masks ${0,3,15}$ and difference masks $(3,12)$. The local setting is the full periodic star of that hinge: exactly four (cube translate, Kuhn simplex) pairs contain it, each with flat cosine $0$, so the star angle sum is $2\pi$.
The 15-class edge stencil indexes lattice edge orbits under the residual symmetry. The assembled kernel at class $d$ is the sum of four star-member contributions (each member maps its ten local edges into stencil classes and deposits deficit/cosine weights). The closed-form kernel is the sparse table of those totals after cancellation.
Upstream siblings for orbits (1,1) and (1,2) prove the same assembly identity with six or four members respectively; this file is the next kernel-checked increment in that campaign and reuses the incidence, stencil, and Gram-projection cosine APIs without redefining them.
proof idea
Term-mode proof. Unfold the assembled kernel to the four-term sum over star members, then rewrite by the four-sum identity. Case-split on the fifteen stencil indices. In each case, simplify with the member-evaluation lemma, the star-slot class map, the type-(2,2) deficit and cosine kernels, and the closed-form table; finish by norm_num. No analytic estimates: pure finite enumeration and arithmetic.
why it matters
Closes deliverable A.4 of the type-(2,2) star campaign: the full-star deficit class kernel is identified with its assembled sum on all fifteen classes. Downstream, Bloch local-incidence identities for the (1,1) orbit already pattern-match on this equality to replace assembled means by closed kernels; sibling modules for orbits (1,1), (1,2), and (1,3) carry the same lemma and feed status flags that mark fullStarClassKernelClosed.
In the Recognition Science gravity stack this is a discrete curvature building block toward matching Regge deficit action with continuum Einstein–Hilbert on the eight-tick lattice (T7) in $D=3$ spatial dimensions (T8). It does not yet flip gap-action recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D; those remain open above the kernel layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.