orthDeficitKernel
plain-language theorem explainer
Orthogonal star-member deficit class kernel on the ten local edge slots of the seed hinge stencil. It places ±1/2 on edge classes 1, 3, 7, 9 and zero elsewhere. Downstream star assembly uses it for the two orthogonal cube-translate members; a one-line fin_cases identity equates it to −chainOrth times the orthogonal cosine kernel. Pure case-split definition, no proof obligations.
Claim. Define the orthogonal deficit kernel $K_{\mathrm{orth}}:\{0,\ldots,9\}\to\mathbb{R}$ by $K_{\mathrm{orth}}(1)=-1/2$, $K_{\mathrm{orth}}(3)=1/2$, $K_{\mathrm{orth}}(7)=1/2$, $K_{\mathrm{orth}}(9)=-1/2$, and $K_{\mathrm{orth}}(k)=0$ for every other index $k$.
background
The module builds the full periodic-lattice star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D Freudenthal triangulation. Exactly six (cube translate, Kuhn simplex) pairs contain that hinge; the star is partitioned into single-simplex, orthogonal, and opposite members.
Edge variations are scored on a ten-slot local stencil (classes drawn from the broader 15-class Regge edge stencil). Separate kernels encode how each star member contributes to the angle deficit under those edge moves. The orthogonal kernel is the contribution attached to the two orthogonal cube-translate members.
A companion identity states that this kernel equals $-\mathrm{chainOrth}$ times the orthogonal cosine kernel, so the $\pm 1/2$ pattern is the deficit-side image of the flat cosine calculus already checked for those members.
proof idea
Definition by exhaustive pattern match on Fin 10. Four constructors return the nonzero half-integers; the catch-all returns zero. No tactics, no lemmas, no computational content beyond the case table.
why it matters
This is the orthogonal piece of deliverable A item 4 in the module: the full-star deficit class kernel. It is wired into starLocalDeficitKernel on star members 2 and 3, so every later star-sum or gate that walks the six-member star reads these coefficients.
Immediate consumers include the chain identity equating the kernel to $-\mathrm{chainOrth}\cdot$ (orthogonal cosine kernel), the off-support vanishing lemma, and the private member-2/3 evaluation lemmas that expand assembleStarMember into explicit half-integer sums. Those evaluations feed the flatness gate (star angle sum $=2\pi$) and the nonvacuity, swap-symmetry, scaling-decoy, and homothety-stationarity gates.
In the QG campaign this is the next kernel-checked increment after the dihedral cosine calculus. It does not yet assemble the flat Hessian over all hinge orbits, nor does it flip gap_action_recovery or prove $S_{RS}$ converges to Einstein–Hilbert in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.