angleKernel_nine
plain-language theorem explainer
At the flat Freudenthal seed hinge, the angle kernel on squared-edge slot 9 equals 1/2. Anyone assembling the two-simplex partial deficit gradient from arccos chain-ruled dihedral cosines will cite this evaluation. The proof multiplies the fixed flat factor -√2 by the known cos-kernel value -√2/4 and simplifies by ring and norm_num.
Claim. For the seed-hinge angle kernel $\theta' = -(1/\sin\theta)\,\cos'$ evaluated at the flat Freudenthal point (where $1/\sin\theta=\sqrt{2}$), the partial with respect to local squared-edge coordinate $9$ equals $1/2$.
background
This module sits in the QG full-theory campaign after the flat 4D Regge hinge kernel. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum remains open. The deliverable is Gram-projection dihedral cosine as a function of the ten local squared edge lengths, its flat value $\cos=1/\sqrt{2}$, and all ten coordinate derivatives packaged as cosDihedralKernel.
The angle kernel is the arccos chain rule applied to that cosine kernel: $\theta'=-(1/\sin\theta)\cos'$ with flat factor $1/\sin\theta=\sqrt{2}$, so angleKernel k := -√2 · cosDihedralKernel k. Slot 9 is one of the two nonzero cosine-kernel slots (the other is slot 8); the cosine kernel on slot 9 is already known to be $-\sqrt{2}/4$.
proof idea
One-line algebraic evaluation. Unfold angleKernel and substitute cosDihedralKernel_nine (cosDihedralKernel 9 = -√2/4). Rewrite $-√2 · (-√2/4)$ as $(√2·√2)/4 by ring, cancel $√2·√2=2 via Real.mul_self_sqrt, then norm_num yields $1/2$.
why it matters
Feeds singleSimplexDeficitKernel_nine, which flips the sign for one seed simplex's contribution to the deficit gradient $\delta=2\pi-\sum\theta$ and obtains $-1/2$ on slot 9. Together with the slot-8 value and the zero slots, this assembles the local angle kernel $(8,9)\mapsto(-1/4,1/2)$ stated in the module deliverable, and thence the two-simplex partial deficit support on edge classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$.
It is a kernel-checked increment toward the flat Hessian of the 4D Regge action inside Recognition Science gravity analysis. It does not close $S_{\mathrm{RS}}\to$ Einstein–Hilbert in 4D, nor flip gap_action_recovery; those remain open campaign goals. No direct T0–T8 forcing step is discharged here; the link is through the discrete geometric scaffolding of the Regge hinge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.