cmCofactor3_10_eq_poly
plain-language theorem explainer
The (1,0) cofactor of the tetrahedral Cayley-Menger matrix equals the named explicit polynomial in the six squared edge lengths. Geometry and dihedral-angle calculus cite it when replacing opaque minors by closed forms. The proof unfolds the cofactor, identifies the deleted submatrix with a hand-built 4×4 matrix, and evaluates its determinant against the polynomial normal form.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{1,0}(a)$ equals the explicit polynomial $\mathrm{cmCofactor3Poly}(1,0;a)$ in those six coordinates.
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 use named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The Cayley-Menger cofactor $C_{r,c}$ is the signed minor obtained by deleting row $r$ and column $c$ from the $5\times5$ Cayley-Menger matrix and multiplying by $(-1)^{r+c}$. The companion definition cmCofactor3Poly is a match on $(r,c)$ that writes each of the twenty-five cofactors as a concrete multilinear polynomial in the six edges.
Upstream, cmMinor10_submatrix_eq identifies the concrete submatrix after deleting row 1 and column 0 with a named $4\times4$ matrix whose determinant is already expanded by det_cmMinor10Matrix.
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix of cmMatrix3 a. Rewrite that submatrix via cmMinor10_submatrix_eq to the hand-built matrix cmMinor10Matrix a, then replace its determinant by the already-proved expansion det_cmMinor10Matrix. A final simp inserts the cofactor sign: $1+0$ is odd, so the sign is $-1$, matching the polynomial normal form for indices $(1,0)$.
why it matters
This is one cell in the exhaustive case split that proves cmCofactor3_eq_poly: every determinant cofactor of the tetrahedral Cayley-Menger matrix agrees with the explicit polynomial normal form. That global agreement is the cofactor analogue of the Cayley-Menger derivative expansions; it lets dihedral-angle identities and volume calculus work with named polynomials rather than symbolic minors.
In the Recognition geometry stack these polynomials feed rigid-embedding and angle constraints on the tetrahedron, which sit under the $D=3$ spatial forcing (T8) and the eight-tick discrete structure. The declaration itself is fully proved scaffolding closure for the $(1,0)$ entry; no open hypothesis remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.