Geometry Schlaefli Tetrahedron Proof Has Deriv At Volume3 Closed Deriv Length

The volume derivative

In solid geometry, the Schläfli formula relates how a tetrahedron's volume changes to how its six dihedral angles change. The theorem hasDerivAt_volume3ClosedDerivLength pins down one half of that relationship: it gives an exact, closed-form expression for the derivative of volume with respect to a single edge length. The formula is not an approximation; it is a precise algebraic statement, verified by a machine-checked library of formal theorems.

The statement concerns a non-degenerate tetrahedron, meaning one with positive volume, and one of its six edges, indexed by k. The theorem says that if you take the volume as a function of that edge's length, its derivative at the actual edge length equals a specific expression: 2 times the square root of the edge length, times a term built from the Cayley-Menger determinant and its gradient. In symbols, for edge length L, the derivative is 2√L · (cm3_grad / (576 · √(cm3/288))), where cm3 is the squared-volume determinant. This is the derivative with respect to length, not squared length; the theorem also proves the squared-length version separately.

The value of this result is that it converts a geometric rate of change into a finite algebraic recipe. Instead of measuring or approximating how volume responds to stretching an edge, you compute directly from the six edge lengths. The theorem is a component in a larger proof effort: the library uses it, together with analogous derivative statements for dihedral angles, to establish the full closed-form Schläfli identity for tetrahedra. That identity, in turn, is a stepping stone toward a geometric forcing result in the Recognition Science framework.

The theorem does not claim that the volume derivative is zero, nor that it has any particular sign. It does not assert the full Schläfli formula; it only provides the volume-side derivative. The closed-form identity that sums these derivatives over all six edges is a separate theorem, schlaefliTetrahedronTheorem, which the library proves by combining this derivative with the angle-side derivatives. The present declaration is a lemma, not the final identity.

/-- The closed-form edge-length derivative of volume is obtained from the
squared-edge derivative by `d(a_k)/dL_k = 2 L_k`. -/
theorem hasDerivAt_volume3ClosedDerivLength
    (T : NonDegenerateTet) (k : Fin 6) :
    HasDerivAt
      (fun L : ℝ => volume3SqEdges (Function.update T.sqEdge k (L ^ 2)))
      (volume3ClosedDerivLength T k) (Real.sqrt (T.sqEdge k)) := by
  unfold volume3ClosedDerivLength
  have hsq := hasDerivAt_sqEdgeCoordinate_from_edgeLength T k
  have hsqsqrt : Real.sqrt (T.sqEdge k) ^ 2 = T.sqEdge k :=
    Real.sq_sqrt (le_of_lt (T.sqEdge_pos k))
  have hvol : HasDerivAt
      (fun t : ℝ => volume3SqEdges (Function.update T.sqEdge k t))
      (volume3ClosedDerivSq T.sqEdge k)
      (Real.sqrt (T.sqEdge k) ^ 2) := by
    simpa [hsqsqrt] using hasDerivAt_volume3ClosedDerivSq T k
  have hcomp := HasDerivAt.comp_of_eq
    (x := Real.sqrt (T.sqEdge k)) hvol hsq rfl
  simpa [mul_comm, mul_left_comm, mul_assoc] using hcomp

/-- The closed-form edge-length derivative of volume is obtained from the
squared-edge derivative by `d(a_k)/dL_k = 2 L_k`. -/
theorem hasDerivAt_volume3ClosedDerivLength
    (T : NonDegenerateTet) (k : Fin 6) :
    HasDerivAt
      (fun L : ℝ => volume3SqEdges (Function.update T.sqEdge k (L ^ 2)))
      (volume3ClosedDerivLength T k) (Real.sqrt (T.sqEdge k)) := by
  unfold volume3ClosedDerivLength
  have hsq := hasDerivAt_sqEdgeCoordinate_from_edgeLength T k
  have hsqsqrt : Real.sqrt (T.sqEdge k) ^ 2 = T.sqEdge k :=
    Real.sq_sqrt (le_of_lt (T.sqEdge_pos k))
  have hvol : HasDerivAt
      (fun t : ℝ => volume3SqEdges (Function.update T.sqEdge k t))
      (volume3ClosedDerivSq T.sqEdge k)
      (Real.sqrt (T.sqEdge k) ^ 2) := by
    simpa [hsqsqrt] using hasDerivAt_volume3ClosedDerivSq T k
  have hcomp := HasDerivAt.comp_of_eq
    (x := Real.sqrt (T.sqEdge k)) hvol hsq rfl
  simpa [mul_comm, mul_left_comm, mul_assoc] using hcomp

/-- The local tetrahedral Schläfli derivative-data package is now constructed
from the explicit cofactor formulas. -/
theorem schlaefliTetrahedronTheorem :
    SchlaefliTetrahedronTheorem :=
  schlaefliTetrahedronTheorem_of_closedForm schlaefliTetrahedronClosedForm

What this page does not claim

The theorem does not state that the volume derivative is zero or has any particular sign. The theorem does not by itself prove the full Schläfli identity; that requires combining it with angle-side derivatives. The theorem does not apply to degenerate tetrahedra with zero volume.

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/SchlaefliTetrahedronProof.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: