dihedralAngleData3_of_realization
plain-language theorem explainer
Packages cofactor dihedral-angle data for a nondegenerate abstract tetrahedron once a Euclidean point realization of its squared edges is given. Callers no longer supply the cosine range bounds by hand. Anyone wiring realized tets into the DihedralAngleData API would cite this. The body is a two-line wrapper: obtain the range from the realization theorem, then hand both bounds to the cofactor packaging constructor.
Claim. Let $T$ be a nondegenerate abstract tetrahedron, $R$ a Euclidean four-point realization with the same squared edge lengths as $T$, and $e\in\{0,\ldots,5\}$ an edge index. Return the dihedral-angle data whose cosine equals the Cayley–Menger cofactor cosine of $T$ at $e$, with the interval bounds $-1\le\cos\le 1$ filled automatically from the realization.
background
This module develops the Euclidean geometric side of tetrahedral dihedral cosines: face normals via cross products and the normalized inner product of adjacent face normals. The target identification is the Berger cofactor formula, equating that geometric cosine with the Cayley–Menger cofactor ratio from DihedralCayleyMenger.
DihedralAngleData is the shared API object: a real cosine together with proofs that it lies in $[-1,1]$, from which the angle is recovered by arccos. The cofactor packaging constructor dihedralAngleData3 builds that object from the abstract cofactor cosine dihedralCos3, but it demands the two range inequalities as explicit hypotheses.
A realized tetrahedron is a four-point configuration in Euclidean space whose pairwise squared distances match the abstract edge data of $T$. The upstream theorem dihedralCos3_range_of_realization states that any such realization forces the cofactor cosine into $[-1,1]$.
proof idea
One-line style wrapper. First invoke dihedralCos3_range_of_realization on $(T,R,hR,e)$ to obtain the conjunction $-1\le\mathrm{dihedralCos3}(T,e)\le 1$. Project the two conjuncts and pass them, with $T$ and $e$, to dihedralAngleData3, which simply records the cofactor cosine and the supplied bounds into a DihedralAngleData structure. No new arithmetic is performed.
why it matters
Removes a recurring proof obligation when moving from abstract edge data to the shared dihedral API: once a Euclidean realization is known, the cofactor cosine is automatically a legitimate angle cosine. That sits on the geometric side of the Berger cofactor program in this module, whose remaining goal is to identify the cross-product normal cosine with the Cayley–Menger cofactor ratio.
No downstream consumers are wired yet (used_by is empty), so the definition is infrastructure for later Regge or discrete-geometry arguments that need packaged dihedrals rather than bare cofactors. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure Euclidean tetrahedron geometry supporting those layers when curvature or deficit angles appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.