star_cofactor_34
plain-language theorem explainer
The Cayley–Menger cofactor C_{3,4} on the unit-hinge star tetrahedron with rim squared length p equals the linear polynomial 3−2p. Anyone computing the central dihedral cosine of the four-tet hinge star cites this identity. The proof unfolds the cofactor as signed minor, inserts the precomputed 3×3 determinant 2p−3, and finishes by ring.
Claim. For every real $p$, the Cayley–Menger cofactor $C_{3,4}$ of the squared-edge data $(1,1,1,1,1,p)$ equals $3-2p$.
background
The module studies an abstract four-tetrahedron hinge star: four congruent tets around a common edge AB, given only as squared-edge data and certified nondegenerate by the Cayley–Menger sign. The one-parameter family used here freezes the hinge and spoke squared lengths at 1 and varies the equatorial rim length $p$, written starSq p $=(1,1,1,1,1,p)$ with AB as edge 0.
Dihedral cosines in the repository are extracted from Cayley–Menger cofactors. A cofactor $C_{r,c}$ is the signed minor obtained by deleting row $r$ and column $c$ from the $5\times5$ Cayley–Menger matrix and multiplying by $(-1)^{r+c}$. The off-diagonal pair $(3,4)$ is the hinge-facing cofactor that enters the cosine formula for edge 0.
Upstream, the deleted submatrix is identified with an explicit $3\times3$ matrix whose determinant is already computed as $\det=2p-3$. The present lemma only packages that determinant into the signed cofactor.
proof idea
Unfold the cofactor into sign times minor. The index sum $3+4=7$ is odd, so the sign is $-1$ (discharged by a one-line parity check). Rewrite the minor via the matrix-equality lemma that matches the deleted submatrix to the explicit star minor, then substitute the determinant identity $\det=2p-3$. The remaining arithmetic $- (2p-3)=3-2p$ is closed by ring.
why it matters
This is the numerator half of the kernel-checked rational certificate for the central dihedral cosine on the $l=m=1$ slice. The parent theorem fourTet_centralDihedralCosine rewrites the repository cosine formula and obtains $q(p)=(3-2p)/3$ by combining this cofactor with the matching diagonal denominator cofactor.
That rational $q$ is the bridge from squared-edge data to signed Regge deficit: on the deformation $p=(3/2)(1-h)$ one has $q=h$ exactly, so $\mathrm{deficit}(h)=4\arcsin(h)$ and the sign of the deficit is the sign of a rational, with no arccos numerics. The module’s claim to supply the first kernel-checked signed deficits on an abstract four-tet star rests on this algebraic step.
Within Recognition geometry this is pure classical Cayley–Menger algebra supporting discrete curvature bookkeeping; it does not itself invoke the forcing chain T0–T8, but it supplies the local curvature sign needed for later discrete-gravity comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.