Geometry Schlaefli Deficit Eq

The deficit identity

In Regge calculus, a discrete approach to general relativity, space is built from flat simplices joined along hinges. At each hinge, the surrounding flat pieces fail to close flat by an amount called the deficit: the angular gap left when the dihedral angles of all simplices meeting there are added up. The classical definition is exactly deficit = 2π − (sum of dihedral angles). The Recognition Science declaration deficit_eq records this as a formal identity: for any hinge data structure, the deficit field is definitionally equal to that expression. It is a theorem whose proof is just unfolding definitions, tagged THEOREM in the framework's machine-checked library.

The identity matters because it is the hinge-level atom of the Regge action. The variation of that action with respect to an edge length splits into two sums: one involving how hinge areas change, and one involving how the deficits change. Schläfli's identity, a classical result from 1858, makes the second sum vanish identically, leaving only the area term. The framework's SchlaefliIdentity records this as a named hypothesis, not a proved theorem, because the full proof needs boundary-integration machinery that the ambient library does not yet provide. The declaration schlaefli_kills_dtheta then shows that, assuming that hypothesis, the troublesome sum is zero.

What deficit_eq does not claim is just as precise. It does not assert that any particular physical space has a given deficit; it only states the algebraic relationship that defines the term. It does not prove Schläfli's identity, which remains a hypothesis in the framework, explicitly threaded through downstream consumers. And it says nothing about the Regge equations themselves: the declaration totalDeficit_flat shows that if every hinge satisfies the flat-sum condition, the total deficit vanishes, but that is a separate, conditional statement. The power of the declaration is its modesty: it pins down the vocabulary so that every later theorem knows exactly what a deficit is.

theorem deficit_eq (h : SimplicialHingeData) :
    h.deficit = 2 * Real.pi - h.totalTheta := rfl

theorem deficit_eq (h : SimplicialHingeData) :
    h.deficit = 2 * Real.pi - h.totalTheta := rfl

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

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

What this page does not claim

This answer does not claim that deficit_eq proves Schläfli's identity; that remains a named hypothesis. This answer does not claim that any particular physical space has a nonzero or zero deficit. This answer does not claim that the Regge equations of motion are derived in the framework.

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: