cmCofactorSign3
plain-language theorem explainer
Cofactor sign for the 5×5 Cayley–Menger matrix of a tetrahedron: +1 or −1 according as the sum of the row and column indices is even or odd, i.e. (−1)^{r+c} as a real. Anyone expanding CM cofactors for dihedral cosines or volume identities cites it. The body is a one-line parity branch on Fin 5 values.
Claim. For indices $r,c\in\{0,1,2,3,4\}$, the cofactor sign is $1$ if $r+c$ is even and $-1$ if $r+c$ is odd (equivalently $(-1)^{r+c}\in\mathbb{R}$).
background
This module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant. That determinant/cofactor layer is what the dihedral cosine formula needs.
Row/column layout is fixed: index 0 is the bordering ones-row/column; indices 1–4 label the four vertices; off-diagonal blocks hold the six squared edge lengths $a_0,\ldots,a_5$ for pairs $(01),(02),(03),(12),(13),(23)$. A cofactor is the signed minor $C_{r,c}=(-1)^{r+c}M_{r,c}$. This definition isolates the pure sign factor as a real, so later lemmas can multiply it by the corresponding $4\times 4$ minor without re-deriving parity each time.
proof idea
Pure definition, not a proof. On Fin 5 indices it returns 1 when Even (r.val + c.val) and -1 otherwise. That is exactly the real value of $(-1)^{r+c}$. Downstream code unfolds it and discharges the parity goal with decide or simp.
why it matters
Immediate parent is the cofactor constructor, which multiplies this sign by the corresponding minor. That cofactor is then evaluated on the regular unit tetrahedron for every off-diagonal pair $(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)$ and on the vertex-diagonal slots; those identities feed the dihedral-cosine and volume pipeline.
In the Recognition geometry stack this is the sign bookkeeping for the tetrahedron in $D=3$ (forcing landmark T8). Without a uniform real-valued sign, the cofactor expansion of the CM determinant cannot be stated uniformly across all index pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.