Geometry Schlaefli N Schlaefli Identity N

The n-dimensional identity

The Schläfli identity is a classical result in geometry that describes how the volume of a polyhedron or simplex changes when its dihedral angles are varied. In three dimensions, it states that the sum over all edges of the edge length times the rate of change of the dihedral angle at that edge is zero. This is a powerful constraint: it says that the volume derivative depends only on the boundary's angle changes, not on interior details.

The general form for n dimensions replaces edge lengths with (n-2)-dimensional hinge measures. A hinge is a codimension-two face, so in 3D a hinge is an edge, in 4D a hinge is a face, and so on. The identity then states that the sum over all hinges of the hinge measure times the derivative of the dihedral angle with respect to any edge-length coordinate equals zero. This is the statement formalized in the machine-checked library of formal theorems as SchlaefliIdentityN, a definition that takes abstract hinge data and angle-derivative data and asserts this vanishing sum for every edge coordinate.

The library also proves a direct eliminator theorem, schlaefliN_kills_angle_term, which simply unpacks the definition: if the identity holds, then for any chosen edge coordinate, the corresponding sum is zero. This is a trivial logical step, but it matters because it makes the identity usable in later proofs. The 3D tetrahedral case is intended to be shown as an instance of this n-dimensional interface at n = 3, though that instantiation is not yet in the library.

In Recognition Science, this declaration is part of a broader program that treats geometry as derived from recognition events. The framework models a discrete record of events, called a ledger, and derives constants and dimensions from forced cost functions. Within this account, the Schläfli identity is a candidate structural law that the framework expects to instantiate in its own geometric derivations. The n-dimensional statement here is the abstract interface, not yet a theorem about any particular simplex or any physical space.

What the declaration does not claim is important. It does not prove the Schläfli identity for any concrete geometric object; it only defines what the identity would mean for abstract hinge data. It does not assert that the identity holds in any specific dimension, nor does it connect this n-dimensional statement to the framework's derived three-dimensional space. Those connections remain open targets. The value of this declaration is architectural: it sets up a clean interface so that later work can instantiate and prove the identity where it applies.

/-- The n-dimensional Schläfli identity:
`Σ_h V_{n-2}(h) · ∂θ_h/∂L_e = 0` for every edge coordinate `e`. -/
def SchlaefliIdentityN {nH nE : ℕ} (D : SchlaefliDataN nH nE) : Prop :=
  ∀ e : Fin nE, ∑ h : Fin nH, (D.hinge h).measure * D.dTheta_dL h e = 0

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

This declaration does not prove the Schläfli identity for any specific simplex or polyhedron. This declaration does not assert the identity holds in any particular dimension n. This declaration does not connect the n-dimensional statement to the framework's derived three-dimensional space.

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: