chainT13
plain-language theorem explainer
The chain factor for the type-(1,3) Regge hinge at flat cosine 1/2 is the real constant -2/√3, i.e. -1/sin with sin=√3/2. Anyone building the star deficit class kernel on the (1,3) Freudenthal orbit cites it when converting cosine derivatives into deficit values. It is a one-line constant definition; the rationalized form -2√3/3 is proved immediately downstream.
Claim. Define the chain factor at flat cosine $1/2$ by $C_{13} := -\frac{2}{\sqrt{3}}$. Equivalently $C_{13} = -\frac{1}{\sin\theta}$ where $\sin\theta = \frac{\sqrt{3}}{2}$ (the sine of the flat dihedral angle $\arccos(1/2)=\pi/3$).
background
In 4D Regge calculus on a periodic lattice, the deficit at a triangle hinge is assembled from the dihedral angles of the Kuhn simplices that meet there. For the type-(1,3) hinge with absolute masks ${0,1,15}$ (local flat squared lengths $(1,3,4)$), every simplex in the origin star has flat cosine $1/2$, so the flat angle is $\pi/3$ and $\sin=\sqrt{3}/2$.
The module is the next kernel-checked increment after the type-(1,1) seed orbit and the orbit classification layer. It imports the Freudenthal incidence data, the 15-class edge stencil, and the Gram-projection cosine calculus, and never redefines their API. The chain factor $-1/\sin$ is the standard conversion coefficient from cosine-kernel derivatives to deficit-kernel values at that flat point.
Scope is the full periodic star of this single hinge class; the complementary type $(3,1)$ is related by mask complement but transport of the kernel remains open.
proof idea
Pure definition: the real equals $-(2/\sqrt{3})$. No tactics and no lemmas. Downstream, chainT13_eq rewrites it to the rationalized form $-(2\sqrt{3})/3$ by field_simp and Real.sq_sqrt; that form is then used in the finitary case split of t13DeficitKernel_eq_chain.
why it matters
Cited by chainT13_eq (rationalized identity) and by t13DeficitKernel_eq_chain, which states that the ten-component deficit kernel equals $-C_{13}$ times the cosine kernel. That identity is the bridge from Gram-projection cosine calculus to 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})$.
It is deliverable A.5 of the type-(1,3) star kernel campaign. It does not complete flat Hessian assembly over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. Transport to the complementary type $(3,1)$ is explicitly open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.