fourTet_centralDihedralCosine
plain-language theorem explainer
For the one-parameter four-tetrahedron hinge star with unit hinge and legs, the Cayley-Menger cofactor formula for the common dihedral cosine at the hinge equals the rational function $(3-2p)/3$ of the rim squared length $p$. Workers on signed Regge deficits for abstract stars cite this as the kernel-checked $l=m=1$ slice of the general cofactor formula. The proof unfolds the cofactor definition, fixes opposite vertices for the hinge edge, and rewrites by the precomputed star cofactor and denominator identities.
Claim. For every real $p$, let $a(p)$ be the squared-edge data of the star tetrahedron with hinge and leg lengths squared equal to $1$ and equatorial rim length squared equal to $p$. Then the Cayley-Menger dihedral cosine of $a(p)$ at the hinge edge equals $(3-2p)/3$.
background
The module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tetrahedra share an interior hinge $AB$ in a closed 4-cycle link. Squared edges are locked to the panel $(l,m,m,m,m,p)$ in the repository edge convention (hinge is edge 0). Congruence forces all four dihedral angles at $AB$ equal; their common cosine is the repository Cayley-Menger cofactor formula (off-diagonal cofactor over the adjacent-minor denominator).
On the kernel-checked slice $l=m=1$ the configuration is the one-parameter family of squared-edge vectors with rim parameter $p$. Upstream, the hinge cofactor identity evaluates $C_{34}$ to $3-2p$, and the opposite-vertex map for edge 0 returns Cayley-Menger indices $(3,4)$. Offline, the general cofactor ratio $q(l,m,p)=(l-4m+2p)/(l-4m)$ specializes exactly to $(3-2p)/3$ here. The algebraic identity is stated for all real $p$; a geometric dihedral-angle reading needs the nondegenerate window $0<p<3$.
proof idea
Term-mode, four rewrites. Unfold the cofactor cosine definition (ratio of the off-diagonal Cayley-Menger cofactor to the dihedral denominator). Simplify the opposite-vertex pair for hinge edge 0 to indices $(3,4)$. Rewrite the numerator by the star hinge-cofactor theorem ($C_{34}=3-2p$) and the denominator by the matching star-denominator identity (value $3$). The target rational $(3-2p)/3$ is then definitional.
why it matters
This is the rational certificate named in the module header: the only kernel-checked slice of the prose general formula $q(l,m,p)$. Downstream, the regular sanity anchor specializes at $p=1$ to cosine $1/3$, matching the standard regular-tetrahedron cofactor value. The deformation theorem then sets $p(h)=(3/2)(1-h)$ and obtains cosine exactly equal to $h$, so the star-local deficit $2\pi-4\arccos(h)=4\arcsin(h)$ has sign certified by the rational $h$ alone (no arccos bounds, no interval arithmetic).
In the Recognition geometry stack this supplies the first proved signed Regge deficit on an abstract four-tet star in $D=3$, with explicit mesh bounds in the weak-field regime. It does not yet encode a full Triangulation3D or a closed coordinate link; it is the algebraic hinge kernel those later objects will quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.