cmCofactor3_opposite_eq_poly
plain-language theorem explainer
For any squared-edge assignment of a tetrahedron and any of the six edges, the Cayley–Menger cofactor at the vertex pair opposite that edge equals the matching explicit cofactor polynomial. Anyone writing tetrahedral dihedral cosines in edge coordinates cites this to swap opaque minors for named polynomials. The proof is a six-way case split on the edge index, each arm a prior pairwise identity.
Claim. Let $a$ be an assignment of six squared edge lengths of a tetrahedron, and let $e\in\{0,\ldots,5\}$ index an edge. Write $(r,c)$ for the pair of Cayley–Menger vertex indices opposite $e$. Then the cofactor $C_{r,c}(a)$ equals the explicit polynomial $\mathrm{Poly}_{r,c}(a)$ 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 $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$. The cofactor $C_{r,c}$ is the signed $3\times 3$ minor of the $5\times 5$ Cayley–Menger matrix obtained by deleting row $r$ and column $c$. The companion object $\mathrm{cmCofactor3Poly},r,c$ is the same quantity written as a concrete polynomial in the six edge squares.
Dihedral cosine formulas for a tetrahedron need, for each edge, the cofactor at the two vertices opposite that edge (the numerator of the cosine). The map oppositeCMVertices sends an edge index to that vertex pair in the Cayley–Menger indexing. Six prior lemmas already equate $C_{r,c}$ with $\mathrm{Poly}_{r,c}$ for each unordered pair among ${1,2,3,4}$.
proof idea
Tactic proof by exhaustive case analysis on the edge index $e:\mathrm{Fin},6$. After fin_cases e, each goal is exactly one of the six pairwise polynomial-agreement theorems already proved in this module:
- opposite pair $(3,4)$ via
cmCofactor3_34_eq_poly, - $(2,4)$ via
cmCofactor3_24_eq_poly, - $(2,3)$ via
cmCofactor3_23_eq_poly, - $(1,4)$ via
cmCofactor3_14_eq_poly, - $(1,3)$ via
cmCofactor3_13_eq_poly, - $(1,2)$ via
cmCofactor3_12_eq_poly.
Each arm is a one-line exact. Those pairwise lemmas themselves unfold the signed minor, rewrite the submatrix to an explicit $3\times 3$ matrix of edge squares, expand the determinant, and simplify the cofactor sign.
why it matters
This is the single entry point that packages all six numerator cofactors used by tetrahedral dihedral cosines. The module doc positions the whole file as the cofactor analogue of CayleyMengerDerivatives: once every $C_{r,c}$ is a named polynomial, partial derivatives with respect to edge squares become ordinary polynomial calculus rather than abstract fderiv terms.
In the Recognition geometry stack, dihedral angles of the fundamental simplex feed volume, curvature, and packing identities that sit downstream of the forcing chain’s $D=3$ and eight-tick octave landmarks. Having opposite-edge cofactors as polynomials is the algebraic prerequisite for differentiating those angles in edge coordinates without leaving the explicit polynomial ring.
No downstream consumers are wired yet in the dependency graph (used_by is empty), so this theorem is presently a ready interface rather than a load-bearing step of a larger proved chain. It closes the “every opposite cofactor agrees with its polynomial” obligation stated in the declaration’s own doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.