farDeficitKernel
plain-language theorem explainer
Far-orbit deficit class kernel on the ten edge stencil classes for the type-(1,2) Regge hinge star. It is definitionally identical to the far cosine kernel (cleared-denominator Gram cosines on the far squared-length orbit). Downstream star assembly and support lemmas cite it when wiring the two far star members into the local deficit.
Claim. The far deficit kernel is the map $K^{\mathrm{far}}_{\delta}:\{0,\ldots,9\}\to\mathbb{R}$ equal to the far cosine kernel $K^{\mathrm{far}}_{\cos}$, whose nonzero values on the far squared-length orbit are rational multiples of $1/\sqrt{2}$ (explicitly $-4/(8\sqrt{2})$, $8/(8\sqrt{2})$, $4/(8\sqrt{2})$ on the supported classes).
background
Module setting: full periodic Freudenthal star for the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ in the 4D integer lattice (two unit cubes, four incident 4-simplices). The campaign builds a 15-class stencil deficit kernel with values in ${\pm\sqrt{2}/2}$ after flat cosine recomputation via the committed Gram-projection / cleared-denominator cosine calculus.
Star members split into near and far squared-length orbits. The far cosine kernel records the cleared-denominator cosine contributions on the far orbit (indices in $\mathrm{Fin},10$), with explicit entries $(-4)/(8\sqrt{2})$, $(8)/(8\sqrt{2})$, $(4)/(8\sqrt{2})$ on the supported classes and zero elsewhere in the match.
This definition simply names that far cosine table as the far deficit kernel, so later assembly can treat near and far orbits under a uniform deficit-kernel API without re-deriving the cosine values.
proof idea
One-line definitional abbreviation: the body is exactly the far cosine kernel. No tactics, no lemmas, no arithmetic. Downstream identities (e.g. the chain-factor rewrite) unfold this abbreviation by simp.
why it matters
Wires the far half of the type-(1,2) star local deficit. starLocalDeficitKernel sends star members 2 and 3 to this kernel (members 0 and 1 use the near kernel). Support lemmas far_kernel_zero_off, member2_eval, and member3_eval evaluate assembly on the far members by reading these entries; farDeficitKernel_eq_chain records the chain-factor identity relating deficit and cosine tables.
In the module deliverable list this is the far half of item 4 (full-star deficit class kernel on the stencil). It does not close the open type-(2,1) complement orbit, the remaining hinge orbits, flat Hessian assembly over all hinges, S_RS_converges_EH_4d, or gap_action_recovery. It is a naming step inside the QG full-theory kernel-checked increment after the type-(1,1) seed orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.