Geometry Schlaefli

Schläfli's identity

Schläfli's identity is a classical result in geometry, first stated by Ludwig Schläfli in 1858. It concerns piecewise-flat shapes, which are built by gluing flat triangles, tetrahedra, or their higher-dimensional analogues along their faces. The identity says that if you take such a shape and slightly change the length of one edge, a certain weighted sum of the changes in the angles at the hinges, the lower-dimensional faces where pieces meet, always equals zero. The weights are the areas of those hinges. In symbols, for each edge e, the sum over hinges h of A_h times the partial derivative of the total dihedral angle θ_h with respect to the edge length L_e is zero.

The identity is not obvious. In the literature it is proved by integrating by parts on the boundary of each simplex, a technique that requires substantial geometric calculus. Tullio Regge used it in 1961 when he formulated general relativity without coordinates, replacing smooth spacetime with a piecewise-flat approximation. The identity is what makes the Regge equations of motion simplify: a variation of the action with respect to an edge length normally produces two terms, one from the change in area and one from the change in angle. Schläfli's identity kills the second term, leaving only the area term. This is a standard and important tool in discrete gravity.

The Recognition Science framework's library, a machine-checked collection of formal theorems, records this identity as a named hypothesis. The reason is practical: the full proof requires boundary-integration machinery that the library's ambient mathematics does not yet provide. So the module defines the relevant data structures, such as edge lengths, hinge areas, and dihedral angles, and states the identity as a formal proposition. It then proves two consequences that follow from that hypothesis. First, if every hinge is flat, meaning the angles around it sum to 2π, then the total deficit, the area-weighted sum of the deviations from flatness, is zero. Second, the identity indeed makes the angle-variation term vanish. The certificate structure packages these results, and the library checks them with zero unproved assumptions and zero new axioms.

What this establishes in plain language is a clean bookkeeping of a classical fact. The module does not prove Schläfli's identity; it names it as a hypothesis and shows what downstream reasoning depends on it. This matters because it lets future work in the framework, such as checking how Regge calculus converges to general relativity, state explicitly which classical result is being used. The reader can see exactly what is assumed and what follows from that assumption.

/-- **SCHLÄFLI'S IDENTITY** (piecewise-flat form).

    For a finite collection of hinges (indexed by `Fin nH`) with areas
    `A_h` and a matrix `dThetadL` of dihedral-angle derivatives with
    respect to edge lengths, the weighted sum vanishes:

    `∀ e, Σ_h A_h · (∂θ_h / ∂L_e) = 0`.

    This is the classical local identity; see Regge (1961, eq. 2.8) and
    Brewin (2000). We record it as a hypothesis structure because the
    full proof requires boundary-integration machinery not yet in
    Mathlib. -/
def SchlaefliIdentity {nH nE : ℕ}
    (hinges : Fin nH → SimplicialHingeData)
    (M : DeficitDerivativeMatrix nH nE) : Prop :=
  ∀ e : Fin nE,
    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0

/-- If every hinge satisfies the flat-sum condition, the total deficit
    vanishes. -/
theorem totalDeficit_flat {nH : ℕ}
    (hinges : Fin nH → SimplicialHingeData)
    (hFlat : ∀ h : Fin nH,
      DihedralAngle.FlatSumCondition (hinges h).dihedrals) :
    totalDeficit hinges = 0 := by
  unfold totalDeficit
  apply Finset.sum_eq_zero
  intro h _
  have : (hinges h).deficit = 0 := by
    unfold SimplicialHingeData.deficit
    exact DihedralAngle.deficit_eq_zero_of_flat _ (hFlat h)
  rw [this]; ring

/-- Under Schläfli, the `Σ A · dθ/dL` term in the Regge variation is
    identically zero. -/
theorem schlaefli_kills_dtheta {nH nE : ℕ}
    (hinges : Fin nH → SimplicialHingeData)
    (M : DeficitDerivativeMatrix nH nE)
    (hS : SchlaefliIdentity hinges M) (e : Fin nE) :
    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0 := hS e

/-- If every hinge satisfies the flat-sum condition, the total deficit
    vanishes. -/
theorem totalDeficit_flat {nH : ℕ}
    (hinges : Fin nH → SimplicialHingeData)
    (hFlat : ∀ h : Fin nH,
      DihedralAngle.FlatSumCondition (hinges h).dihedrals) :
    totalDeficit hinges = 0 := by
  unfold totalDeficit
  apply Finset.sum_eq_zero
  intro h _
  have : (hinges h).deficit = 0 := by
    unfold SimplicialHingeData.deficit
    exact DihedralAngle.deficit_eq_zero_of_flat _ (hFlat h)
  rw [this]; ring

/-- Under Schläfli, the `Σ A · dθ/dL` term in the Regge variation is
    identically zero. -/
theorem schlaefli_kills_dtheta {nH nE : ℕ}
    (hinges : Fin nH → SimplicialHingeData)
    (M : DeficitDerivativeMatrix nH nE)
    (hS : SchlaefliIdentity hinges M) (e : Fin nE) :
    (∑ h : Fin nH, (hinges h).area * M.dThetadL h e) = 0 := hS e

theorem schlaefliCert : SchlaefliCert where
  flat_total_zero := fun hinges hFlat => totalDeficit_flat hinges hFlat
  schlaefli_kills_sum := fun hinges M hS e => schlaefli_kills_dtheta hinges M hS e

What this page does not claim

This module does not prove Schläfli's identity; it records it as a named hypothesis. This module does not establish any connection between Schläfli's identity and the recognition cost function J(x). This module does not provide a proof that Regge calculus converges to general relativity.

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