det_cmMinor22Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley-Menger minor for cofactor index (2,2) equals the named polynomial normal form in the six squared edge lengths. Anyone expanding tetrahedral CM cofactors or feeding dihedral-angle calculus from those polynomials would cite this identity. The proof unfolds both sides, expands the 4×4 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_{2,2}(a) = P_{2,2}(a)$, where $M_{2,2}(a)$ is the explicit $4\times 4$ Cayley-Menger minor matrix for cofactor $(2,2)$ and $P_{2,2}$ is the corresponding explicit cofactor polynomial in those six squared lengths.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The cofactor polynomial family supplies a closed-form normal form $P_{r,c}(a)$ for each entry of the $5\times 5$ bordered Cayley-Menger matrix. The minor matrix for index $(2,2)$ is the concrete $4\times 4$ array
$$\begin{pmatrix}0&1&1&1\1&0&a_1&a_2\1&a_1&0&a_5\1&a_2&a_5&0\end{pmatrix},$$
the normal form of the diagonal minor used by cofactor $(2,2)$.
This lemma is the pure determinant identity that later equates the abstract CM cofactor at $(2,2)$ to that polynomial.
proof idea
Term/tactic hybrid, four lines. Unfold the minor-matrix definition and the cofactor-polynomial definition so both sides are concrete expressions in the six edge squares. Apply Matrix.det_succ_row_zero together with the standard Fin summation and succAbove rewrites to expand the $4\times 4$ determinant along its first row (the bordered row of ones and a zero). The resulting multilinear polynomial identity is discharged by ring_nf.
why it matters
Immediate parent is the agreement theorem that the abstract Cayley-Menger cofactor at $(2,2)$ equals the explicit polynomial: that proof rewrites the abstract minor to this matrix, applies the present determinant identity, and adjusts the cofactor sign (even parity of $4$).
Together with the sibling identities for the other minors ($(3,4)$, $(2,4)$, $(2,3)$, \ldots), it closes the cofactor half of the module's programme: every tetrahedral CM cofactor becomes a named polynomial in the six squared edges. That is the cofactor analogue of the Cayley-Menger derivative expansions, and it is what lets dihedral-angle calculus work with ordinary partial derivatives of polynomials rather than opaque fderiv terms. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched directly; the result is pure classical geometry scaffolding inside the RS geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.