cmCofactor3_22_eq_poly
plain-language theorem explainer
The (2,2) cofactor of the tetrahedral Cayley-Menger matrix equals a named explicit polynomial in the six squared edge lengths. Anyone computing dihedral-angle denominators or differentiating CM cofactors cites this cell identity. The proof unfolds the cofactor, replaces the minor by its closed 4×4 determinant polynomial, and simplifies the even-parity sign to +1.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{2,2}(a)$ equals the corresponding explicit polynomial in those six coordinates.
background
This 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.
The bordered Cayley-Menger matrix encodes squared distances among four points. Its cofactor $C_{r,c}$ is the signed determinant of the minor obtained by deleting row $r$ and column $c$, with sign $(-1)^{r+c}$. Indices run over a $5\times 5$ bordered matrix. The input type packages the six independent squared edge lengths.
The companion polynomial definition supplies the expanded form for each index pair. Upstream, the cofactor is defined as sign times minor determinant; this theorem asserts agreement specifically at the diagonal cell $(2,2)$.
proof idea
Unfold the cofactor into sign times minor determinant. Rewrite that minor via the dedicated submatrix identity for the $(2,2)$ deletion and the closed-form determinant of the resulting explicit $4\times 4$ matrix. Then simplify: the cofactor sign at indices $(2,2)$ is $(-1)^{2+2}=(-1)^4=+1$ because $4$ is even (discharged by decide), so the signed minor collapses exactly to the named polynomial.
why it matters
Feeds the master agreement theorem that cases on every $\mathrm{Fin},5\times\mathrm{Fin},5$ index pair and invokes each cell-wise identity. Also used by the opposite-diagonal packaging theorem, whose doc-comment states it covers "every diagonal cofactor used by tetrahedral dihedral cosine denominators."
Explicit polynomials let Recognition Science geometry differentiate dihedral angles algebraically rather than through opaque derivative terms. That supports the geometric side of the framework once $D=3$ spatial dimensions are forced (T8), where tetrahedral Cayley-Menger data are the natural distance coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.