star_cofactor_44
plain-language theorem explainer
The (4,4) Cayley-Menger cofactor of the unit-slice four-tetrahedron star (hinge and legs squared length 1, free equatorial squared length p) equals the constant -3 for every real p. Anyone assembling the hinge dihedral denominator or cosine on this star cites it. The proof matches the deleted minor to a fixed regular-unit matrix already known to have determinant -3, with cofactor sign +1.
Claim. For every real $p$, the Cayley-Menger cofactor $C_{4,4}$ of the squared-edge data of the four-tetrahedron star with unit hinge and legs and equatorial edge squared length $p$ equals $-3$.
background
The module builds the first kernel-checked signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tetrahedra around a common hinge AB, given only as squared-edge data and certified nondegenerate by Cayley-Menger sign. On the panel-locked unit slice the squared-edge vector is $(1,1,1,1,1,p)$, with free equatorial parameter $p$.
Cayley-Menger cofactors $C_{r,c}$ are signed minors of the $5\times 5$ Cayley-Menger matrix on squared edges. Dihedral cosines at a hinge are ratios of such cofactors. Offline sympy predicts $C_{33}=C_{44}=l(l-4m)=-3$ on $l=m=1$; this theorem kernel-checks the $C_{44}$ half.
Upstream, the $(4,4)$-deleted submatrix of the star Cayley-Menger matrix is identified with a fixed regular-unit diagonal minor matrix whose determinant equals $-3$.
proof idea
Term-mode proof. Unfold the cofactor into the product of the cofactor sign $(-1)^{r+c}$ and the deleted-minor determinant. For indices $4,4$ the exponent is $8$, which is even, so the sign simplifies to $+1$. Rewrite the minor via star_minor_44_eq, which equates the deleted submatrix to regularUnitDiagMinorMatrix, then apply det_regularUnitDiagMinorMatrix to obtain $-3$.
why it matters
Direct input to star_denom, which asserts that the hinge dihedral denominator on the star is the constant $3$ (square root of the product of the two diagonal cofactors $C_{33}$ and $C_{44}$). That denominator is the bottom half of the kernel-checked cosine $q(p)=(3-2p)/3$ used to certify the signed deficit $\mathrm{deficit}(h)=4\arcsin(h)$ by the sign of the rational quantity $h$, with no arccos evaluation or interval arithmetic.
This sits inside the Geometry track that supplies signed Regge deficits for hinge-aware analysis; it is not itself a step of the T0-T8 forcing chain. It closes the $C_{44}$ half of the unit-slice cofactor table needed for the four-tet star deficit package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.