angleKernel_eight
plain-language theorem explainer
At the flat Freudenthal seed hinge, the angle kernel on squared-edge slot 8 equals -1/4. Anyone building the single-simplex deficit gradient from the arccos chain rule cites this evaluation. The proof multiplies the known cosine-kernel value √2/8 by the flat factor -√2 and simplifies by ring arithmetic.
Claim. The local angle kernel at squared-edge coordinate slot $8$ equals $-1/4$. With the angle kernel defined by the arccos chain rule $\theta' = -(1/\sin\theta)\cdot(\cos\theta)'$ and flat value $1/\sin\theta = \sqrt{2}$, and with the cosine kernel on slot $8$ equal to $\sqrt{2}/8$, the product is $-1/4$.
background
In the Regge 4D seed-hinge analysis, the dihedral angle $\theta$ of the seed triangle hinge ${0,e_0,e_0+e_1}$ is studied inside its two seed-cell Freudenthal 4-simplices only. The cosine of that angle is an explicit algebraic function of the ten local squared edge lengths (Gram-projection form). At the flat Freudenthal point one has $\cos\theta = 1/\sqrt{2}$ and $\sin\theta = 1/\sqrt{2}$.
The cosine kernel packages the ten coordinate derivatives of $\cos\theta$ at flat: slot 8 maps to $\sqrt{2}/8$, slot 9 to $-\sqrt{2}/4$, and slots 0–7 vanish. The angle kernel applies the arccos chain-rule factor: $\theta' = -(1/\sin\theta)\cdot\cos'$ with flat $1/\sin\theta = \sqrt{2}$, so the angle kernel on index $k$ is $-\sqrt{2}$ times the cosine kernel on $k$.
This module is the next kernel-checked increment after the flat cosine kernel. Scope is the seed hinge in the two seed simplices; the full lattice orbit sum remains open.
proof idea
Unfold the angle kernel as $-\sqrt{2}$ times the cosine kernel. Substitute the already-proved fact that the cosine kernel on slot 8 equals $\sqrt{2}/8$. Rewrite $-\sqrt{2}\cdot(\sqrt{2}/8)$ as $-(2/8)$ by ring (associating the product under the minus sign) and the identity $\sqrt{2}\cdot\sqrt{2}=2$ (via mul_self_sqrt). Finish with norm_num to obtain $-1/4`.
why it matters
This is the slot-8 half of the local angle-kernel pair (slot 8 $\mapsto -1/4$, slot 9 $\mapsto 1/2$) listed in the module deliverable. Downstream, the single-simplex deficit kernel on slot 8 flips the sign (deficit contribution is $-\theta'$ per simplex) and yields $+1/4$. That value feeds the two-simplex partial deficit gradient, supported on edge classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$.
In the Recognition Science gravity campaign this is a concrete arithmetic checkpoint on the path from discrete Regge geometry toward continuum Einstein–Hilbert recovery. It does not close gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D; those remain open. The eight-tick octave and $D=3$ landmarks of the forcing chain sit upstream of the lattice setup but are not invoked in this local kernel identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.