Geometry Schlaefli Tetrahedron Has Deriv At Volume3 Along

The derivative rule

A tetrahedron is a pyramid with a triangular base, the simplest three-dimensional solid. Its volume is determined entirely by the six edge lengths. The theorem hasDerivAt_volume3_along states, in the framework's formal library, that if you know how those six lengths change as a single parameter moves, you can compute how the volume changes at that same instant. The formula is precise: the volume's rate of change equals the rate of change of a certain squared-edge expression, divided by 576 times the square root of that expression divided by 288. The condition is that the expression stays positive, meaning the tetrahedron does not collapse to a flat shape at the moment in question.

This is a calculus result, not a geometric discovery. It is a derived rule that follows from the chain rule applied to the volume formula V = sqrt(cm3 / 288), where cm3 is the Cayley-Menger determinant, a polynomial in the squared edge lengths that vanishes exactly when the six lengths cannot form a nondegenerate tetrahedron. The theorem does not prove that this determinant has any particular derivative; it assumes that derivative as a hypothesis and then produces the volume derivative as a consequence. The proof is a direct application of the square-root differentiation rule, checked by the machine.

In the framework's account, this theorem is one step toward a larger target: the Euclidean Schläfli identity, which says that a certain sum of edge lengths times dihedral angle changes equals zero. That identity is a statement about angles, not volumes. The volume derivative here is auxiliary data, kept for later Hessian computations. The theorem itself does not establish the Schläfli identity, nor does it say anything about angles. It is a lemma, cleanly isolated, that a later proof will use.

What the theorem gives a reader is a reliable tool: whenever a path through tetrahedra is given and the Cayley-Menger derivative is known, the volume derivative follows without further work. What it does not give is the Schläfli identity itself, which remains a separate, unproved target in this file. The distinction matters because the framework's claims are only as strong as their proofs, and this proof stops at the derivative rule.

/-- Derivative of tetrahedral volume along a squared-edge path, assuming
the derivative of `cm3` along the path. -/
theorem hasDerivAt_volume3_along
    {γ : ℝ → SqEdges} {x cmDeriv : ℝ}
    (hcm : HasDerivAt (fun t : ℝ => cm3 (γ t)) cmDeriv x)
    (hpos : 0 < cm3 (γ x) / 288) :
    HasDerivAt (fun t : ℝ => volume3SqEdges (γ t))
      (cmDeriv / (576 * Real.sqrt (cm3 (γ x) / 288))) x :=
  hasDerivAt_volume3_of_hasDerivAt_cm3 hcm hpos

/-- Derivative of tetrahedral volume along a squared-edge path, assuming
the derivative of `cm3` along the path. -/
theorem hasDerivAt_volume3_along
    {γ : ℝ → SqEdges} {x cmDeriv : ℝ}
    (hcm : HasDerivAt (fun t : ℝ => cm3 (γ t)) cmDeriv x)
    (hpos : 0 < cm3 (γ x) / 288) :
    HasDerivAt (fun t : ℝ => volume3SqEdges (γ t))
      (cmDeriv / (576 * Real.sqrt (cm3 (γ x) / 288))) x :=
  hasDerivAt_volume3_of_hasDerivAt_cm3 hcm hpos

/-- Tetrahedral volume as a function of squared edge data:
`V = sqrt (CM_3 / 288)`. -/
def volume3SqEdges (a : SqEdges) : ℝ :=
  Real.sqrt (cm3 a / 288)

What this page does not claim

The theorem does not prove the Euclidean Schläfli identity, which remains a separate target. The theorem says nothing about dihedral angles or their derivatives. The theorem does not establish that any particular path has a derivative; it only converts a known Cayley-Menger derivative into a volume derivative.

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