geometricDihedralCos_range
plain-language theorem explainer
For any realized tetrahedron and any of its six edges, the geometric dihedral cosine (normalized inner product of the two adjacent face normals) lies in the closed interval [-1,1]. Anyone equating geometric dihedrals with Cayley–Menger cofactor ratios cites this bound. The proof unfolds the cosine definition and applies the elementary estimate that a normalized absolute inner product is at most one.
Claim. Let $T$ be a realized tetrahedron in Euclidean space and let $e$ be any of its six edges. Write $\cos\theta_e(T)$ for the geometric dihedral cosine along $e$, i.e. the normalized inner product of the outward (or consistently oriented) normals of the two faces meeting at $e$. Then $-1 \le \cos\theta_e(T) \le 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 long-term target is the Berger cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four affinely independent points in $\mathbb{R}^3$. For each of the six edges one forms the two face normals (cross products of the edge vectors spanning each face) and defines the geometric dihedral cosine as numerator over square-root of the product of the two normal self-dots. The auxiliary lemma that $|\langle u,v\rangle|/\sqrt{|u|^2|v|^2}\le 1$ is the only analytic input.
The surrounding Recognition geometry stack uses this bound so that cofactor-defined dihedral cosines inherit a legitimate cosine range before any identification with ledger or $\varphi$-ladder structure.
proof idea
Term-mode proof. Unfold the definitions of the geometric dihedral cosine, its numerator (inner product of the two face normals), and its squared denominator (product of the two normal self-dots). After dsimp, the claim is exactly the statement that the absolute value of a normalized inner product is at most one, which is discharged by abs_le.mp applied to the local lemma abs_dot_div_sqrt_self_mul_self_le_one. No tetrahedron-specific geometry beyond the definition is used.
why it matters
The range bound is the first sanity check on the geometric dihedral cosine before it is identified with the Cayley–Menger cofactor ratio (the Berger formula still pending in this module). Downstream, dihedralCos3Sq_sqEdgeOfPoints_range rewrites the cofactor cosine via that equality and quotes this theorem to conclude that cofactor-defined dihedrals of realized tetrahedra also lie in $[-1,1]$. The companion geometricDihedralCos_interior_of_ne_endpoints starts from the same closed range and upgrades it to a strict interior bound once the endpoint values $\pm 1$ are excluded.
In the broader Recognition geometry program this keeps dihedral data inside the domain of inverse cosine and of subsequent curvature or deficit identities. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the $\varphi$-ladder; it is pure Euclidean linear algebra supporting those later identifications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.