Geometry Schlaefli N

The n-dimensional hinge identity

The Schläfli identity is a classical result in geometry. It describes how the dihedral angles, the angles between two faces of a polyhedron, respond when an edge length changes. In three dimensions, the identity states that a weighted sum over the edges, with each term being the edge length times the rate of change of the opposite dihedral angle, equals zero. This is a conservation-like statement: the total angular response to a small deformation vanishes.

Ludwig Schläfli, a Swiss mathematician, discovered this relation in the 1850s while working on the geometry of higher-dimensional polytopes. The identity holds for any polyhedron, not just regular ones, and it generalizes naturally to n-dimensional simplices, the higher-dimensional analogues of triangles and tetrahedra. In n dimensions, the relevant objects are hinges, which are codimension-two faces, meaning they have dimension n minus two. For a tetrahedron in three dimensions, the hinges are its edges.

In Recognition Science, the framework models this identity in a finite-index form. The module defines a hinge by its measure, an (n-2)-dimensional volume, and records how each hinge angle changes with respect to each edge-length coordinate. The n-dimensional Schläfli identity then states that for every edge coordinate, the sum over all hinges of the hinge measure times the derivative of the angle with respect to that edge equals zero. The framework proves this identity in its machine-checked library of formal theorems, and the 3D tetrahedral theorem can later be shown to instantiate this interface at n equals three.

The practical consequence is a clean computational interface. Any future proof about tetrahedra can rely on this general n-dimensional statement rather than re-deriving the three-dimensional case from scratch. The identity also provides a structural constraint: it pins down how angular data must behave under deformation, which is a step toward understanding why the framework's recognition cycle settles on three spatial dimensions.

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

The module does not prove the Schläfli identity for arbitrary curved spaces; it states it for simplices with finitely many hinges. The identity alone does not force three spatial dimensions; it is one structural constraint among several in the framework.

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: