t13DeficitKernel_eq_chain
plain-language theorem explainer
For each of ten edge-class indices, the type-(1,3) Regge star deficit kernel equals the flat chain factor times the cosine kernel. Anyone assembling the full-star deficit class kernel on the Freudenthal star cites this identity. The proof is exhaustive fin_cases on Fin 10, unfolding the three definitions and clearing √3 by field_simp and ring.
Claim. For every class index $k\in\{0,\ldots,9\}$, the type-$(1,3)$ deficit kernel at $k$ equals $-c_{T13}$ times the cosine kernel at $k$, where the chain factor is $c_{T13}=-2/\sqrt{3}$ (i.e. $-1/\sin\theta$ at the flat cosine $1/2$).
background
This module is the next kernel-checked increment in the 4D Regge campaign after the type-(1,1) star kernel and the orbit classification. The hinge is the type-(1,3) triangle with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star of six Kuhn simplices in the origin unit cube.
At flat geometry every simplex has cosine $1/2$, so $\sin=\sqrt{3}/2$. The chain factor chainT13 is defined as $-2/\sqrt{3}$, which is exactly $-1/\sin$ at that angle: it converts cosine derivatives into deficit-angle derivatives via the arccos chain rule. The cosine kernel records the ten coordinate derivatives of the flat Gram cosines; the deficit kernel is the corresponding object for the angular deficit.
The local setting is pure kernel arithmetic on the 15-class stencil: no Hessian assembly, no Einstein–Hilbert recovery, and no transport to the complementary type $(3,1)$.
proof idea
Term-mode proof by exhaustive case analysis. First record $\sqrt{3}\neq 0$ and $(\sqrt{3})^2=3$. Then fin_cases k over the ten class indices. In each branch, unfold the three definitions (deficit kernel, chain factor, cosine kernel), apply field_simp with the nonzero square-root hypothesis, simplify the squared root, and finish by ring. No external lemmas beyond the real-arithmetic API; the identity is definitional once the three tables are expanded.
why it matters
Closes the algebraic link between the cosine and deficit presentations of the full-star 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})$ (module deliverable A.5). Downstream, hinge4DStarKernel13Status_flags uses this (with the rest of the kernel suite) to set fullStarClassKernelClosed = true while leaving type-$(3,1)$ transport and flat Hessian assembly open.
In the broader Recognition gravity stack this is a checked increment toward discrete curvature matching, not a claim that $S_{RS}$ converges to Einstein–Hilbert in 4D, nor a flip of gap_action_recovery. It sits strictly inside the Regge hinge analysis layer imported from the dihedral, flat, and edge-stencil kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.