dihedralCos3_range_of_realization
plain-language theorem explainer
Any abstract nondegenerate tetrahedron realized by Euclidean points has cofactor dihedral cosines in $[-1,1]$. Cite when packaging those cosines into range-certified dihedral angle data. The proof unfolds the cofactor cosine, rewrites squared edges through the realization hypothesis, and applies the squared-edge range lemma on the realizing points.
Claim. Let $T$ be a nondegenerate abstract tetrahedron and $R$ a Euclidean four-point realization whose squared edge lengths equal those of $T$. Then for every edge index $e\in\{0,\ldots,5\}$, the cofactor dihedral cosine of $T$ at $e$ satisfies $-1\le\cos\theta_e(T)\le 1$.
background
This module develops the Euclidean geometric side of the tetrahedral dihedral cosine: face normals via cross products and the normalized inner product of adjacent face normals. The target is the Berger cofactor formula, which will identify that geometric cosine with the Cayley–Menger cofactor ratio from DihedralCayleyMenger.
The cofactor cosine on a nondegenerate abstract tetrahedron is defined from the six squared edge lengths. A realized tetrahedron supplies four Euclidean points whose pairwise squared distances match those edges. Dihedral angle data is a cosine value packaged with explicit bounds in $[-1,1]$, so any construction of that structure needs a range proof.
The immediate upstream fact is the range lemma for the squared-edge form of the cofactor cosine on a point realization: once edges come from Euclidean points, the cofactor expression already lies in $[-1,1]$.
proof idea
Short term-mode reduction. Unfold the cofactor cosine on the abstract nondegenerate tetrahedron (it is the squared-edge cofactor cosine of $T$'s edge data). Rewrite the squared-edge vector via the realization hypothesis so it matches the realizing points. Discharge the goal by the already-proved range lemma for the squared-edge cofactor cosine on a Euclidean realization, applied at the same edge index.
why it matters
This lemma is the range certificate that lets the module build dihedral angle data for a realized abstract tetrahedron without forcing callers to supply $-1\le\cos\le 1$ proofs. The sole downstream consumer packages the cofactor cosine together with the two bounds from this theorem into a DihedralAngleData record.
In the broader geometry stack, that record is the typed carrier for tetrahedral dihedral angles used when comparing the geometric (face-normal) cosine to the Cayley–Menger cofactor formula. Closing the Berger identification needs both sides to live in the same bounded cosine type; this result supplies the abstract/cofactor side whenever a Euclidean realization exists. It sits in the Regge/tetrahedral geometry layer that supports discrete curvature and forcing-chain geometry (eight-tick structure, $D=3$), not in the J-cost or mass-ladder core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.