Geometry Schlaefli Tetrahedron Tetra Schlaefli Derivative Data

Tetrahedral derivative data

A tetrahedron is a pyramid with four triangular faces, six edges, and six dihedral angles, the angles between adjacent faces. In 1852, Ludwig Schläfli proved a remarkable identity: if you deform a tetrahedron smoothly, the sum over each edge of its length times the change in its opposite dihedral angle equals zero. This is the Schläfli identity, a local balance law that constrains how a tetrahedron's shape can change.

The declaration TetraSchlaefliDerivativeData packages this identity for a single nondegenerate tetrahedron. It records two pieces of data: the derivative of each dihedral angle with respect to each edge length, and an auxiliary volume derivative. The key requirement is that for any chosen edge, the sum of edge length times the corresponding dihedral derivative vanishes, exactly the Schläfli identity. This is a structure, not a proof: it states what data must satisfy, and provides a target for future theorems to fill in.

The declaration also connects to the volume formula. The squared volume of a tetrahedron equals its Cayley-Menger determinant divided by 288, and the square root of that quotient gives the volume. The library proves this identity and derives the volume's derivative along a path, assuming the Cayley-Menger derivative is known. These pieces support later Hessian computations in Regge calculus, where the Schläfli identity underpins the discrete Einstein equations.

In Recognition Science, this declaration is a stepping stone. The framework's machine-checked library of formal theorems uses it to pin down the local calculus needed for the Regge component theorem. The exact Euclidean statement, that the Schläfli sum vanishes, is recorded as a structure field, but the hard theorem, filling that structure from cofactor derivatives, remains a target. The declaration makes that target precise, not achieved.

What the declaration does not claim is equally important. It does not prove the Schläfli identity from first principles; it assumes it as a structural requirement. It does not assert that any concrete derivative functions exist for a given tetrahedron. It only defines the data package and the equation it must satisfy. The statement that such data always exists for every nondegenerate tetrahedron is a separate proposition, SchlaefliTetrahedronTheorem, and remains open.

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

/-- The local tetrahedral Schläfli derivative data at a nondegenerate
tetrahedron.  `dihedralDeriv e e'` means `∂θ_e/∂L_e'`; `volumeDeriv e'`
is retained as auxiliary volume derivative data for downstream Hessian
computations.  The Euclidean Schläfli identity itself is the vanishing of
`Σ_e L_e dθ_e`; it is not a volume-derivative formula. -/
structure TetraSchlaefliDerivativeData (T : NonDegenerateTet) where
  dihedralDeriv : Fin 6 → Fin 6 → ℝ
  volumeDeriv : Fin 6 → ℝ
  schlaefli :
    ∀ e' : Fin 6,
      (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralDeriv e e')
        = 0

/-- The local tetrahedral Schläfli derivative data at a nondegenerate
tetrahedron.  `dihedralDeriv e e'` means `∂θ_e/∂L_e'`; `volumeDeriv e'`
is retained as auxiliary volume derivative data for downstream Hessian
computations.  The Euclidean Schläfli identity itself is the vanishing of
`Σ_e L_e dθ_e`; it is not a volume-derivative formula. -/
structure TetraSchlaefliDerivativeData (T : NonDegenerateTet) where
  dihedralDeriv : Fin 6 → Fin 6 → ℝ
  volumeDeriv : Fin 6 → ℝ
  schlaefli :
    ∀ e' : Fin 6,
      (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralDeriv e e')
        = 0

What this page does not claim

The declaration does not prove the Schläfli identity; it assumes it as a structural field. The declaration does not assert the existence of derivative functions for any tetrahedron. The declaration does not establish the global Regge component theorem.

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: