oppCosKernel
plain-language theorem explainer
Lookup table of first derivatives of the opposite-edge dihedral cosine along the ten-slot edge-length path, evaluated at the flat square configuration. Nonzero only on slots 2 and 9, with values √2/8 and −√2/4. Cited by the opposite-coordinate derivative theorem and the opposite deficit-kernel chain identity in the full-star Regge hinge analysis.
Claim. Define a map $K_{\mathrm{opp}}\colon\{0,\ldots,9\}\to\mathbb{R}$ by $K_{\mathrm{opp}}(2)=\sqrt{2}/8$, $K_{\mathrm{opp}}(9)=-\sqrt{2}/4$, and $K_{\mathrm{opp}}(k)=0$ for all other indices $k$.
background
The ambient module builds the full periodic Freudenthal star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D integer lattice. Scope is six incident 4-simplices across four unit cubes; other hinge orbits remain open. The campaign sits one increment past the two-simplex dihedral cosine calculus and the 15-class edge stencil.
In Regge calculus the deficit angle at a hinge is $2\pi$ minus the sum of dihedral angles of incident simplices. Differentiating that deficit with respect to squared edge lengths requires the derivative of each dihedral cosine at the flat configuration. The opposite-coordinate path varies one edge-length slot while holding the flat square edge data fixed; the ten slots index the stencil classes relevant to the opposite Gram geometry.
Sibling data (oppFlatSqEdges, hingeGramDet_opp, apexDotNum_opp) supply the flat edge vector and Gram numerics against which this kernel is evaluated.
proof idea
Pure definition by pattern match on Fin 10. Two explicit nonzero assignments and a default zero; no lemmas, no tactics.
why it matters
Supplies the numerical derivative values that turn the opposite-coordinate path into a concrete first-order kernel for the star deficit. Downstream, hasDerivAt_opp_coord asserts that the derivative of the dihedral cosine along each opposite path equals this kernel entry at the flat square edges. The identity oppDeficitKernel_eq_chain then factors the opposite deficit kernel as $-\mathrm{chainSeedOpp}$ times these two nonzero entries, linking the cosine calculus to the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
Within the QG full-theory campaign this is a checked increment toward flat Hessian assembly; it does not yet prove Einstein–Hilbert recovery or close gap_action_recovery. It supports the flatness gate (star angle sum $=2\pi$) and the listed stationarity gates without reverse-engineering continuum weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.