Geometry Dihedral Derivatives

Dihedral angle derivatives

A dihedral angle is the angle between two planes, such as two triangular faces of a tetrahedron. In geometry, this angle is often computed from the lengths of the tetrahedron's six edges using the Cayley-Menger determinant, a formula that gives the volume of a simplex from its edge lengths. The cosine of the dihedral angle can be written as a ratio of cofactors of the Cayley-Menger matrix, a purely algebraic expression in the squared edge lengths.

This geometry dihedral derivatives library isolates the analytic part of differentiating that angle. The core result is the standard calculus rule: if θ = arccos(cos θ), then dθ = -(1 / sqrt(1 - cos²θ)) · d(cos θ). This is the chain rule applied to the arccosine function, and it holds whenever the cosine is not exactly 1 or -1, meaning the angle is not 0 or 180 degrees.

The library proves this derivative exists along any smooth path of squared edge lengths, provided the cosine derivative along that path is known. It packages this into a structure called DihedralAngleDerivativeAlong, which bundles the cosine derivative, the proof that the cosine stays away from the endpoints, and the resulting angle derivative. This packaged theorem is designed for downstream work with Regge calculus, a discrete approach to general relativity where spacetime is built from flat simplices.

For a realized tetrahedron, the library shows that the endpoint hypotheses for arccos are satisfied automatically when the cosine is not exactly ±1. It then provides a closed-form derivative value, dihedralAngle3SqClosedFormDeriv, which is the arccos chain-rule multiplier applied to the cofactor-ratio derivative. The final theorem, hasDerivAt_dihedralAngle3Sq_explicit, states that this closed-form value is indeed the derivative of the dihedral angle with respect to a single squared edge coordinate, under the same non-degeneracy conditions.

In plain language, this library establishes the exact formula for how a dihedral angle changes when you slightly stretch one edge of a tetrahedron, assuming the shape does not degenerate. It separates the clean calculus step from the heavier algebraic work of differentiating the cofactor expressions, which belongs to a separate cofactor derivative layer. This separation makes the calculus interface precise and reusable for any downstream geometric computation.

/-- Derivative of a dihedral angle along any one-parameter squared-edge path,
assuming the cofactor cosine derivative along that path is known and the
cosine stays away from the arccos endpoints at the base point. -/
theorem hasDerivAt_dihedralAngle3Sq_along
    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x cosDeriv : ℝ} (e : Fin 6)
    (hcos : HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e) cosDeriv x)
    (hm : dihedralCos3Sq (γ x) e ≠ -1)
    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) * cosDeriv) x := by
  exact hasDerivAt_arccos_comp hcos hm hp

/-- Closed-form coordinate derivative value for the tetrahedral dihedral
angle, as a function of squared edge coordinates. -/
def dihedralAngle3SqClosedFormDeriv
    (a : CayleyMengerPolynomial.SqEdges) (e : Fin 6) (k : Fin 6) : ℝ :=
  -(1 / Real.sqrt (1 - (dihedralCos3Sq a e) ^ 2)) *
    dihedralCos3SqClosedFormDeriv a e k

/-- Explicit coordinate derivative of the cofactor-defined tetrahedral
dihedral angle. -/
theorem hasDerivAt_dihedralAngle3Sq_explicit
    (a : CayleyMengerPolynomial.SqEdges) (e k : Fin 6)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       CayleyMengerMatrix.cmCofactor3 a p p *
         CayleyMengerMatrix.cmCofactor3 a q q) ≠ 0)
    (hden_ne : dihedralDenom3 a e ≠ 0)
    (hm : dihedralCos3Sq a e ≠ -1)
    (hp : dihedralCos3Sq a e ≠ 1) :
    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (Function.update a k t) e)
      (dihedralAngle3SqClosedFormDeriv a e k) (a k) := by
  have hbase :
      Function.update a k (a k) = a := by
    funext i
    by_cases hi : i = k <;> simp [Function.update, hi]
  have hm' : dihedralCos3Sq (Function.update a k (a k)) e ≠ -1 := by
    simpa [hbase] using hm
  have hp' : dihedralCos3Sq (Function.update a k (a k)) e ≠ 1 := by
    simpa [hbase] using hp
  simpa [dihedralAngle3SqClosedFormDeriv] using
    hasDerivAt_dihedralAngle3Sq_along e
      (hasDerivAt_dihedralCos3Sq_explicit a e k hprod_ne hden_ne)
      hm' hp'

What this page does not claim

This library does not compute the derivative of the cofactor cosine itself, which belongs to the cofactor derivative layer. This library does not prove the Cayley-Menger formula for the dihedral angle cosine. This library does not apply the derivative to any specific physical model or Regge calculus simulation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/DihedralDerivatives.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: