cmCofactor3_11_eq_poly
plain-language theorem explainer
The (1,1) 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 determinants by polynomial normal forms. The proof unfolds the cofactor, matches the deleted submatrix to a hand-built 4×4 matrix, evaluates that determinant, and fixes the sign (+1).
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley–Menger cofactor $C_{1,1}(a)$ equals the explicit polynomial $\mathrm{Poly}_{1,1}(a)$ in those six coordinates.
background
The module expands every cofactor of the $5\times5$ tetrahedral Cayley–Menger matrix into a named polynomial in the six squared edge coordinates (SqEdges). Downstream dihedral-angle work can then differentiate those polynomials instead of opaque fderiv terms on determinants.
The cofactor is defined as $C_{r,c}=(-1)^{r+c},M_{r,c}$, where $M_{r,c}$ is the determinant of the matrix obtained by deleting row $r$ and column $c$. The sign factor is $+1$ or $-1$ according as $r+c$ is even or odd. The companion object cmCofactor3Poly is the closed-form polynomial for each index pair.
This lemma is the $(1,1)$ case of that dictionary: it identifies the abstract cofactor at indices $(1,1)$ with the corresponding polynomial entry.
proof idea
Term-mode, four steps. Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix of the Cayley–Menger matrix. Rewrite that submatrix via the sibling identity that equates the deleted $(1,1)$ block to an explicitly constructed $4\times4$ matrix, then replace the determinant by the precomputed polynomial det_cmMinor11Matrix. Finally simp on the sign definition: $1+1=2$ is even, so the sign is $+1$ and the two sides match.
why it matters
Feeds the master agreement theorem that every tetrahedral Cayley–Menger cofactor equals its polynomial normal form (proved by fin_cases on all index pairs, with this lemma as the $(1,1)$ branch). Also feeds the diagonal specialization used by tetrahedral dihedral cosine denominators, which only need opposite-vertex diagonal cofactors.
In the Recognition geometry stack this is bookkeeping, not a forcing-chain step: it makes the Cayley–Menger route to dihedral angles fully algebraic in the six edge squares, so later calculus (partials, critical-point conditions) stays inside named polynomials rather than symbolic determinants. No T0–T8 landmark is discharged here; the value is reusable, inspectable algebra for 3D simplex geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.