Geometry Schlaefli Simplicial Edge Data

Edge data and its limits

In the geometry of curved space, physicists often approximate a smooth surface by a patchwork of flat triangles, tetrahedra, or higher-dimensional simplexes. This is the Regge calculus, introduced by Tullio Regge in 1961 as a way to do general relativity without coordinates. The framework's machine-checked library of formal theorems formalizes the bookkeeping for such a patchwork. The declaration SimplicialEdgeData is a structure that records the edge lengths of a simplicial complex with finitely many edges, indexed by a finite set, together with the requirement that every edge length is positive. It is a definitional choice, a way to say what data a geometric configuration carries, not a theorem about that data.

The companion structure SimplicialHingeData records, for each hinge (the shared face where two simplexes meet), its area and the list of dihedral angles of the top-dimensional simplexes meeting it. The total angle around a hinge is the sum of those dihedral angles, and the deficit is 2π minus that total. In flat space the total is exactly 2π and the deficit is zero; a nonzero deficit signals curvature concentrated along the hinge. A theorem in the library, totalDeficit_flat, proves that if every hinge satisfies the flat-sum condition, the total deficit vanishes. That is a genuine formal result, but it is a check on the definitions, not a claim about physical space.

The central object, Schläfli's identity, is a classical result from 1858 by Ludwig Schläfli, adapted by Regge to piecewise-flat complexes. It states that for every edge, the sum over hinges of the hinge area times the derivative of the total dihedral angle with respect to that edge length vanishes. This identity is what makes the Regge equations of motion simplify from two terms to one. The library does not prove this identity. Its docstring says explicitly that the full proof requires boundary-integration machinery not yet available in the ambient mathematics library. Instead, the framework records Schläfli's identity as a named hypothesis, a structure called SchlaefliIdentity, which downstream consumers thread through explicitly so callers can see exactly which classical fact is being assumed. A theorem, schlaefli_kills_dtheta, then shows that under that hypothesis the troublesome term in the Regge variation is identically zero.

What this means in plain terms: the library has rigorously packaged the data of a discrete geometry and proved the consequences that follow from assuming Schläfli's identity, but it has not established the identity itself. The identity remains an assumption, clearly labeled, pending future work on the geometric calculus needed for its proof. The practical payoff is that any later result built on this foundation can be audited: a reader knows precisely which classical fact is being taken on faith and which parts are machine-checked.

/-- Abstract edge-length data for a simplicial complex with finitely many
    edges indexed by `Fin nE`. -/
structure SimplicialEdgeData (nE : ℕ) where
  len : Fin nE → ℝ
  len_pos : ∀ e, 0 < len 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

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

What this page does not claim

The library does not prove Schläfli's identity; it assumes it as a named hypothesis. The definitions do not establish that any particular physical space is curved or flat. The flat-sum theorem does not imply that real simplicial complexes have zero total deficit.

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: