angleKernel
plain-language theorem explainer
The angle kernel packages the flat-point derivative of the seed-hinge dihedral angle in each of the ten local squared-edge coordinates. It is the arccos chain rule on the cosine kernel: scale by -√2, the flat value of -1/sin θ. Anyone differentiating Regge angles or Schläfli summands along coordinate paths cites it. The body is a one-line constant scaling of the already-proved cosine derivatives.
Claim. For each local squared-edge index $k \in \{0,\ldots,9\}$, the angle kernel is $\theta'_k = -\sqrt{2}\,(\partial_k \cos\theta)$ at the flat Freudenthal seed, i.e. the chain-rule identity $\theta' = -(1/\sin\theta)\cdot(\cos\theta)'$ with the flat evaluation $1/\sin\theta = \sqrt{2}$.
background
In 4D Regge calculus the action depends on hinge deficits $\delta = 2\pi - \sum\theta$, with each dihedral angle recovered from edge lengths through a Gram-projection cosine. This module treats the seed triangle hinge ${0, e_0, e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices only, using the ten local squared edge lengths as coordinates. The full lattice orbit sum is left open.
The cosine kernel already records all ten flat derivatives of $\cos\theta$: nonzero only on slots 8 and 9, with values $\sqrt{2}/8$ and $-\sqrt{2}/4$. At the flat point one has $\cos\theta = 1/\sqrt{2}$ and $\sin\theta = 1/\sqrt{2}$ (via $\sin^2 = 1-\cos^2$), so the arccos factor $d(\arccos)/d(\cos) = -1/\sin$ collapses to $-\sqrt{2}$.
Upstream, the geometric deficit is defined as $2\pi - \sum\theta$ (DihedralAngle / Schläfli). Per simplex, the contribution to the deficit gradient is therefore $-\theta'$.
proof idea
Pure definition: multiply the cosine kernel by the constant flat chain factor $-\sqrt{2}$. No tactics and no new analysis. Numerical content is inherited from the cosine kernel (slot 8 $\mapsto \sqrt{2}/8$, slot 9 $\mapsto -\sqrt{2}/4$, else $0$), which immediately yields angle-kernel values $(-1/4, 1/2)$ on those two slots and zero elsewhere.
why it matters
Feeds the pathwise Schläfli calculus and the flat second-variation campaign. Downstream results prove the seed dihedral angle is differentiable along every coordinate path with derivative equal to this kernel, and re-export that fact into the second-variation module. The Schläfli pathwise layer identifies the flat angle Jacobian with this kernel and factors each Schläfli summand as hinge area times the angle kernel.
In the Recognition Science gravity program this is deliverable A item 4 of the Regge hinge-kernel campaign: the local angle kernel that, once pushed through each seed simplex's local edge-class table, assembles the two-simplex partial deficit gradient supported on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. The full lattice orbit sum, the flat Hessian of the 4D Regge action, and the gap-action / Einstein-Hilbert recovery targets remain open, as the module scope explicitly records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.