t13CosKernel
plain-language theorem explainer
Lookup table of the ten partial derivatives of the dihedral cosine for a type-(1,3) Regge hinge, evaluated at the flat squared-edge point. Nonzero only on coordinate slots 4, 6, 7, 9, with values −1/4, 3/8, 3/8, −3/4. Gravity analysts cite it when assembling the star deficit class kernel. Pure pattern-match definition; no proof.
Claim. The type-$(1,3)$ cosine kernel is the map $k \mapsto c_k$ on ten edge-squared coordinates with $c_4 = -1/4$, $c_6 = 3/8$, $c_7 = 3/8$, $c_9 = -3/4$, and $c_k = 0$ otherwise. These are the flat-point values of $\partial(\cos\theta)/\partial q_k$ for the hinge dihedral angle.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-$(1,1)$ star kernel and the orbit classification layer. It treats the type-$(1,3)$ triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the origin unit cube.
The cosine calculus comes from the Gram-projection layer already imported: dihedral cosines are algebraic functions of the ten squared edge lengths of a 4-simplex. At the flat configuration the shared Gram data force every star simplex to have cosine $1/2$, so the angle sum is exactly $2\pi$. Differentiating that cosine along each coordinate path yields a ten-slot numerical kernel.
The present definition records those ten numbers. Downstream, the deficit kernel is recovered by the chain rule through $\mathrm{d}(\arccos)/\mathrm{d}u = -1/\sqrt{1-u^2}$, which at $u=1/2$ contributes a universal $\sqrt{3}$ factor.
proof idea
No proof: this is a pattern-matching definition on Fin 10. Four explicit arms assign the nonzero flat derivatives; the catch-all returns zero. The numerical values themselves are justified later by the ten HasDerivAt lemmas that evaluate the cleared-denominator master formula at flat squared edges $(N,P,Q)=(8,8,8)$.
why it matters
Feeds two immediate parents in the same module. hasDerivAt_t13_coord states that the derivative of the dihedral cosine along each coordinate path equals this kernel entry at the flat point. t13DeficitKernel_eq_chain then multiplies by the universal chain-rule factor to obtain the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$.
That deficit kernel is deliverable A.5 of the module: the type-$(1,3)$ contribution to the flat Hessian of the Regge action on the periodic lattice. It does not yet assemble the global Hessian, prove Einstein–Hilbert recovery, or transport the kernel to the complementary type-$(3,1)$ orbit (explicitly open). Within Recognition Science gravity, it is one more checked star class toward the continuum limit of the discrete action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.