t22DeficitKernel
plain-language theorem explainer
The type-(2,2) per-simplex deficit kernel on the ten hinge-ordered local edge slots is identical to the flat cosine kernel. Star-assembly and class-kernel proofs cite this alias when folding local contributions into the 15-class stencil. It is a one-line definitional identification, later justified by the chain factor equaling −1.
Claim. The type-(2,2) per-simplex deficit kernel is the map $D:\{0,\ldots,9\}\to\mathbb{R}$ equal to the flat cosine kernel $c$, with leading values $c(0)=c(1)=-1/4$, $c(2)=0$, $c(3)=1/2$, $c(4)=-1/4$. Equivalently $D(k)=-\chi\,c(k)$ holds with chain weight $\chi=-1$.
background
This module treats the full periodic Freudenthal star of the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) in 4D Regge calculus on the axis-aligned lattice. The campaign imports the Gram-projection cosine calculus and the 15-class edge stencil; it does not redefine those APIs.
The upstream cosine kernel assigns, to each of the ten hinge-ordered local edge slots of a Kuhn simplex, the flat cosine of the dihedral data at that slot. Its explicit values begin $(-1/4,-1/4,0,1/2,-1/4,\ldots)$. In the Regge deficit, each simplex contributes a signed multiple of those cosines; the scalar is the chain weight for this orbit.
Four cube-translate/simplex pairs meet the hinge. Flatness of the star (angle sum $2\pi$) and the closed-form full-star class kernel are the deliverables that consume this kernel.
proof idea
Pure definitional alias: the deficit kernel is declared equal to the cosine kernel on Fin 10. No tactics or lemmas fire at the definition site. The companion identity t22DeficitKernel_eq_chain then discharges the chain factor by simp with chainT22 = -1, confirming $-\chi,c = c$.
why it matters
Local star assembly routes every edge-slot contribution through this kernel. assembleStarMember sums t22DeficitKernel e over the ten slots filtered by starSlotClass; member_eval expands that sum slot-by-slot; fullStarClassKernel_eq equates the assembled 15-class vector to the closed form by rewriting through this alias and the cosine table. The companion theorem t22DeficitKernel_eq_chain records the chain identity used in those rewrites.
In the QG full-theory campaign this is the next kernel-checked increment after the type-(1,1) seed orbit. It supplies the per-simplex weights needed for the type-(2,2) full-star deficit class kernel and the flatness, symmetry, and stationarity gates listed in the module brief. It does not by itself close Hessian assembly 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.