Geometry Schlaefli Tetrahedron Has Deriv At Volume3 Of Has Deriv At Cm3

The volume derivative

A tetrahedron is a solid with four triangular faces, six edges, and four vertices. Its volume can be computed from the six edge lengths alone, without any angles, through a formula named after Arthur Cayley and Karl Menger. The formula is not a simple product; it involves a square root of a polynomial in the squared edge lengths. In the framework's notation, if cm3 stands for that polynomial, the volume is V = sqrt(cm3 / 288).

The declaration hasDerivAt_volume3_of_hasDerivAt_cm3 proves a calculus fact about that formula. Suppose the squared edge data change smoothly along a one-parameter path, and suppose the derivative of cm3 along that path is known at a point. Then the derivative of the volume along the same path is forced: it equals the derivative of cm3 divided by 576 times sqrt(cm3 / 288). The proof requires the volume to be positive at that point, which means the tetrahedron is not degenerate. This is a standard application of the chain rule and the derivative of the square root function, carried out in a machine-checked library of formal theorems.

In Recognition Science, this derivative rule is a stepping stone, not a destination. The framework's goal in this part of its geometry library is the Schläfli identity, a classical statement about how a tetrahedron's volume responds when its dihedral angles change. The identity says that the sum over the six edges of edge length times the change in the opposite dihedral angle equals zero. That identity is a statement about angles, not directly about volume. The derivative rule here only connects changes in squared edge data to changes in volume; it does not by itself say anything about angles.

The framework has stated the exact Schläfli identity as a target: for every nondegenerate tetrahedron, there exist derivative functions for the dihedral angles such that the Schläfli sum vanishes. Proving that target from the cofactor derivative formulas remains open. The volume derivative rule is one of the calculus pieces the framework has secured on the way to that target, but the full identity is not yet proved.

What this means for a reader is simple: the framework has a precise, machine-checked rule for how tetrahedral volume changes when edge data change, and it has a clearly stated, still unproved goal for the angle-based Schläfli identity. The volume rule is a tool, not the theorem itself.

/-- Generic derivative of `sqrt (f / 288)` along a real parameter. -/
theorem hasDerivAt_volume3_of_hasDerivAt_cm3
    {f : ℝ → ℝ} {f' x : ℝ}
    (hf : HasDerivAt f f' x)
    (hpos : 0 < f x / 288) :
    HasDerivAt (fun t : ℝ => Real.sqrt (f t / 288))
      (f' / (576 * Real.sqrt (f x / 288))) x := by
  have hdiv : HasDerivAt (fun t : ℝ => f t / 288) (f' / 288) x := by
    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
      hf.const_mul ((288 : ℝ)⁻¹)
  have hsqrt := Real.hasDerivAt_sqrt (ne_of_gt hpos)
  have hcomp := hsqrt.comp x hdiv
  convert hcomp using 1
  field_simp [hpos.ne']
  ring

/-- Generic derivative of `sqrt (f / 288)` along a real parameter. -/
theorem hasDerivAt_volume3_of_hasDerivAt_cm3
    {f : ℝ → ℝ} {f' x : ℝ}
    (hf : HasDerivAt f f' x)
    (hpos : 0 < f x / 288) :
    HasDerivAt (fun t : ℝ => Real.sqrt (f t / 288))
      (f' / (576 * Real.sqrt (f x / 288))) x := by
  have hdiv : HasDerivAt (fun t : ℝ => f t / 288) (f' / 288) x := by
    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
      hf.const_mul ((288 : ℝ)⁻¹)
  have hsqrt := Real.hasDerivAt_sqrt (ne_of_gt hpos)
  have hcomp := hsqrt.comp x hdiv
  convert hcomp using 1
  field_simp [hpos.ne']
  ring

/-- Generic derivative of `sqrt (f / 288)` along a real parameter. -/
theorem hasDerivAt_volume3_of_hasDerivAt_cm3
    {f : ℝ → ℝ} {f' x : ℝ}
    (hf : HasDerivAt f f' x)
    (hpos : 0 < f x / 288) :
    HasDerivAt (fun t : ℝ => Real.sqrt (f t / 288))
      (f' / (576 * Real.sqrt (f x / 288))) x := by
  have hdiv : HasDerivAt (fun t : ℝ => f t / 288) (f' / 288) x := by
    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
      hf.const_mul ((288 : ℝ)⁻¹)
  have hsqrt := Real.hasDerivAt_sqrt (ne_of_gt hpos)
  have hcomp := hsqrt.comp x hdiv
  convert hcomp using 1
  field_simp [hpos.ne']
  ring

/-- The local data gives the Schläfli sum for its own derivative matrices. -/
theorem schlaefli_sum_of_tetraData
    {T : NonDegenerateTet} (D : TetraSchlaefliDerivativeData T) (e' : Fin 6) :
    (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * D.dihedralDeriv e e')
      = 0 :=
  D.schlaefli e'

What this page does not claim

This answer does not claim that the full Schläfli identity has been proved in the framework. This answer does not claim that the volume derivative rule by itself describes how dihedral angles change. This answer does not claim that the Cayley-Menger formula is valid for degenerate tetrahedra.

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: