Geometry Schlaefli Tetrahedron Tetra Schlaefli Derivative Data Of Equation

The local Schläfli identity

In Euclidean geometry, a tetrahedron is a solid with four triangular faces, six edges, and six dihedral angles, the angles between adjacent faces. The Schläfli identity is a classical relation: for a smooth one-parameter deformation of the tetrahedron, the sum over the six edges of the edge length times the change in the opposite dihedral angle equals zero. Written with differentials, Σ_e L_e dθ_e = 0. It is a local statement, meaning it holds instant by instant along any continuous path that keeps the tetrahedron nondegenerate, and it is the foundation for the Regge calculus of discrete gravity, where spacetime is approximated by flat simplices glued together.

The identity was discovered by Ludwig Schläfli in the mid-nineteenth century. Its power is that it links metric data, the edge lengths, to angular data, the dihedral angles, without requiring the full metric tensor. For a single tetrahedron the relation is exact, not approximate. The same identity generalizes to higher-dimensional simplices, where it becomes Σ_e V_e dθ_e = 0 with volume elements in place of lengths, but the three-dimensional case is the one used in Regge's discretization of general relativity.

In Recognition Science, the machine-checked library of formal theorems pins down this local identity in the notation used by its Regge component theorem. It defines a structure called the tetrahedral Schläfli derivative data, which packages three pieces: the derivative of each dihedral angle with respect to each squared edge length, the derivative of the volume with respect to each squared edge length, and a proof that the Schläfli sum vanishes for every choice of the varying edge. The declaration tetraSchlaefliDerivativeData_of_equation is the assembly step: it takes any concrete functions for those derivatives, together with a proof that they satisfy the Schläfli equation, and builds the full package. It also proves the volume-squared relation V² = cm3 / 288, where cm3 is the Cayley-Menger determinant of the squared edge data, and derives the derivative of the volume along a path from the derivative of that determinant.

The declaration does not prove that such derivative functions exist. That is the remaining hard theorem, stated precisely in the library as the claim that for every nondegenerate tetrahedron, the derivative data package is nonempty. The current file only constructs the package from a supplied equation proof. It also does not derive the dihedral derivatives from the cofactor formulas; that derivation is the target the file makes explicit. The volume derivative is retained as auxiliary data for downstream Hessian computations, but the Schläfli identity itself is a statement about edge lengths and dihedral angles, not a volume-derivative formula.

What this means for a reader is that the local geometry of a tetrahedron, the exact relation that makes Regge calculus work, is now available as a verified building block. The next step, filling the package from the cofactor derivatives, is a precise open target rather than a vague hope. The identity itself is classical and exact; the framework's contribution is to record it in a form that downstream proofs can use without re-deriving it.

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

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

The declaration does not prove that derivative functions satisfying the Schläfli equation exist for every tetrahedron. It does not derive the dihedral derivatives from the cofactor formulas. It does not establish the Schläfli identity for curved or 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: