Geometry Schlaefli Tetrahedron Schlaefli Sum Of Tetra Data

The tetrahedral identity

A tetrahedron is the simplest three-dimensional solid: four triangular faces, six edges, and six dihedral angles where pairs of faces meet. In 1848, Ludwig Schläfli proved a remarkable relation for such a solid: if you deform it smoothly, the sum over all six edges of the edge length times the change in the opposite dihedral angle is exactly zero. This is the local Schläfli identity, a key part of Regge calculus, where spacetime is approximated by flat simplices.

The identity is not a statement about volume. It relates the geometry of the boundary (edge lengths) to the geometry of the angles between faces. For a one-parameter family of tetrahedra, the identity says that the changes in the six dihedral angles, weighted by the current edge lengths, cancel out perfectly. It holds for any smooth deformation, not just special ones, as long as the tetrahedron remains nondegenerate, meaning its volume does not collapse to zero.

In the Recognition Science framework, this classical fact appears as a formal theorem in the machine-checked library of formal theorems. The declaration schlaefli_sum_of_tetraData states that for any tetrahedron and any choice of derivative data satisfying the Schläfli condition, the sum over edges of the square root of the squared edge length times the dihedral derivative equals zero. In plainer terms: the library confirms that the weighted sum of dihedral angle changes vanishes, exactly as Schläfli proved.

The framework's contribution here is not a new physical law. It is a precise, machine-checked statement of a known geometric identity, expressed in the notation the framework uses for its Regge component theorem. The library also proves that the volume of a tetrahedron is the square root of a Cayley-Menger determinant divided by 288, and that the derivative of this volume along a path follows from the derivative of that determinant. These are the calculus pieces the framework needs for its larger geometric program.

What the declaration does not claim is just as important. It does not prove that the Schläfli identity follows from the cofactor derivatives of the dihedral angles; that harder theorem remains a stated target. It does not assert any statement about volumes changing, since the identity concerns angles, not volumes. And it does not say anything about the physical interpretation of Regge calculus or about how this identity connects to the framework's broader forcing chain. It is a local, geometric fact, cleanly stated and checked.

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

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

What this page does not claim

The declaration does not prove the Schläfli identity from the cofactor derivatives of the dihedral angles; that remains an open target. The declaration makes no statement about volume changes, since the identity concerns angles, not volumes. The declaration says nothing about the physical interpretation of Regge calculus or the framework's broader forcing chain.

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: