cosDihedralKernel
plain-language theorem explainer
Packages the ten partial derivatives of the seed-hinge dihedral cosine at the flat Freudenthal point: only local squared-length slots 8 and 9 are nonzero (√2/8 and −√2/4). Anyone computing the flat Hessian or Schläfli gradient of the 4D Regge action on the seed hinge cites this kernel. It is a pure pattern-match definition, not a proved identity.
Claim. Define the flat cosine kernel $K_{\cos}:\{0,\ldots,9\}\to\mathbb{R}$ on the ten local squared edge lengths by $K_{\cos}(8)=\sqrt{2}/8$, $K_{\cos}(9)=-\sqrt{2}/4$, and $K_{\cos}(k)=0$ for $k\le 7$. These are the coordinate derivatives of the seed-hinge dihedral cosine at the flat point.
background
In 4D Regge calculus the action is assembled from hinge areas times deficit angles. A deficit is $2\pi$ minus the sum of dihedral angles of the 4-simplices meeting at a triangular hinge. This module treats one seed hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices, working entirely in the ten local squared edge lengths.
The dihedral cosine is obtained by Gram projection: inner products and norms of the two apex vectors orthogonal to the hinge plane, written in cleared-denominator form. At the flat Freudenthal assignment one has $\cos\theta=1/\sqrt{2}$ (equivalently $\sin\theta=1/\sqrt{2}$), proved by transcendental-free arithmetic.
The present definition simply records the ten partials of that cosine with respect to the local squared lengths. Downstream the arccos chain rule multiplies by $-1/\sin\theta=-\sqrt{2}$ to produce the angle kernel, which then feeds the two-simplex partial deficit gradient on the 15 edge classes.
proof idea
Pure definition by pattern match on Fin 10. Slot 8 returns $\sqrt{2}/8$, slot 9 returns $-\sqrt{2}/4$, and every other index returns 0. No lemmas are invoked; the values are the content of the master derivative theorem hasDerivAt_cosDihedral_coord, which this kernel packages for later use. Companion rfl lemmas pin the two nonzero slots and the vanishing on indices $\le 7$.
why it matters
This is deliverable A of the Regge 4D seed-hinge campaign: the flat cosine derivative kernel that every subsequent gradient identity quotes. It is multiplied by $-\sqrt{2}$ to form angleKernel, which appears in hasDerivAt_seedDihedralAngle_coord and in the pathwise Schläfli identity flatSchlaefliSummand_seed_eq_area_angleKernel (hinge area times angle kernel). The two-simplex partial deficit gradient is then supported only on edge classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$.
Within Recognition Science this sits in the gravity/analysis layer that aims at continuum recovery of Einstein–Hilbert from the discrete Regge action. The module explicitly does not yet complete the flat Hessian, prove $S_{\mathrm{RS}}$ converges to EH in 4D, or flip gap_action_recovery. The full lattice orbit sum over all hinges remains open; only the seed triangle inside its two Freudenthal cells is kernel-checked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.