det_cmMinor13Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for index pair (1,3) equals the named cofactor polynomial in the six squared edge lengths. Anyone expanding tetrahedral cofactors for dihedral-angle calculus cites this identity. The proof unfolds both sides and reduces the 4×4 determinant by row expansion and ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the normal-form $4\times 4$ minor matrix associated to cofactor indices $(1,3)$ equals the explicit cofactor polynomial $\mathrm{cmCofactor3Poly}(1,3;a)$.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then refer to named polynomial partials instead of opaque Fréchet derivatives.
Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The cofactor polynomial family cmCofactor3Poly is a match on row/column indices giving a fixed multilinear expression in those six coordinates. The companion matrix cmMinor13Matrix is the concrete $4\times 4$ array
$$\begin{pmatrix}0&1&1&1\1&a_0&0&a_4\1&a_1&a_3&a_5\1&a_2&a_4&0\end{pmatrix}$$
used as the normal form of the minor for cofactor $(1,3)$.
This lemma equates the ordinary matrix determinant of that minor with the corresponding branch of the polynomial table.
proof idea
Unfold both cmMinor13Matrix and cmCofactor3Poly so the goal is a concrete $4\times 4$ determinant equal to a fixed polynomial expression. Expand the determinant along the first row via Matrix.det_succ_row_zero, together with the finite-sum and succAbove simplifiers that discharge the resulting $3\times 3$ minors. Finish by ring_nf, which identifies the expanded multilinear form with the tabulated polynomial for indices $(1,3)$.
why it matters
Feeds directly into cmCofactor3_13_eq_poly, which proves that the abstract Cayley–Menger cofactor cmCofactor3 a 1 3 equals the explicit polynomial. That bridge is the cofactor analogue of the derivative expansions in CayleyMengerDerivatives: once every cofactor is a named polynomial, partial derivatives and dihedral-angle formulae become algebraic rather than analytic.
In the broader Recognition geometry stack, tetrahedral Cayley–Menger data underwrite volume, orientation, and angle identities used when discrete recognition structure is realized in three spatial dimensions (forcing landmark T8). Closing the cofactor-to-polynomial equalities removes scaffolding between the matrix definition of the Cayley–Menger determinant and the explicit rung-ladder calculus that downstream mass and coupling formulae expect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.