DihedralStructure
plain-language theorem explainer
Packages a dihedral-angle assignment on non-degenerate tetrahedra: six real angles in $[0,\pi]$, one per edge, plus a named smoothness placeholder. Anyone citing the conditional Regge component theorem needs this interface. It is a pure structure declaration; the classical Cayley–Menger cosine formula is deferred.
Claim. A dihedral structure is a triple $(\theta, R, S)$ where $\theta$ assigns to each non-degenerate tetrahedron $T$ and each of its six edges $e$ a real number $\theta(T,e)\in[0,\pi]$, the range condition $R$ asserts $0\le\theta(T,e)\le\pi$ for all $T,e$, and $S$ is a named proposition standing in for smoothness of $\theta$ in the squared-edge coordinates (classically from the Cayley–Menger cofactor formula).
background
The module builds the analytic substrate for a genuine 3D Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$. It already supplies the Cayley–Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths, its gradient, and a polynomial Taylor identity, together with named classical hypotheses (Schläfli, dihedral cosine via cofactors, smoothness on the realisability cone).
A non-degenerate tetrahedron is a six-tuple of positive squared edge lengths with $\mathrm{CM}_3>0$ (positive volume). Edges are indexed by $\mathrm{Fin},6$. Dihedral angles are the internal angles between faces meeting at each edge; classically they are recovered from Cayley–Menger cofactors (Berger §9.7) and enter Schläfli's identity, which relates volume derivatives to face areas and dihedral angles.
This structure is the interface that packages those angles before an explicit cosine formula is formalized. The smoothness field is intentionally a bare Prop placeholder, matching the module's honest treatment of external classical input.
proof idea
No proof body: this is a structure declaration (def_or_abbrev style). The three fields are the data (angle map), a universal range axiom in $[0,\pi]$, and a named smoothness hypothesis left as an uninterpreted proposition for later discharge by the Cayley–Menger cofactor formula.
why it matters
The Regge component theorem under the conformal edge ansatz needs dihedral angles as smooth functions of edge data so that the Hessian off-diagonals can be identified with minus face areas. This structure is the named external interface for that datum, parallel to the Schläfli identity hypothesis in the same module.
It sits in the geometry layer that supports discrete gravity / Regge calculus inside Recognition Science, not in the T0–T8 forcing chain itself. Downstream use is not yet wired (used_by empty); the doc-comment states the intended replacement is the explicit Cayley–Menger cosine formula. Until that expansion, any conditional component theorem must assume an instance of this structure rather than derive angles from $\mathrm{CM}_3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.