star_cofactor_33
plain-language theorem explainer
On the one-parameter four-tet star with hinge and spoke squared lengths 1 and rim squared length p, the Cayley-Menger diagonal cofactor C_{3,3} equals -3 for every real p. Anyone assembling the dihedral cosine or its denominator on this star cites the identity. The proof matches the (3,3)-minor to a fixed regular unit-diagonal matrix already known to have determinant -3, with positive cofactor sign.
Claim. For every real $p$, the Cayley-Menger cofactor $C_{3,3}$ of the squared-edge data $(1,1,1,1,1,p)$ equals $-3$.
background
The module studies signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link. Squared edges are locked to the panel $(l,m,m,m,m,p)$; the kernel-checked slice is $l=m=1$, encoded by starSq p as the squared-edge vector $(1,1,1,1,1,p)$ with hinge edge 0.
Cayley-Menger cofactors supply the dihedral cosine at the hinge. The 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 prose offline formula predicts $C_{33}=C_{44}=l(l-4m)$, hence $-3$ on the unit slice; this theorem is the kernel check of that constant.
Upstream, star_minor_33_eq identifies the deleted submatrix with the fixed matrix regularUnitDiagMinorMatrix, whose determinant is already computed as $-3$ by det_regularUnitDiagMinorMatrix.
proof idea
Term-mode proof. Unfold the cofactor into sign times minor. The index sum $3+3=6$ is even, so the cofactor sign is $+1$ (discharged by norm_num). Rewrite the minor via star_minor_33_eq, which equates the deleted submatrix of cmMatrix3 (starSq p) to regularUnitDiagMinorMatrix. Finish by det_regularUnitDiagMinorMatrix, giving determinant $-3$, hence cofactor $-3$.
why it matters
Feeds star_denom, which assembles the hinge dihedral denominator as $\sqrt{C_{33}C_{44}}=3$ (constant, independent of $p$). That constant denominator, together with the companion numerator cofactor, yields the kernel-checked cosine $q(p)=(3-2p)/3$ on the star and the signed deficit $4\arcsin(h)$ along the deformation $p=(3/2)(1-h)$. The result is a concrete algebraic step in the first repository theorem tier for signed Regge deficits on an abstract four-tet star, certifying sign without arccos evaluation or interval arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.