cmCofactor3_41_eq_poly
plain-language theorem explainer
The (4,1) cofactor of the tetrahedral Cayley-Menger matrix equals a fixed explicit polynomial in the six squared edge lengths. Cite this when replacing an opaque minor determinant by a named algebraic expression in edge coordinates. The proof unfolds the cofactor, matches the deleted submatrix to a pre-expanded determinant, and fixes the odd-parity sign factor.
Claim. For every assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{4,1}(a)$ equals the explicit polynomial normal form $\mathrm{Poly}_{4,1}(a)$ in those six coordinates.
background
The tetrahedral Cayley-Menger matrix is the standard $5\times 5$ bordered matrix of squared distances among four points. Its cofactors $C_{r,c}$ are sign times the determinant of the matrix with row $r$ and column $c$ deleted; they appear in classical formulas for dihedral angles and for derivatives of volume with respect to edges.
This module expands every such cofactor as an explicit polynomial in the six squared edge coordinates (SqEdges). The abstract cofactor is sign(r,c) * det(submatrix), while the polynomial form is a match on the pair $(r,c)$ giving the fully expanded expression in the six edge variables.
Upstream, the concrete submatrix after deleting row 4 and column 1 is identified entrywise with a named matrix whose determinant has already been expanded as a polynomial.
proof idea
Unfold the cofactor into sign times minor. Rewrite the deleted submatrix via the entrywise identity that equates it to the named $(4,1)$-minor matrix, then replace that matrix's determinant by its precomputed polynomial expansion. Finally simplify the cofactor sign: $4+1=5$ is odd, so the sign is $-1$, and the result matches the $(4,1)$ branch of the polynomial normal form.
why it matters
This is one arm of the exhaustive fin_cases split that proves every tetrahedral Cayley-Menger cofactor equals its polynomial normal form. That global agreement is the module's main theorem: downstream dihedral-angle calculus can then cite named polynomial partials instead of opaque fderiv terms, exactly as the module documentation requires.
In the broader Recognition geometry stack, explicit cofactor polynomials keep simplex and rigid-body calculus inside an algebraic edge-coordinate ring, ready for later specialization to phi-ladder edge data. The result is fully proved; it closes no open scaffold, it simply discharges one concrete index pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.