Geometry Schlaefli Deficit Derivative Matrix

The derivative matrix

In piecewise-flat geometry, a simplicial complex is built from flat simplices glued along hinges. The dihedral angle at a hinge is the angle between two adjacent simplex faces. When several simplices meet around a hinge, their dihedral angles sum to a total angle; the deficit, the amount by which this total falls short of 2π, measures curvature concentrated at that hinge. The Regge calculus, Tullio Regge's 1961 coordinate-free formulation of general relativity, discretizes spacetime this way and writes the gravitational action as a sum over hinges of area times deficit.

The declaration DeficitDerivativeMatrix packages the variational data: for each hinge and each edge, it records a real number intended to be the partial derivative of the total dihedral angle at that hinge with respect to that edge's length. The matrix itself is pure bookkeeping, a finite table of numbers indexed by hinges and edges. What gives it content is Schläfli's identity, a classical result from 1858 adapted to piecewise-flat complexes by Regge: for every edge, the area-weighted sum of these derivatives vanishes, Σ_h A_h · (∂θ_h/∂L_e) = 0.

That identity is what makes the Regge equations tractable. Varying the action with respect to an edge length produces two terms: one from changing hinge areas, one from changing deficit angles. Schläfli's identity kills the second term entirely, leaving only the area derivative. The framework's machine-checked library of formal theorems records this as a named hypothesis, not a proved theorem, because the full proof requires boundary-integration machinery not yet available in the underlying formal library. Zero sorry and zero new axioms are used; the identity is threaded explicitly through downstream consumers so callers can see exactly which classical fact is being invoked.

The declaration also establishes two clean consequences. If every hinge satisfies the flat-sum condition, the total deficit vanishes. And under Schläfli's identity, the troublesome Σ A · dθ/dL term in the Regge variation is identically zero. These are the results that Phase C3 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes relies on.

/-- A matrix of deficit-angle derivatives: `dThetadL h e` is intended
    to be `∂(totalTheta h) / ∂(len e)`. -/
structure DeficitDerivativeMatrix (nH nE : ℕ) where
  dThetadL : Fin nH → Fin nE → ℝ

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

Schläfli's identity is not proved in the framework; it is recorded as a named hypothesis because the proof requires boundary-integration machinery not yet in the formal library. The derivative matrix does not itself assert any geometric content; it is a bookkeeping structure whose meaning comes from the identity that constrains it. No claim is made that the Regge equations of motion are derived here; the framework only establishes the vanishing of one term in their variation.

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: