Geometry Schlaefli N Schlaefli Data N

The n-simplex hinge record

In geometry, a simplex is the simplest shape in a given dimension: a point in zero dimensions, a line segment in one, a triangle in two, a tetrahedron in three. Each simplex has hinges, the lower-dimensional faces where two facets meet. For a tetrahedron, a hinge is an edge; for a triangle, a hinge is a vertex. The Schläfli identity is a classical relation connecting the volume of these hinges to how the dihedral angles change as edge lengths vary.

The declaration SchlaefliDataN defines a structure that packages this data for an n-dimensional simplex. It takes two natural numbers as parameters: nH, the number of hinges, and nE, the number of edge-length coordinates. The structure holds two fields. The first, hinge, assigns to each hinge a nonnegative real number, its measure, which is an (n-2)-volume. The second, dTheta_dL, is a matrix of real numbers giving the derivative of each hinge's dihedral angle with respect to each edge-length coordinate.

Alongside this data structure, the declaration defines a predicate, SchlaefliIdentityN, which states the n-dimensional Schläfli identity in a finite-index form. The identity asserts that for every edge coordinate e, the sum over all hinges h of the hinge measure times the angle derivative equals zero: Σ_h V_{n-2}(h) · ∂θ_h/∂L_e = 0. A theorem, schlaefliN_kills_angle_term, provides a direct eliminator: given a data record and a proof that it satisfies the identity, the theorem extracts the specific zero-sum equation for any chosen edge coordinate.

In Recognition Science, the framework's discrete ledger of recognition events, this structure serves as an interface. The declaration's documentation states that the 3D tetrahedral theorem can later be shown to instantiate this interface at n = 3. This means the structure is a general template, not a proof that any particular simplex satisfies the identity. It establishes what data must look like and what equation must hold, leaving the construction of actual instances for later work.

What this declaration does not claim is equally important. It does not prove that any specific geometric object satisfies the identity. It does not define what a hinge is geometrically, only that each hinge carries a nonnegative measure. It does not assert that the identity holds for all simplices, nor does it provide a way to compute hinge measures from coordinates. It establishes a formal interface, a contract that future theorems can use, not a theorem about the physical world.

/-- Schläfli derivative data in dimension `n`, over finitely many hinges and
edge-length coordinates. -/
structure SchlaefliDataN (nH nE : ℕ) where
  hinge : Fin nH → HingeDataN
  dTheta_dL : Fin nH → Fin nE → ℝ

/-- Schläfli derivative data in dimension `n`, over finitely many hinges and
edge-length coordinates. -/
structure SchlaefliDataN (nH nE : ℕ) where
  hinge : Fin nH → HingeDataN
  dTheta_dL : Fin nH → Fin nE → ℝ

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

No specific geometric object is proven to satisfy the identity. No definition of what a hinge is geometrically, only that each carries a nonnegative measure. No assertion that the identity holds for all simplices.

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: