dihedralCos3_interior_of_realization_ne_endpoints
plain-language theorem explainer
For a nondegenerate tetrahedron realized by four points in Euclidean 3-space with matching squared edges, any cofactor dihedral cosine that is not exactly ±1 lies strictly in (−1,1). Regge-calculus and Cayley–Menger workers cite this to rule out flat dihedral collapse once endpoints are excluded. Proof is a one-line transfer: unfold the cofactor cosine and apply the squared-edge interior lemma.
Claim. Let $T$ be a nondegenerate tetrahedron (positive squared edge lengths and positive Cayley–Menger 3-volume) and let $R$ be four affinely independent points in $\mathbb{R}^3$ whose pairwise squared distances equal those of $T$. For any edge index $e\in\{0,\ldots,5\}$, if the cofactor dihedral cosine of $T$ at $e$ is neither $-1$ nor $1$, then $-1 < \cos\theta_e(T) < 1$.
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals via cross products of edge vectors, then the normalized inner product of the two normals adjacent to a chosen edge. The stated target is the Berger cofactor formula, equating that geometric cosine with the Cayley–Menger cofactor ratio from DihedralCayleyMenger.
A nondegenerate tetrahedron carries six positive squared edge lengths and a strictly positive Cayley–Menger determinant. A realized tetrahedron is four points in $\mathbb{R}^3$ that are affinely independent; its squared edge map records the six pairwise squared distances. The cofactor cosine on a nondegenerate tet is defined by feeding those squared edges into the Cayley–Menger cofactor ratio.
The immediate upstream result states that cofactor dihedral cosines of realized tetrahedra are strictly interior once the endpoint values $\pm 1$ are excluded. The present theorem lifts that statement from the squared-edge realization to an abstract nondegenerate tet that admits such a realization.
proof idea
One-line wrapper. Unfold the cofactor cosine (it is the squared-edge cofactor cosine of the tet's edge data). Rewrite the endpoint hypotheses and the goal along the assumption that the realization's squared edges equal those of the abstract tet. Apply the upstream interior lemma for realized squared edges, which already yields the strict double inequality $-1 < \cdot < 1$.
why it matters
Strict interior range for dihedral cosines is the geometric content needed before identifying cofactor and face-normal formulas: values in $(-1,1)$ correspond to genuine angles, while $\pm 1$ are the flat endpoint collapses. The module doc names the Berger cofactor formula as the remaining identification between this geometric cosine and the Cayley–Menger ratio; the present lemma clears the range side of that bridge for any abstract nondegenerate tet that is realized in $\mathbb{R}^3$.
In the broader Recognition geometry stack this sits under the Regge-rigorous foundation and the tetrahedron-realization layer, both of which feed discrete curvature and eight-tick spatial constructions consistent with the forced $D=3$ landmark. No downstream consumers are wired yet; the natural parents are the Berger identification and any later strict-angle or positive-volume corollaries that need interior cosines on realized tets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.