Geometry Schlaefli Tetrahedron

The tetrahedral identity

The Schläfli identity is a classical fact about tetrahedra, the simplest three-dimensional shapes with flat triangular faces. In plain terms, it says that as a tetrahedron deforms smoothly, the weighted sum of how each edge length changes times how its opposite dihedral angle changes is always zero. Dihedral angles are the angles between two faces meeting along an edge. The identity is local: it holds for a single tetrahedron, not only for a whole triangulated surface.

For a tetrahedron with six edges, label each edge length L_e and the opposite dihedral angle θ_e. The identity states that Σ_e L_e dθ_e = 0 along any smooth one-parameter deformation. This is a differential relation, not a formula for volume. It was discovered by Ludwig Schläfli in the mid-1800s while studying the geometry of higher-dimensional polytopes, and it became a key element for later work in geometric analysis and general relativity.

In Recognition Science, the framework's machine-checked library of formal theorems takes up this classical identity. The module SchlaefliTetrahedron establishes the local calculus pieces needed for a larger program: it defines the tetrahedral volume as V = sqrt(CM_3 / 288), where CM_3 is a Cayley-Menger determinant of squared edge data, and proves the squared-volume identity V² = CM_3 / 288. It also proves the derivative of that volume along a one-parameter path of squared edges, assuming the derivative of CM_3 is known. The derivative formula is explicit: if f(t) is the CM_3 value along the path, then d/dt sqrt(f/288) = f' / (576 * sqrt(f/288)).

The module then states the exact local Schläfli identity as a structure: for every nondegenerate tetrahedron, there exists a matrix of dihedral derivatives such that the weighted sum Σ_e L_e dθ_e vanishes for each of the six edge directions. This is captured in the proposition SchlaefliTetrahedronTheorem, which asserts that every nondegenerate tetrahedron admits such derivative data. The module also provides a bridge: if one can prove the explicit Schläfli equation for concrete derivative functions, that proof automatically constructs the required structure package. The remaining hard step, filling this structure from cofactor dihedral derivative formulas, is left as a precise target for future work.

What this establishes in plain language is a clean, machine-checked foundation for the Schläfli identity in the framework's notation. It does not yet prove the full identity from first principles; it sets up the exact statement and the calculus tools needed to reach it. The payoff is that downstream work on Regge calculus, the discrete version of general relativity that uses tetrahedral angles and edge lengths, can build on a verified local identity rather than an assumed one.

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

/-- The squared-volume identity, by definition of `volume3SqEdges`. -/
theorem volume3SqEdges_sq (a : SqEdges) (hcm : 0 ≤ cm3 a / 288) :
    volume3SqEdges a ^ 2 = cm3 a / 288 := by
  unfold volume3SqEdges
  exact Real.sq_sqrt hcm

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

/-- The exact local statement we need to prove from the cofactor derivative
formulas. -/
def SchlaefliTetrahedronTheorem : Prop :=
  ∀ T : NonDegenerateTet, Nonempty (TetraSchlaefliDerivativeData T)

/-- If the explicit Schläfli equation has been proved for concrete
derivative functions, it constructs the local derivative-data package. -/
def tetraSchlaefliDerivativeData_of_equation
    (T : NonDegenerateTet)
    (dTheta_dL : Fin 6 → Fin 6 → ℝ) (dVolume_dL : Fin 6 → ℝ)
    (hS : TetraSchlaefliEquation T dTheta_dL dVolume_dL) :
    TetraSchlaefliDerivativeData T where
  dihedralDeriv := dTheta_dL
  volumeDeriv := dVolume_dL
  schlaefli := hS

What this page does not claim

The full Schläfli identity is not yet proved from first principles in this module. This module does not establish any connection between the Schläfli identity and the framework's cost function or forcing chain. The classical history of Schläfli's work is general knowledge, not a claim from the framework's library.

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: