Geometry Dihedral Derivatives Arccos Endpoint Hypotheses Of Realized Ne Endpoint

Endpoint conditions for a dihedral angle

In geometry, the dihedral angle between two faces of a tetrahedron is the angle you measure when you slice the solid along an edge and look at the two triangular faces meeting there. Its cosine can be computed from the six squared edge lengths by a formula built from Cayley-Menger determinants, which encode the volume and metric data of the tetrahedron. The angle itself is the arccosine of that cosine, and the standard derivative formula for arccosine has a well-known singularity: the derivative blows up when the cosine approaches 1 or -1, which corresponds to the faces becoming coplanar, either folded flat or fully opened.

The declaration arccos_endpoint_hypotheses_of_realized_ne_endpoints is a theorem in the framework's machine-checked library of formal theorems. It states a simple but load-bearing fact: if you have a realized tetrahedron, meaning one with an actual set of points in space, and you know that the cosine of a particular dihedral angle is not equal to 1 and not equal to -1, then that cosine is indeed not at either endpoint. This is a tautology in the sense that the conclusion repeats the two hypotheses, but its role is to package those two conditions into the exact form that the arccosine derivative theorem requires. The theorem converts the geometric condition "the faces are not flat" into the analytic condition "the arccosine is differentiable at this point".

The theorem does not prove that any particular tetrahedron satisfies those endpoint conditions. It does not show that a given set of squared edge lengths comes from a realizable tetrahedron, nor does it compute the cosine value. It only says: given a realized tetrahedron and given the two non-endpoint assumptions, the derivative of the dihedral angle along any smooth path is well-defined. The actual derivative computation, which involves the cofactor derivatives of the Cayley-Menger matrix, is a separate layer of theorems in the same module. This declaration is the analytic interface that downstream modules, such as those dealing with Regge calculus, can rely on when they need to differentiate a dihedral angle with respect to edge lengths.

What this means in practice is that the framework has isolated the exact condition under which the geometry is smooth: the tetrahedron must not degenerate to a flat configuration at the edge in question. The theorem is a formal guarantee that if you avoid that degeneracy, the angle varies smoothly as you move the vertices. It does not tell you how to avoid the degeneracy, or what happens when you reach it; that remains a separate question about the geometry of the realization space.

/-- Endpoint hypotheses for a cofactor cosine coming from a realized
tetrahedron, provided the endpoint cases are excluded. -/
theorem arccos_endpoint_hypotheses_of_realized_ne_endpoints
    (T : TetrahedronRealization.RealizedTet) (e : Fin 6)
    (hneg : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1)
    (hpos : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1) :
    dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1 ∧
      dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1 :=
  ⟨hneg, hpos⟩

/-- Endpoint hypotheses for a cofactor cosine coming from a realized
tetrahedron, provided the endpoint cases are excluded. -/
theorem arccos_endpoint_hypotheses_of_realized_ne_endpoints
    (T : TetrahedronRealization.RealizedTet) (e : Fin 6)
    (hneg : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1)
    (hpos : dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1) :
    dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ -1 ∧
      dihedralCos3Sq (TetrahedronRealization.sqEdgeOfPoints T) e ≠ 1 :=
  ⟨hneg, hpos⟩

/-- 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

What this page does not claim

The theorem does not prove that any particular tetrahedron is realized or that its cosines avoid the endpoints. The theorem does not compute the derivative of the dihedral angle; it only provides the analytic interface for that computation. The theorem does not address what happens at the endpoints where the cosine equals 1 or -1.

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: