Geometry Schlaefli Tetrahedron Proof Has Deriv At Dihedral Closed Deriv Length

The derivative formula

A tetrahedron is the simplest solid with flat faces: four triangular sides meeting at four corners. Its volume depends on the lengths of its six edges. The classical formula of Cayley and Menger expresses that volume as a square root of a polynomial in the squared edge lengths. The question here is how the volume responds when one edge length is nudged, and the answer turns out to be expressible in a single closed-form derivative.

The declaration hasDerivAt_dihedralClosedDerivLength states that a specific formula, dihedralClosedDerivLength, is the derivative of the volume with respect to a single edge length. In plain terms: for any non-degenerate tetrahedron, if you change the length of one edge by a tiny amount, the volume changes by an amount equal to that formula. The formula itself is built from the squared edge lengths, the dihedral angles (the angles between faces), and the volume's square-root expression. It is a closed form, meaning it involves only algebraic operations and square roots, not an infinite series or an implicit equation.

This result is a recognition theorem: it is part of a machine-checked library of formal theorems, meaning the proof has been verified step by step by a computer. The theorem covers the derivative with respect to a squared-edge coordinate, and a companion result converts that to the derivative with respect to the actual edge length. The chain of reasoning connects the closed-form derivative to the classical Schläfli formula, which relates the change in volume to the sum of dihedral angle changes times edge lengths.

What the declaration does not claim is just as important. It does not claim that the formula is valid for degenerate tetrahedra, where the volume is zero and the square root in the denominator vanishes. It does not claim any global statement about all tetrahedra at once; it is a pointwise derivative at a specific tetrahedron with given edge lengths. And it does not itself prove the full Schläfli identity, only the derivative component that feeds into it.

/-- Convert a squared-edge derivative of a dihedral angle to an edge-length
derivative. -/
def dihedralClosedDerivLength (T : NonDegenerateTet) (e k : Fin 6) : ℝ :=
  2 * Real.sqrt (T.sqEdge k) * dihedralClosedDerivSq T e k

/-- Convert a squared-edge derivative of a dihedral angle to an edge-length
derivative. -/
def dihedralClosedDerivLength (T : NonDegenerateTet) (e k : Fin 6) : ℝ :=
  2 * Real.sqrt (T.sqEdge k) * dihedralClosedDerivSq T e k

What this page does not claim

The declaration does not cover degenerate tetrahedra where the volume is zero. The declaration does not prove the full Schläfli identity, only a derivative component. The declaration does not make a global statement about all tetrahedra at once.

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: