dihedralCos3
plain-language theorem explainer
Defines the dihedral cosine of a nondegenerate tetrahedron along any of its six edges by evaluating the Cayley–Menger cofactor formula on the tetrahedron’s squared edge lengths. Anyone working with Regge calculus, discrete curvature, or tetrahedral dihedral angles in the geometry stack will cite it. The body is a one-line wrapper around the squared-edge cofactor cosine.
Claim. For a nondegenerate tetrahedron $T$ (positive squared edge lengths and positive Cayley–Menger determinant) and an edge index $e \in \{0,\ldots,5\}$, the dihedral cosine of $T$ at $e$ is the real number obtained by applying the Cayley–Menger cofactor cosine formula to the squared edge lengths of $T$ at $e$.
background
This module supplies a Lean definition of tetrahedral dihedral cosines from Cayley–Menger cofactors, replacing earlier prose references. For an edge $e=(i,j)$, let $(p,q)$ be the two opposite vertices. Vertex rows in the $5\times 5$ Cayley–Menger matrix are shifted by one, so vertex $v$ maps to CM index $v+1$. The classical formula is
$$\cos\theta_e = C_{p,q}/\sqrt{C_{p,p}C_{q,q}},$$
where $C$ is the cofactor matrix. The sign convention yields $\cos\theta=1/3$ on the regular tetrahedron (internal dihedral).
A NonDegenerateTet packages squared edge lengths that are strictly positive and whose Cayley–Menger $3$-volume determinant is positive. The sibling dihedralCos3Sq already implements the cofactor ratio on raw squared-edge data; the present definition simply feeds it $T$'s squared edges.
proof idea
One-line definitional wrapper: evaluate dihedralCos3Sq on T.sqEdge at edge index e. No tactics or lemmas are invoked; the mathematical content lives entirely in dihedralCos3Sq (cofactor numerator over the geometric mean of the two diagonal cofactors of the opposite CM vertices).
why it matters
This is the typed entry point that lifts the squared-edge cofactor cosine onto the nondegenerate-tetrahedron API used throughout the geometry and Regge stacks. Downstream it feeds dihedralAngle3 (arccos of this cosine), dihedralAngleData3 (packaging into the existing dihedral-angle data structure), the regular-unit identity dihedralCos3_regularUnit (proving $\cos\theta=1/3$ with no external assumptions), interior-range theorems in DihedralCofactorFormula, and smoothness/chart constructions such as LocalAnalyticFlatChart. In the broader Recognition geometry program it is the concrete cosine that Regge hinge and curvature analyses consume when they need dihedral data from edge lengths alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.