dihedralCofactorPoly_discriminant_eq
plain-language theorem explainer
For any tetrahedron edge, the Cayley–Menger cofactor Gram discriminant equals twice the Cayley–Menger volume polynomial times that squared edge length. Anyone working dihedral cosines, Schläfli identities, or radical-free sin² expressions cites this. The proof is a one-line term wrapper of the existing polynomial discriminant identity.
Claim. Let $a$ be the six squared edge lengths of a tetrahedron and let $e$ be any edge. Write $p,q$ for the two Cayley–Menger vertex indices opposite $e$. Then the cofactor Gram discriminant satisfies $C_{pp}(a)\,C_{qq}(a)-C_{pq}(a)^2=2\,\mathrm{CM}_3(a)\,a_e$.
background
Squared edge lengths of a tetrahedron are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The scalar $\mathrm{CM}3(a)$ is the explicit Cayley–Menger polynomial in those six lengths; it vanishes precisely on degenerate embeddings. Each entry $C{rc}(a)$ is the matching polynomial cofactor of the bordered Cayley–Menger matrix, given in closed form by cmCofactor3Poly.
For a fixed edge $e$, the pair $(p,q)$ of opposite Cayley–Menger vertices is supplied by oppositeCMVertices. The $2\times 2$ Gram block of cofactors on that pair is exactly the algebraic content of the dihedral cosine denominator: its determinant is the quantity controlled here.
The module sits in the calculus layer for Cayley–Menger cofactors and dihedral ratios. Upstream, cmCofactor_discriminant_eq already records the same identity and notes that it "turns the arccos denominator into the common volume factor in Schläfli."
proof idea
One-line term wrapper: the statement is definitionally identical to cmCofactor_discriminant_eq a e, which already expands the opposite-vertex pair and proves $C_{pp}C_{qq}-C_{pq}^2=2,\mathrm{CM}_3(a),a_e$ by direct polynomial algebra on the six edge variables. No extra rewriting is required.
why it matters
This is the local name under which the cofactor discriminant is consumed by the dihedral derivative interfaces. Downstream, one_sub_dihedralCos3SqPoly_sq_eq uses it to obtain a radical-free expression for $1-\cos^2$ of the dihedral angle (the algebraic $\sin^2$ identity). Separately, dihedralCofactorProductPoly_pos_of_nonDegenerate feeds the same equality into a positivity argument: for a nondegenerate tetrahedron the product of opposite cofactors is strictly positive on every edge.
In the broader Recognition geometry stack this identity is the bridge from pure Cayley–Menger algebra to dihedral cosine denominators, which is the input needed for closed-form derivatives of dihedral angles and for Schläfli-type volume variations. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is pure tetrahedral geometry scaffolding those later analytic steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.