RegularUnitCofactorCheck
plain-language theorem explainer
Isolates the three numerical cofactor identities on the unit regular tetrahedron that force the Cayley-Menger dihedral cosine to equal 1/3. Geometers deriving tetrahedral angles from CM minors cite this predicate instead of re-expanding determinants. It is a pure Prop definition: for each of the six edges, the opposite-vertex cofactors equal 1, -3, and -3.
Claim. For every edge $e$ among the six edges of the unit regular tetrahedron (all squared lengths equal to $1$), if $p$ and $q$ are the Cayley-Menger matrix indices of the two vertices opposite $e$, then the cofactors satisfy $C_{p,q}=1$, $C_{p,p}=-3$, and $C_{q,q}=-3$.
background
The module defines tetrahedral dihedral cosines from Cayley-Menger cofactors. For an edge $e$, let $(p,q)$ be the two vertices opposite that edge. Vertex rows in the $5\times 5$ CM matrix are shifted by one, so vertex $v:\mathrm{Fin},4$ sits at CM index $v+1$. The classical formula is $\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$, with the sign convention that yields $\cos\theta=1/3$ for the regular tetrahedron.
cmCofactor3 is the signed minor $C_{r,c}$ of the CM matrix built from squared edge lengths. regularUnitSqEdges is the constant edge data with every squared length equal to $1$. oppositeCMVertices maps each of the six edges to the pair of CM indices opposite that edge (e.g. edge $(0,1)$ maps to $(3,4)$).
The three equalities $C_{p,q}=1$, $C_{p,p}=-3$, $C_{q,q}=-3$ are exactly what plug into the cofactor formula to give $1/\sqrt{(-3)(-3)}=1/3$. Isolating them as a single Prop keeps the expensive minor expansions out of every downstream call site.
proof idea
No proof: this is a definition of a proposition. The body quantifies over all six edges $e:\mathrm{Fin},6$, unpacks the opposite CM vertex pair $(p,q)$ via oppositeCMVertices, and asserts the three equalities of cmCofactor3 on regularUnitSqEdges. Downstream theorems take a hypothesis of this type and rewrite; the companion theorem regularUnitCofactorCheck later discharges the Prop by case analysis on $e$ and precomputed minor lemmas.
why it matters
This Prop is the single gate between the general cofactor cosine and the classical regular-tetrahedron value $\cos\theta=1/3$. The theorems dihedralCos3_regularUnit_of_cofactorCheck and dihedralAngle3_regularUnit_of_cofactorCheck both take it as hypothesis and conclude agreement with the existing regular-tetrahedron dihedral API. The companion theorem regularUnitCofactorCheck proves the Prop outright, so the check is no longer an assumption.
In the Recognition geometry stack this closes the gap between abstract CM cofactors and the concrete internal dihedral used by Regge-type discrete curvature. The module doc states the goal explicitly: replace the prose reference in DihedralAngle with a Lean definition that recovers $\cos\theta=1/3$. Isolating the numerical check keeps determinant work local and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.