cmCofactor3_eq_poly
plain-language theorem explainer
Every cofactor of the 5×5 tetrahedral Cayley-Menger matrix equals an explicitly named polynomial in the six squared edge lengths. Geometric analysts working on dihedral-angle derivatives or Regge calculus cite this to swap opaque determinant minors for polynomial algebra. The proof is exhaustive case analysis on the twenty-five index pairs, each reduced to a precomputed minor-determinant identity.
Claim. For every assignment $a$ of six squared edge lengths of a tetrahedron and every pair of indices $r,c\in\{0,1,2,3,4\}$, the signed Cayley-Menger cofactor $C_{r,c}(a)$ equals the corresponding explicit cofactor polynomial evaluated at $a$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. Squared edges are packaged as maps $\mathrm{Fin},6\to\mathbb{R}$. The cofactor $C_{r,c}$ is the signed determinant of the complementary $4\times 4$ minor of the bordered distance matrix (the standard $5\times 5$ Cayley-Menger matrix for a tetrahedron).
This is the cofactor analogue of the Cayley-Menger derivative layer: downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives. Each specialized index-pair lemma unfolds the cofactor definition, rewrites the minor as an explicit matrix of edge coordinates, evaluates that determinant as a polynomial, and inserts the cofactor sign $(\pm 1)$ according to parity of $r+c$.
proof idea
Double fin_cases on the row and column indices in $\mathrm{Fin},5$ yields twenty-five goals. Each goal is closed by the matching specialized lemma (one per pair $(i,j)$). Those lemmas unfold the cofactor and minor, rewrite the submatrix equality, evaluate the named minor determinant, and simplify the cofactor sign by parity. No further algebraic work occurs at this level; the theorem is pure case dispatch.
why it matters
This agreement is the bridge from determinant-defined cofactors to polynomial calculus. It feeds the equalities that turn squared dihedral cosines and their denominators into rational functions of edge polynomials, the closed-form coordinate derivative of every cofactor along a single edge length, and positivity of diagonal cofactor products at the flat Freudenthal tetrahedron inside the Regge TT derivative gate. Without the normal-form match, dihedral partials remain stuck behind opaque derivatives and cannot enter the explicit Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.