Geometry Dihedral Derivatives Dihedral Angle Derivative Along

The derivative package

A dihedral angle is the angle between two faces of a polyhedron, measured along their shared edge. For a tetrahedron, the simplest three-dimensional solid, there are six such angles, one for each edge. In geometry and physics, knowing how these angles change when the tetrahedron is stretched or squeezed is essential: it appears in Regge calculus, a discrete approach to general relativity where spacetime is built from flat tetrahedral blocks and curvature lives at the edges. The classical problem is to compute the derivative of a dihedral angle with respect to a deformation of the edge lengths.

The framework's machine-checked library of formal theorems isolates the analytic part of that problem. It defines the dihedral angle as the arccosine of a cosine term derived from the Cayley-Menger determinant, the standard algebraic object that encodes the volume of a simplex from its edge lengths. The library then proves the chain rule for this composition: if the cosine term has a derivative, and the cosine stays strictly between -1 and 1, then the angle's derivative is the arccosine chain-rule multiplier, namely -1 divided by the square root of 1 minus the cosine squared, times the cosine derivative. This is the classical calculus fact, stated as a formal theorem.

The declaration DihedralAngleDerivativeAlong packages this into a single reusable object. It bundles four ingredients for a given one-parameter path of squared edge data: a real number that is the derivative of the cosine term along that path, a proof that this number is indeed the derivative, and two proofs that the cosine at the base point is not equal to -1 or 1. From this package, a theorem extracts the derivative of the dihedral angle itself along the same path. The purpose is to give downstream modules, such as those for Regge calculus, a clean interface: they supply the cosine derivative and the endpoint conditions, and the library supplies the angle derivative.

In Recognition Science, this result is a tool, not a discovery about the framework's core axioms. It does not involve the cost function, the golden ratio, or the forcing chain. It is a piece of standard differential geometry, formalized so that later work can build on it without re-deriving the chain rule. The declaration is a definitional structure, and the theorem it enables is a proved calculus fact; the framework's contribution is the formal packaging, not a new mathematical statement.

What the declaration does not claim is as important as what it proves. It does not compute the derivative of the cosine term itself; that harder algebraic work, involving cofactor minors of the Cayley-Menger matrix, belongs to a separate cofactor derivative layer. It also does not handle degenerate cases where the cosine reaches -1 or 1, which correspond to flat or flipped tetrahedra; those cases are explicitly excluded by the endpoint hypotheses. Finally, it does not assert that any particular path of edge lengths is physically realizable as a tetrahedron; that realizability is a separate geometric condition.

/-- Dihedral angle as a function of squared edge data. -/
def dihedralAngle3Sq (a : CayleyMengerPolynomial.SqEdges) (e : Fin 6) : ℝ :=
  Real.arccos (dihedralCos3Sq a e)

/-- Generic derivative of `arccos ∘ f`. -/
theorem hasDerivAt_arccos_comp
    {f : ℝ → ℝ} {f' x : ℝ}
    (hf : HasDerivAt f f' x)
    (hm : f x ≠ -1) (hp : f x ≠ 1) :
    HasDerivAt (fun t : ℝ => Real.arccos (f t))
      (-(1 / Real.sqrt (1 - (f x) ^ 2)) * f') x := by
  have hacos := Real.hasDerivAt_arccos hm hp
  simpa [mul_comm, mul_left_comm, mul_assoc] using hacos.comp x hf

/-- The local derivative package needed for a single dihedral angle. -/
structure DihedralAngleDerivativeAlong
    (γ : ℝ → CayleyMengerPolynomial.SqEdges) (e : Fin 6) (x : ℝ) where
  cosDeriv : ℝ
  cos_hasDerivAt :
    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e) cosDeriv x
  cos_ne_neg_one : dihedralCos3Sq (γ x) e ≠ -1
  cos_ne_one : dihedralCos3Sq (γ x) e ≠ 1

/-- The local derivative package needed for a single dihedral angle. -/
structure DihedralAngleDerivativeAlong
    (γ : ℝ → CayleyMengerPolynomial.SqEdges) (e : Fin 6) (x : ℝ) where
  cosDeriv : ℝ
  cos_hasDerivAt :
    HasDerivAt (fun t : ℝ => dihedralCos3Sq (γ t) e) cosDeriv x
  cos_ne_neg_one : dihedralCos3Sq (γ x) e ≠ -1
  cos_ne_one : dihedralCos3Sq (γ x) e ≠ 1

What this page does not claim

This answer does not claim the framework derives the dihedral angle formula from its core axioms. This answer does not claim the declaration handles degenerate flat or flipped tetrahedra. This answer does not claim any particular edge-length path is physically realizable as a tetrahedron.

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: