geometricDihedralCos_edge1_eq_cmCofactorRatio
plain-language theorem explainer
For a realized tetrahedron, the geometric dihedral cosine at edge 1 equals the Cayley-Menger cofactor ratio built from its squared edge lengths at that same edge. Anyone assembling Berger's cofactor formula for all six tetrahedral edges cites this case. The proof unfolds both cosine definitions, rewrites via two cofactor-to-geometry identities for edge 1, and cancels a common factor of four by field simplification.
Claim. For every realized tetrahedron $T$, the geometric dihedral cosine at edge $1$ equals the Cayley-Menger dihedral cosine of the squared edge lengths of $T$ at edge $1$. Explicitly, if $C_{r,c}$ denotes the Cayley-Menger cofactor of those squared lengths, then $$\frac{N_{\mathrm{geom}}(T,1)}{\sqrt{D_{\mathrm{geom}}(T,1)}} = \frac{C_{2,4}}{\sqrt{C_{2,2}\,C_{4,4}}},$$ where the left-hand side is the normalized inner product of the two adjacent face normals at edge $1$.
background
This module builds the Euclidean geometric dihedral cosine for a tetrahedron: face normals arise as cross products of edge vectors on adjacent faces, and the cosine is their normalized inner product. The module target is Berger's cofactor formula, equating that geometric cosine to a pure distance expression.
On the algebraic side, the Cayley-Menger presentation defines the same cosine as $C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$, where $C_{r,c}$ is the signed minor cofactor of the $5\times 5$ bordered squared-distance matrix, and $(p,q)$ are the two Cayley-Menger vertices opposite the chosen edge. A realized tetrahedron supplies four embedded points; its squared edge lengths feed both presentations.
Edge index $1$ selects opposite CM vertices $2$ and $4$. Upstream results already match $C_{2,4}$ to four times the geometric numerator and match $\sqrt{C_{2,2}C_{4,4}}$ to the geometric denominator square root, so only algebraic cleanup remains for this edge.
proof idea
Unfold the geometric cosine, the CM cosine, and the CM denominator to expose both ratios explicitly. Change the goal to
$N_{\mathrm{geom}}(T,1)/\sqrt{D_{\mathrm{geom}}(T,1)} = C_{2,4}/\sqrt{C_{2,2}C_{4,4}}$.
Rewrite the numerator with the identity that $C_{2,4}$ equals four times the geometric numerator, and the denominator with the matching square-root diagonal-product identity. A final field_simp cancels the common factor of four and closes the equality. Term-mode proof; no case split beyond the fixed edge index.
why it matters
This is one of the six edge-specialized equalities that assemble Berger's cofactor formula for all tetrahedral edges (the parent theorem geometricDihedralCos_eq_cmCofactorRatio, which fin_cases on the edge and dispatches each case to a sibling). The module doc names that all-edge identification as the remaining target of the file: geometric face-normal cosine equals the Cayley-Menger cofactor ratio.
In the Recognition geometry stack, matching embedded Euclidean dihedral data to a distance-only Cayley-Menger presentation keeps tetrahedral structure available in pure metric form. That supports later geometric arguments tied to the forcing-chain landmark $D=3$ without retaining coordinate frames. The claim is fully proved; no hypothesis interface or sorry remains on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.