IndisputableMonolith.Geometry.DihedralDerivatives
Defines the tetrahedral dihedral angle as a smooth function of squared edge lengths via Cayley-Menger cofactors, and supplies HasDerivAt lemmas for that map. Anyone proving a local Schläfli identity or a Regge Hessian cites these derivative interfaces. The module chains arccos composition with cofactor-ratio derivatives already exposed upstream.
claimFor a tetrahedron with squared edge data $s$, the dihedral angle opposite an edge is $\theta(s) = \arccos\!\big(C(s)\big)$, where $C$ is the normalized Cayley-Menger cofactor ratio. The module proves $\theta$ is differentiable (in the interior of the admissible domain) along edge variations, and records an explicit closed-form expression for $d\theta$ in terms of cofactor derivatives.
background
In discrete gravity and Regge calculus the local Schläfli identity relates volume variation to edge lengths times dihedral-angle variations. For a single Euclidean tetrahedron those angles are most cleanly written through Cayley-Menger determinants: the cosine of the dihedral angle on an edge is a ratio of cofactors of the bordered squared-distance matrix.
Upstream, DihedralCayleyMenger defines that cofactor cosine, DihedralCofactorFormula ties it to the geometric face-normal formula (Berger), and CofactorDerivatives exposes derivative hooks for the cofactors and the ratio. This module sits on top of that stack and treats the dihedral angle itself as $\arccos$ of the cofactor cosine, as a function of squared edge data.
The calculus setting is ordinary real one-variable differentiation along affine paths in edge-squared space (Mathlib HasDerivAt), with endpoint hypotheses that keep the cosine strictly inside $(-1,1)$ so $\arccos$ is smooth.
proof idea
Definition layer first: dihedralAngle3Sq is arccos of the Cayley-Menger dihedral cosine in squared-edge coordinates. Differentiability is obtained by composing Mathlib's derivative of arccos with the upstream cofactor-ratio derivative along a path (hasDerivAt_arccos_comp, hasDerivAt_dihedralAngle3Sq_along, hasDerivAt_dihedralAngle3Sq_from_cofactors).
Endpoint bookkeeping lemmas (arccos_endpoint_hypotheses_of_interior, ..._of_realized_ne_endpoints) discharge the open-interval hypotheses of arccos. A closed-form derivative object (dihedralAngle3SqClosedFormDeriv) packages the explicit formula, and hasDerivAt_dihedralAngle3Sq_explicit ties that formula back to HasDerivAt. No deep new algebra: the work is composition and hypothesis plumbing.
why it matters in Recognition Science
Local Schläfli for one tetrahedron needs $dV = \frac16 \sum \ell_e, d\theta_e$. The angle side of that identity is exactly the derivative interface built here. Downstream, SchlaefliTetrahedron and SchlaefliTetrahedronProof consume these lemmas to connect Cayley-Menger volume and dihedral derivatives into a closed-form tetrahedral Schläfli package; ReggeActionConcrete uses the same derivatives for the analytic Hessian of a finite 3D Regge action under a conformal ansatz; Regge4DSchlaefliPathwise mirrors the pattern at the 4-simplex (Freudenthal) level.
In the broader Recognition geometry stack this is the bridge from static cofactor formulas to variational discrete gravity, without leaving the squared-edge coordinate chart.
scope and limits
- Does not prove the Berger identification of cofactor cosine with face-normal cosine; that lives upstream.
- Does not prove the tetrahedral Schläfli identity itself; only supplies $d\theta$ inputs.
- Does not treat Lorentzian or non-Euclidean signature tetrahedra.
- Does not establish global smoothness up to the boundary of the Cayley-Menger cone.
- Does not compute second derivatives or the full Regge Hessian.
used by (4)
depends on (3)
declarations in this module (10)
-
def
dihedralAngle3Sq -
theorem
hasDerivAt_arccos_comp -
theorem
hasDerivAt_dihedralAngle3Sq_along -
structure
DihedralAngleDerivativeAlong -
theorem
arccos_endpoint_hypotheses_of_interior -
theorem
arccos_endpoint_hypotheses_of_realized_ne_endpoints -
theorem
hasDerivAt_dihedralAngle3Sq_from_cofactors -
def
dihedralAngle3SqClosedFormDeriv -
theorem
dihedralAngle3SqClosedFormDeriv_def -
theorem
hasDerivAt_dihedralAngle3Sq_explicit