Geometry Schlaefli N Hinge Data N

Hinge data in n dimensions

In the geometry of simplices, the Schläfli identity relates how the dihedral angles of a simplex change when its edge lengths change. For a tetrahedron in three dimensions, the identity says that the sum over all six edges of the edge length times the derivative of the opposite dihedral angle vanishes. The declaration HingeDataN generalizes this to n dimensions: it defines the minimal data needed to state the identity for an n-simplex.

A hinge in an n-simplex is a face of codimension two, meaning it has dimension n-2. For a tetrahedron (n=3), a hinge is an edge (dimension 1). For a 4-simplex, a hinge is a triangular face (dimension 2). The structure HingeDataN packages a single hinge as a real number called measure, together with a proof that this measure is nonnegative. The measure is the (n-2)-volume of the hinge, the natural generalization of edge length in three dimensions.

The related structure SchlaefliDataN collects a finite list of hinges and a matrix of derivatives dTheta_dL, where each entry records how the dihedral angle at one hinge changes as one edge-length coordinate changes. The Schläfli identity itself is the statement that for every edge coordinate e, the sum over all hinges h of measure(h) times dTheta_dL(h,e) equals zero. The theorem schlaefliN_kills_angle_term simply extracts this identity for a particular edge coordinate; it is a direct eliminator, not a new result.

In Recognition Science, this declaration is an interface, not a proof. The docstring states that the 3D tetrahedral theorem can later be shown to instantiate this interface at n=3, but the pack contains no such instantiation. The declaration establishes the vocabulary and the shape of the identity in finite-index form, with finitely many hinges and edge coordinates. It does not prove that any particular geometric object satisfies the identity, nor does it derive the identity from first principles.

What the declaration gives a reader is a precise, machine-checked statement of what an n-dimensional Schläfli identity would assert, once the geometric meaning of measure and dTheta_dL is supplied. The nonnegativity condition on measure is the one property explicitly enforced. Everything else, including the existence of actual hinges in a real simplex and the proof that the identity holds for them, remains for later work.

/-- Abstract hinge data for an n-simplex: a hinge is codimension two, so
its measure is an `(n-2)`-volume. -/
structure HingeDataN where
  measure : ℝ
  measure_nonneg : 0 ≤ measure

/-- Abstract hinge data for an n-simplex: a hinge is codimension two, so
its measure is an `(n-2)`-volume. -/
structure HingeDataN where
  measure : ℝ
  measure_nonneg : 0 ≤ measure

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

HingeDataN does not prove that any particular simplex satisfies the Schläfli identity. The declaration does not derive the identity from geometric first principles. No instantiation at n=3 is provided in this module.

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: