det_cmMinor10Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for index pair (1,0) equals the negative of the named cofactor polynomial in the six squared edge lengths. Anyone proving abstract cofactors match polynomial normal forms cites this identity. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, $\det M_{1,0}(a) = -P_{1,0}(a)$, where $M_{1,0}(a)$ is the $4\times 4$ matrix with first row $(1,1,1,1)$ and remaining rows the squared-edge entries $(a_0,0,a_3,a_4)$, $(a_1,a_3,0,a_5)$, $(a_2,a_4,a_5,0)$, and $P_{1,0}$ is the explicit polynomial normal form of the $(1,0)$-cofactor of the bordered Cayley–Menger matrix.
background
This module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can use named polynomial partials instead of opaque Fréchet derivatives.
Squared edge lengths are packaged as maps $a:\mathrm{Fin},6\to\mathbb{R}$. The definition of the minor hard-codes the $4\times 4$ submatrix obtained by deleting row 1 and column 0 of the bordered Cayley–Menger matrix (1-border, zeros on the squared-distance diagonal). The companion definition supplies a closed-form polynomial for every cofactor index pair $(r,c)$; the $(1,0)$ arm is the target of this identity.
Classical Cayley–Menger theory recovers volume and dihedral data from these minors and cofactors. The present lemma is the pure algebraic bridge from the concrete minor matrix to that polynomial normal form.
proof idea
Unfold the minor matrix and the target cofactor polynomial. Expand the $4\times 4$ determinant along the first row via the successor-row Laplace identity, with the usual Fin sum and succAbove bookkeeping. The resulting cubic expression in the six edge variables is identified with the negative of the $(1,0)$ polynomial by ring normalization. No geometric lemmas are invoked; the equality is multilinear algebra on $\mathbb{R}^6$.
why it matters
This identity is the computational step inside the agreement theorem that equates the abstract Cayley–Menger cofactor at indices $(1,0)$ to the explicit polynomial normal form (after the odd-parity cofactor sign). That agreement result is one of a sibling family (minors 34, 24, 23, …) discharging the module’s purpose: replace opaque cofactors by named polynomials so dihedral-angle derivatives become ordinary partials of polynomials in squared edges.
In the Recognition geometry stack these cofactor polynomials sit under the Cayley–Menger infrastructure for rigid tetrahedral configurations. The lemma itself is classical determinant algebra, not a forcing-chain step, but it is required scaffolding for any later calculus that differentiates dihedral data with respect to edge lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.