Geometry Schlaefli Total Deficit Flat

The flat baseline

In the geometry of piecewise-flat spaces, a hinge is the shared lower-dimensional face where two or more flat simplices meet. Around each hinge, the dihedral angles of the meeting simplices sum to some total. If that sum equals 2π, the hinge is locally flat: the surrounding space unfolds without curvature. The deficit at that hinge is 2π minus the sum, so a flat hinge has deficit zero.

The total deficit of a complex is the area-weighted sum of these deficits over all hinges. The theorem totalDeficit_flat proves the obvious-sounding but load-bearing fact: if every hinge satisfies the flat-sum condition, then the total deficit is zero. The proof is a direct computation: each deficit is zero by assumption, so the weighted sum collapses. This is a THEOREM in the machine-checked library of formal theorems, proved without sorry or new axioms.

The result matters because it is the baseline for Regge calculus, the discrete approximation to general relativity that replaces smooth spacetime with a piecewise-flat simplicial complex. In that setting, the total deficit functional plays the role of the Einstein-Hilbert action. A flat complex has zero action, which is exactly what a vacuum solution should have. The theorem does not claim that zero total deficit forces every hinge to be flat; that converse is false, since positive and negative deficits could cancel in the weighted sum.

The theorem also does not establish Schläfli's identity, the classical result that the weighted sum of area times angle-derivative vanishes under variation of edge lengths. That identity is recorded separately as a named hypothesis, because its proof requires boundary-integration machinery not yet in the library. The flat baseline theorem only handles the static case where all hinges are already flat; it says nothing about how the deficit changes when edges move.

What the theorem gives is a clean starting point: in the framework's library, the flat vacuum is a proved fact, not an assumption. That makes it a useful anchor for the larger program of showing that Regge equations reduce to Einstein's equations in the continuum limit, a program that still has open steps.

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

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

The converse: zero total deficit does not imply every hinge is flat. Schläfli's identity is not proved by this theorem; it is recorded as a named hypothesis. The theorem says nothing about how deficits change under variation of edge lengths.

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: