starLocalDeficitKernel
plain-language theorem explainer
Case dispatcher assigning the near-orbit and far-orbit deficit kernels to the four star members of the type-(1,2) triangle hinge. Anyone assembling the full-star deficit class kernel on the 15-class stencil cites it. Pure definition by pattern match on the star-member index: members 0,1 get the near kernel; members 2,3 get the far kernel.
Claim. The local star deficit kernel for the type-$(1,2)$ hinge is the map $K:\{0,1,2,3\}\times\{0,\ldots,9\}\to\mathbb{R}$ with $K(m,\cdot)=K_{\mathrm{near}}$ when $m\in\{0,1\}$ and $K(m,\cdot)=K_{\mathrm{far}}$ when $m\in\{2,3\}$, where $K_{\mathrm{near}}$ and $K_{\mathrm{far}}$ are the near- and far-orbit cosine deficit kernels on the ten edge classes.
background
This module is the next kernel-checked increment in the Regge 4D QG campaign after the type-$(1,1)$ seed orbit. Scope is 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: two containing unit cubes, four incident 4-simplices. The complement type $(2,1)$ and other hinge orbits remain open.
The star has four members. They fall into two local squared-length orbits (near and far). Each orbit carries its own Gram-derived cosine kernel; the deficit kernels are just those cosine kernels renamed (nearDeficitKernel := nearCosKernel, farDeficitKernel := farCosKernel). The ten-index domain is the edge-class stencil shared with the type-$(1,1)$ module.
The type-$(1,1)$ analogue dispatches six members across three kernels (single-simplex, orthogonal, opposite). Here the star is smaller (cardinality four), so the dispatcher only needs two branches.
proof idea
Definition by exhaustive pattern match on the star-member index in Fin 4. Indices $0$ and $1$ return the near-orbit deficit kernel; indices $2$ and $3$ return the far-orbit deficit kernel. No proof obligations: pure abbreviation of the two already-defined kernels.
why it matters
Delivers item 4 of the module's deliverable A: the full-star deficit class kernel on all 15 stencil classes (values $\pm\sqrt{2}/2$ after assembly). Downstream, assembleStarMember folds this kernel against the star-slot class map to produce a Fin 15 → ℝ contribution per member; the private member*_eval lemmas then evaluate those contributions by cases.
It is the type-$(1,2)$ counterpart of the six-member dispatcher in ReggeHinge4DStarKernel. Together the two kernels feed the flatness gate (star angle sum $=2\pi$) and the nonvacuity, swap-symmetry, uniform-scaling, and homothety-stationarity gates. It does not yet close the flat Hessian over all hinges, nor S_RS_converges_EH_4d, nor gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.