Geometry Schlaefli N Schlaefli N Kills Angle Term

The n-dimensional Schläfli identity

The Schläfli identity is a classical result about how the volume of a polyhedron changes when you nudge its edges. In three dimensions, it says that the sum, over all edges, of the edge length times the change in the dihedral angle at that edge is zero. The theorem schlaefliN_kills_angle_term generalizes this to n dimensions: for any n-simplex, the sum over all hinges (codimension-two faces) of the hinge's (n−2)-volume times the derivative of its angle with respect to an edge length equals zero. That is the whole content: a finite-index restatement of the identity, ready for later use.

In the framework's machine-checked library, the identity is stated as an interface over abstract data: a list of hinges with nonnegative measures and a matrix of angle derivatives. The theorem simply unwraps that interface: if the data satisfies the identity, then for every edge coordinate, the weighted sum is zero. It is a direct eliminator, not a new derivation. The library later plans to show that the 3D tetrahedral case instantiates this interface at n = 3, but that instantiation is not part of this declaration.

What the theorem does not claim is just as important. It does not prove the Schläfli identity from scratch; it assumes it as a hypothesis. It does not say that any particular polyhedron satisfies the identity, only that if the data does, then the angle term vanishes. It does not connect to the framework's cost function, golden ratio, or dimensional forcing; this is a standalone geometric lemma, not a step in the recognition chain. And it does not establish the 3D case, which remains a separate theorem to be instantiated later.

The practical payoff is modularity. A machine-checked proof can now cite this one theorem whenever it needs the identity in any dimension, without re-deriving the sum. That is the kind of small, reusable building block that lets a larger formal theory grow without repeating itself.

/-- Direct eliminator for the n-dimensional identity. -/
theorem schlaefliN_kills_angle_term {nH nE : ℕ}
    (D : SchlaefliDataN nH nE) (hS : SchlaefliIdentityN D) (e : Fin nE) :
    ∑ h : Fin nH, (D.hinge h).measure * D.dTheta_dL h e = 0 :=
  hS e

/-- Direct eliminator for the n-dimensional identity. -/
theorem schlaefliN_kills_angle_term {nH nE : ℕ}
    (D : SchlaefliDataN nH nE) (hS : SchlaefliIdentityN D) (e : Fin nE) :
    ∑ h : Fin nH, (D.hinge h).measure * D.dTheta_dL h e = 0 :=
  hS e

What this page does not claim

The theorem does not prove the Schläfli identity from first principles; it assumes it. It does not show that any particular polyhedron satisfies the identity. It does not connect to the framework's cost function, golden ratio, or dimensional forcing.

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/SchlaefliN.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: