farDeficitKernel_eq_chain
plain-language theorem explainer
On the type-(1,2) Regge star, the far-side deficit class kernel equals the negative of the right-hand chain sign times the far cosine kernel, for every one of the ten stencil classes. Anyone wiring the full-star deficit multiset from the cosine kernel cites this identity. The proof is a one-line simp: the deficit kernel is defined as the cosine kernel and the chain sign is −1.
Claim. For every stencil class index $k\in\{0,\ldots,9\}$, the far deficit kernel at $k$ equals $-c_R$ times the far cosine kernel at $k$, where the right-hand chain sign is the constant $c_R=-1$ and the far deficit kernel is defined to equal the far cosine kernel pointwise.
background
This module is the QG full-theory kernel for 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 sits one orbit past the type-(1,1) seed kernel and reuses the committed Gram-projection cosine calculus and the 15-class edge stencil without redefining their API.
The far cosine kernel assigns, on a ten-class far-side slice of the stencil, the cleared-denominator cosine values $\pm 4/(8\sqrt{2})$ or $8/(8\sqrt{2})$ (equivalently $\pm\sqrt{2}/2$ after reduction). The far deficit kernel is defined by copying that cosine table pointwise. The right-hand chain sign is the constant real $-1$, the orientation factor that converts cosine entries into deficit-class contributions on the far side of the star.
Deliverable A of the module already records flat cosines $0$ on all four simplices, star angle sum $2\pi$, and the full-star deficit class kernel valued in ${\pm\sqrt{2}/2}$. The present identity is the algebraic link between the cosine table and the signed deficit table on the far classes.
proof idea
One-line wrapper. Unfold the far deficit kernel (defined as the far cosine kernel) and the right-hand chain sign (the constant $-1$). Then $-c_R\cdot\mathrm{farCos}(k)= -(-1)\cdot\mathrm{farCos}(k)=\mathrm{farCos}(k)$, which matches the deficit kernel at every $k:\mathrm{Fin},10$. No case split on the ten classes is required.
why it matters
The module's deliverable A is the full-star deficit class kernel on all fifteen stencil classes with values $\pm\sqrt{2}/2$, together with nonvacuity, swap-$1\leftrightarrow 2$ hinge-fixing symmetry, the uniform-scaling decoy $\sqrt{2}/2$, and homothety stationarity $0$. This identity is the signed bridge from the far cosine multiset to that deficit table on the far ten classes; without it the chain-oriented assembly of the deficit kernel would be only notational.
No downstream theorem yet consumes it (used-by is empty), so it is presently a local algebraic gate inside the type-(1,2) star package. It does not close the complement orbit type (2,1), does not finish flat Hessian assembly over all hinges, and does not touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery. In the broader RS gravity campaign it is one more kernel-checked increment on the path from discrete Regge stars toward continuum Einstein–Hilbert matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.