cmCofactor3_edge0_sqrt_diag_product
plain-language theorem explainer
For a realized tetrahedron, the square root of the product of Cayley–Menger diagonal cofactors C_{3,3} and C_{4,4} equals four times the square root of the geometric dihedral denominator at edge 0. Anyone proving Berger’s cofactor identification of dihedral cosines cites this scaling step. The proof rewrites via the already-proved product identity, then extracts √16 = 4.
Claim. Let $T$ be a realized tetrahedron in Euclidean space, with squared edge lengths forming the Cayley–Menger data. Then $\sqrt{C_{3,3}\,C_{4,4}} = 4\sqrt{D_0}$, where $C_{r,c}$ are the signed Cayley–Menger cofactors of that data and $D_0$ is the product of the squared Euclidean norms of the two face normals adjacent to edge $0$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products of edge vectors, and the normalized inner product of the two normals meeting at a chosen edge. The target is Berger’s cofactor formula, equating that geometric cosine to a ratio of Cayley–Menger cofactors.
A realized tetrahedron supplies four points in $\mathbb{R}^3$; squared pairwise distances feed the $5\times 5$ Cayley–Menger matrix. The cofactor $C_{r,c}$ is the signed complementary minor. For edge $0$, the geometric denominator square $D_0$ is $(|n_1|^2)(|n_2|^2)$, with $n_1,n_2$ the outward face normals on the two faces sharing that edge.
The immediate upstream fact is that the product of the two diagonal cofactors already equals $16,D_0$. The present statement is the remaining square-root scaling of that identity.
proof idea
One short tactic chain. Rewrite the product inside the square root by the upstream identity $C_{3,3}C_{4,4}=16,D_0$. Factor $\sqrt{16\cdot D_0}=\sqrt{16}\sqrt{D_0}$ (nonnegativity of $16$ is trivial). Then $\sqrt{16}=\sqrt{4^2}=4$ by the standard square-root-of-square lemma, yielding $4\sqrt{D_0}$.
why it matters
This is the last positivity/scaling fact needed before Berger’s formula for edge $0$. Downstream, geometricDihedralCos_edge0_eq_cmCofactorRatio applies it and records that Berger’s cofactor formula is fully proved for that edge: the geometric dihedral cosine equals the Cayley–Menger cofactor ratio built from squared edge lengths.
In the Recognition geometry stack, dihedral angles of realized tetrahedra sit under the multi-distinction and Freudenthal-strip scaffolding that feeds discrete curvature and dimensional forcing. Closing the edge-$0$ case is the template for the remaining five edges in the same module. It does not itself invoke the T0–T8 forcing chain, but it supplies the Euclidean identification those geometric layers rely on when angles are expressed purely in distance data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.