regularUnit_cofactor_13
plain-language theorem explainer
For the unit regular tetrahedron (all squared edges 1), the Cayley–Menger cofactor C_{1,3} equals 1. Anyone checking the dihedral cosine formula on the regular case cites this. The proof unfolds the cofactor, notes the sign is +1, and reduces the minor to a precomputed 4×4 determinant equal to 1.
Claim. Let $a$ be the squared-edge data of the unit regular tetrahedron (every edge length squared equals $1$). Then the Cayley–Menger cofactor $C_{1,3}(a)$ equals $1$.
background
This module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger matrix, its minors, and cofactors. The matrix convention places a border of ones around the $4\times 4$ block of squared edge lengths $a_0,\ldots,a_5$ for edges $(01),(02),(03),(12),(13),(23)$.
A cofactor is $C_{r,c}=(-1)^{r+c}$ times the determinant of the matrix with row $r$ and column $c$ deleted. The sign factor is the real number $+1$ or $-1$ according as $r+c$ is even or odd. The unit regular tetrahedron is the constant edge datum with every squared length equal to $1$.
Upstream, the $(1,3)$-minor of that regular matrix is identified with an explicit off-diagonal $4\times 4$ matrix whose determinant has already been computed to be $1$.
proof idea
Unfold the cofactor into sign times minor. The indices $1$ and $3$ sum to $4$, which is even, so the sign simplifies to $+1$. Rewrite the minor via the identification of the deleted submatrix with the regular off-diagonal minor matrix, then apply the already-proved fact that that matrix has determinant $1$. The whole argument is a short term/tactic chain: unfold, parity simp, two rewrites.
why it matters
The dihedral cosine formula needs concrete cofactor values on the regular unit tetrahedron. Downstream, regularUnitCofactorCheck packages six such evaluations (including this $C_{1,3}=1$) and thereby turns the regular-unit cofactor hypothesis into a proved theorem rather than an assumption.
That check sits in the geometry layer that feeds Recognition Science’s rigid spatial structure: once cofactors are under control, dihedral angles of the regular simplex are available as exact algebraic numbers, consistent with the forcing of $D=3$ spatial dimensions (T8) and the discrete octave geometry built earlier in the chain. No open scaffold remains on this particular entry; it is a closed algebraic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.