dihedralAngle3
plain-language theorem explainer
Euclidean dihedral angle at a chosen edge of a nondegenerate tetrahedron, recovered as arccos of the Cayley-Menger cofactor cosine. Regge-calculus and causal-simplex workers cite it whenever they need the angle itself rather than only its cosine. The body is a one-line wrapper: Real.arccos of the already-defined cofactor cosine.
Claim. For a nondegenerate tetrahedron $T$ and edge index $e\in\{0,\ldots,5\}$, the dihedral angle at $e$ is $\theta_e(T):=\arccos(\cos\theta_e(T))$, where $\cos\theta_e(T)$ is the Cayley-Menger cofactor cosine of $T$ at edge $e$.
background
The module supplies an explicit Lean definition of tetrahedral dihedral cosines from Cayley-Menger cofactors, replacing a prose reference in the older dihedral-angle API. For edge $e=(i,j)$, let $(p,q)$ be the two opposite vertices. Vertex rows in the $5\times 5$ Cayley-Menger matrix are shifted by one, so vertex $v$ sits at CM index $v+1$. The classical formula is $\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$, with $C$ the cofactor matrix. The sign convention yields $\cos\theta=1/3$ on the regular tetrahedron, matching the standard internal dihedral.
Upstream, dihedralCos3 evaluates that cofactor cosine on a NonDegenerateTet (via squared edge lengths). The older DihedralAngleData structure packages a cosine in $[-1,1]$ and recovers the angle by arccos; the present definition is the bare real-valued angle before that packaging step.
proof idea
Pure definition, not a proof. Body applies Real.arccos to dihedralCos3 T e, the cofactor cosine already computed on the nondegenerate tetrahedron at edge $e$. No tactics, no lemmas, no range check at this layer.
why it matters
Gives the angle-valued face of the cofactor pipeline so downstream results can quote $\theta$ rather than only $\cos\theta$. In-module, the regular-unit theorems show that on the unit regular tetrahedron (under the cofactor check) this angle equals the existing regular-tetrahedron dihedral API value. In Gravity.SevenGaps.CausalSimplexWick it is the carrier for the physical-point theorems: every edge of the physical causal tetrahedron has Euclidean dihedral $\arccos(1/3)$, hence lies strictly in $(0,\pi)$, so deficit angles are real and well-defined. That closes a geometric prerequisite for Regge-style deficit bookkeeping on the causal simplex after Wick rotation, inside the broader RS geometry stack that feeds discrete gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.