Geometry Schlaefli Schlaefli Kills Dtheta

Schläfli's identity

Schläfli's identity is a classical result in geometry, published by Ludwig Schläfli in 1858. It concerns polyhedra and their higher-dimensional analogues. The identity states that if you take a polyhedron and vary one edge length slightly, the sum over all hinges of the hinge area times the change in the total dihedral angle at that hinge is zero. In symbols, for every edge e, ∑ A_h · (∂θ_h / ∂L_e) = 0, where A_h is the area of hinge h and θ_h is the total dihedral angle at that hinge. The name 'hinge' refers to the (n−2)-dimensional face where two top-dimensional simplices meet in a simplicial complex.

The identity became important in 1961 when Tullio Regge used it in his formulation of general relativity without coordinates, now called Regge calculus. In that discrete setting, spacetime is approximated by a patchwork of flat simplices, and curvature is concentrated along hinges as a deficit angle. Regge's equations of motion come from varying the total action with respect to edge lengths. The variation produces two terms: one involving the change in area, and one involving the change in the deficit angle. Schläfli's identity makes the second term vanish identically, so the equations reduce to a single term. This simplification is what the declaration schlaefli_kills_dtheta records.

In the framework's machine-checked library of formal theorems, the declaration is a theorem that states: if the Schläfli identity holds for a given set of hinges and a given matrix of angle derivatives, then the weighted sum ∑ A_h · (∂θ_h / ∂L_e) equals zero for every edge e. The proof is one line: it simply unfolds the hypothesis. The substantive mathematical content is not proved from first principles in the library. The full proof of Schläfli's identity requires integration by parts on simplex boundaries, machinery that the library's ambient geometry calculus does not yet provide. The framework therefore records the identity as a named hypothesis, matching how other classical facts are imported, and threads it explicitly through downstream consumers so callers can see which classical fact is being used.

The declaration itself is a formal consequence: it shows that assuming Schläfli's identity makes the angle-derivative term vanish. It does not prove Schläfli's identity from more basic geometry. It does not establish that the identity holds for any particular simplicial complex, nor does it connect the identity to the framework's cost function, recognition cycles, or the forcing chain. The declaration is a bookkeeping step in a larger program to discharge the Regge deficit linearization hypothesis. Its value is that it makes the dependence on a classical unproved-in-library fact explicit, so that any downstream theorem built on it carries the hypothesis visibly.

What the declaration changes for a reader is the ability to see exactly where a classical geometric fact enters a formal argument. The identity is not trivial, and the framework does not pretend to derive it. By recording it as a named hypothesis, the library keeps the logical ledger honest: every use of the identity is visible, and the classical fact is never silently assumed. The flat baseline case is also recorded: if every hinge satisfies the flat-sum condition, the total deficit vanishes, which is proved in the library as totalDeficit_flat.

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

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

What this page does not claim

The declaration does not prove Schläfli's identity from more basic geometry. It does not establish that the identity holds for any particular physical simplicial complex. It does not connect the identity to the framework's cost function, recognition cycles, or the forcing chain.

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: