Geometry Regge Rigorous Foundation Schlaefli3 Didentity

Schläfli's identity as a formal hypothesis

Schläfli's identity is a classical result in 3D Euclidean geometry. For any tetrahedron, it says that a certain weighted sum of changes in its dihedral angles vanishes. The weights are the lengths of the edges opposite those angles. In the Regge calculus, a discrete approach to general relativity, this identity is a standard tool. It was stated by Ludwig Schläfli in 1858 and used by Tullio Regge in his 1961 paper on coordinate-free general relativity.

In the Recognition Science framework, the declaration Schlaefli3DIdentity records this classical law as a named external hypothesis. It does not prove the identity. The formal statement says that for every non-degenerate tetrahedron, and for every edge e', the sum over all edges e of the edge length L_e times the partial derivative of the dihedral angle at e with respect to L_e' equals zero. This is a precise, machine-readable version of the classical identity, but it is an assumption, not a result derived within the framework.

The declaration is part of a larger body of work that builds a rigorous foundation for the Regge component theorem, which states that a certain matrix entry M_ij equals minus the area of the face f_ij. This body of work proves several things about the Cayley-Menger polynomial, which encodes the volume of a tetrahedron in terms of its edge lengths. It shows that this polynomial is smooth and gives an explicit formula for its gradient. These are genuine theorems. But the Schläfli identity itself is imported from the standard literature, exactly as the framework imports the Cheeger-Müller-Schrader convergence result from spectral geometry.

The reason for this import is practical. A full formal proof of Schläfli's identity would require a substantial Riemannian geometry library, including cross products, parallel transport, and integration over dual cones. That machinery does not yet exist in the framework's machine-checked library of formal theorems. So the identity is recorded as a named hypothesis, with its classical reference cited, and the work proceeds to show what can be proved assuming it. This is honest formal-math practice: it separates what is proved from what is assumed, and it makes the remaining gap explicit.

What the declaration establishes, then, is a precise statement of a classical identity, ready to be used in further formal work. What it does not establish is the identity itself. The distinction matters. A reader who sees the declaration might think the framework has proved Schläfli's identity. It has not. It has stated it as a hypothesis, with a clear reference to the classical proof. The path to a full formal proof of the Regge component theorem still requires proving this identity, along with the dihedral cosine formula and the smoothness of dihedral angles on the realisability cone. These are named as the substantive open items in the work's own summary.

/-- Schläfli identity (3D, Euclidean tetrahedral form), stated as a named
external classical hypothesis.  See module-doc references. -/
def Schlaefli3DIdentity : Prop :=
  ∀ (T : NonDegenerateTet) (dihedralDeriv : Fin 6 → Fin 6 → ℝ)
    (_volumeDeriv : Fin 6 → ℝ),
    -- `dihedralDeriv e e'` represents `∂θ_e^{(T)} / ∂L_{e'}` at `T`.
    -- `_volumeDeriv e` represents `∂V / ∂L_e` at `T` and is auxiliary;
    -- Euclidean Schläfli itself is the vanishing of the angle term.
    -- Schläfli says: for every edge e', the sum of L_e · ∂θ_e/∂L_{e'} over e
    -- vanishes.
    (∀ e' : Fin 6,
      (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralDeriv e e')
        = 0)

/-- Schläfli identity (3D, Euclidean tetrahedral form), stated as a named
external classical hypothesis.  See module-doc references. -/
def Schlaefli3DIdentity : Prop :=
  ∀ (T : NonDegenerateTet) (dihedralDeriv : Fin 6 → Fin 6 → ℝ)
    (_volumeDeriv : Fin 6 → ℝ),
    -- `dihedralDeriv e e'` represents `∂θ_e^{(T)} / ∂L_{e'}` at `T`.
    -- `_volumeDeriv e` represents `∂V / ∂L_e` at `T` and is auxiliary;
    -- Euclidean Schläfli itself is the vanishing of the angle term.
    -- Schläfli says: for every edge e', the sum of L_e · ∂θ_e/∂L_{e'} over e
    -- vanishes.
    (∀ e' : Fin 6,
      (∑ e : Fin 6, Real.sqrt (T.sqEdge e) * dihedralDeriv e e')
        = 0)

theorem reggeRigorousFoundationCert : ReggeRigorousFoundationCert where
  cm3_polynomial_explicit := fun a => by unfold cm3; ring
  cm3_smooth := cm3_contDiff
  cm3_regular := cm3_regular_unit
  cm3_rightAngle := cm3_rightAngle_unit
  cm3_taylor_identity := cm3_taylor
  cm3_update_form := cm3_update_polyform
  conformal_smooth := conformalSqEdge_contDiff
  cm3_conformal_smooth := cm3_conformal_contDiff

theorem reggeRigorousFoundationCert : ReggeRigorousFoundationCert where
  cm3_polynomial_explicit := fun a => by unfold cm3; ring
  cm3_smooth := cm3_contDiff
  cm3_regular := cm3_regular_unit
  cm3_rightAngle := cm3_rightAngle_unit
  cm3_taylor_identity := cm3_taylor
  cm3_update_form := cm3_update_polyform
  conformal_smooth := conformalSqEdge_contDiff
  cm3_conformal_smooth := cm3_conformal_contDiff

What this page does not claim

The declaration does not prove Schläfli's identity; it states it as a hypothesis. The body of work does not prove the full Regge component theorem M_ij = -area(f_ij). The framework does not derive the identity from its own axioms; it imports it from classical geometry literature.

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/ReggeRigorousFoundation.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: