nearCosKernel
plain-language theorem explainer
Explicit ten-slot table of first derivatives of the dihedral cosine along the near squared-edge orbit of the type-(1,2) Regge hinge, evaluated at the flat configuration. Gravity analysts cite it when assembling the full-star deficit class kernel and when differentiating cosines under edge deformations. The body is pure case dispatch on Fin 10, with five nonzero cleared-denominator entries and zeros elsewhere.
Claim. Define the near cosine kernel $K_{\mathrm{near}}:\{0,\ldots,9\}\to\mathbb{R}$ by $K_{\mathrm{near}}(4)=-4/(8\sqrt{2})$, $K_{\mathrm{near}}(6)=4/(8\sqrt{2})$, $K_{\mathrm{near}}(7)=8/(8\sqrt{2})$, $K_{\mathrm{near}}(8)=4/(8\sqrt{2})$, $K_{\mathrm{near}}(9)=-8/(8\sqrt{2})$, and $K_{\mathrm{near}}(k)=0$ for every other index.
background
This module continues the QG full-theory campaign for 4D Regge calculus on the integer lattice. After the type-(1,1) seed orbit, it treats the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$) and its full periodic Freudenthal star: two containing unit cubes and four incident 4-simplices.
The committed cosine calculus differentiates the dihedral cosine of a 4-simplex with respect to squared edge lengths via Gram determinants and cleared denominators. The ten coordinates are the near-orbit squared-edge slots of the 15-class stencil; the flat basepoint is the configuration in which every incident simplex has dihedral cosine $0$.
The table records those partial derivatives at the flat near basepoint. Downstream, the same numbers reappear as the near deficit kernel (up to the constant chain-rule factor) and as summands when each star member is assembled over stencil classes.
proof idea
No proof: the declaration is a definition by exhaustive pattern match on Fin 10. Five indices carry the explicit rational multiples of $1/\sqrt{2}$ written with cleared denominator $8\sqrt{2}$; the remaining five slots are zero. Downstream derivative theorems discharge each nonzero slot by a dedicated HasDerivAt lemma and the zero slots by the zero derivative.
why it matters
This table is the numerical heart of deliverable A for the type-(1,2) star: the full-star deficit class kernel with values in ${\pm\sqrt{2}/2,0}$ after assembly. It is the right-hand side of hasDerivAt_near_coord, which states that the derivative of the dihedral cosine along each near coordinate path equals the corresponding table entry at the flat squared edges.
nearDeficitKernel is definitionally identical to this table, and nearDeficitKernel_eq_chain relates it to the chain-rule form used in deficit assembly. Private member evaluations (member0_eval, member1_eval) inline the same coefficients when summing star contributions over the 15 stencil classes.
In the broader RS gravity program this is one kernel-checked increment toward flat Hessian assembly; it does not yet close $S_{\mathrm{RS}}\to$ Einstein–Hilbert in 4D, nor the type-(2,1) complement orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.