cmCofactor3_edge2_sqrt_diag_product
plain-language theorem explainer
For any realized tetrahedron, the square root of the product of Cayley–Menger diagonal cofactors C_{2,2} and C_{3,3} equals four times the square root of the geometric dihedral denominator square at edge 2. Anyone matching face-normal dihedral cosines to CM cofactor ratios cites this identity. The proof rewrites via the unsquared product lemma, then extracts √16 = 4.
Claim. Let $T$ be a tetrahedron realized by four affinely independent points in Euclidean $3$-space, and let $a$ be its squared-edge data. Then $\sqrt{C_{2,2}(a)\,C_{3,3}(a)} = 4\sqrt{D_2(T)}$, where $C_{r,c}$ denotes the Cayley–Menger cofactor and $D_2(T)$ is the product of the squared Euclidean norms of the two face normals adjacent to edge $2$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products, and the normalized inner product of the two normals on faces sharing a chosen edge. The target is Berger’s cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A RealizedTet is four points in $\mathbb{R}^3$ with affine independence. Squared edge lengths feed the $5\times5$ Cayley–Menger matrix; cmCofactor3 is the signed minor cofactor $C_{r,c}$. The geometric denominator square at edge $e$ is $(|n_1|^2)(|n_2|^2)$ for the two adjacent face normals built from the shared edge and the two opposite vertices.
The immediate upstream fact is that the unsquared product $C_{2,2}C_{3,3}$ already equals $16$ times that geometric denominator square (each diagonal cofactor equals $-4$ times a normal squared norm).
proof idea
One short tactic chain. First rewrite the product inside the square root by cmCofactor3_edge2_diag_product_eq_sixteen_denomSq, obtaining $\sqrt{16\cdot D_2(T)}$. Split with Real.sqrt_mul (nonnegativity of $16$ by norm_num). Identify $\sqrt{16}=4$ by writing $16=4^2$ and applying Real.sqrt_sq. The remaining factor is exactly $4\sqrt{D_2(T)}$.
why it matters
This is the square-root bookkeeping step that lets the geometric dihedral cosine (numerator over $\sqrt{D_e}$) match the CM ratio form used in dihedralCos3Sq. The sole downstream consumer is geometricDihedralCos_edge2_eq_cmCofactorRatio, which unfolds both cosines and substitutes this identity (together with the matching numerator identity) to finish Berger’s formula on edge $2$.
In the broader Recognition geometry stack, equating face-normal dihedrals to pure edge-length cofactors is the bridge from realized $3$-space tetrahedra to combinatorial CM data. That bridge supports later rigidity and packing arguments on the Freudenthal strip and the eight-tick discrete geometry (T7/T8 landmarks), without needing coordinate normals downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.