Pith. sign in
module module high

IndisputableMonolith.Geometry.SchlaefliN

show as:
view Lean formalization →

Dimension-parametric Schläfli data for an n-simplex: hinges (codimension-two faces) carry (n-2)-volume, dihedral angles, and edge lengths so the classical Schläfli identity can be stated without fixing n=3 or n=4. Gravity and discrete-geometry workers cite it when lifting tetrahedral Regge identities to 4-simplices. The module packages hinge and Schläfli records plus the angle-term cancellation identity used downstream.

claimFor an $n$-simplex, a hinge is a codimension-two face with measure equal to its $(n-2)$-volume. The module supplies abstract hinge data, assembled Schläfli data (hinge volumes, dihedral angles, edge lengths), the $n$-dimensional Schläfli identity relating $\sum V_{n-2}\,d\theta$ to edge variations, and the statement that the pure angle term vanishes under that identity.

background

Classical Schläfli says that for a simplex (or polyhedron) deforming in fixed ambient curvature, the weighted sum of dihedral-angle differentials against hinge volumes is determined by edge-length differentials; pure angle motion drops out. In Regge calculus that cancellation is what lets the action's first variation live on edges alone.

This module is the $n$-dimensional counterpart of the tetrahedron-level Schläfli packaging. A hinge is codimension two, so its measure is an $(n-2)$-volume rather than a length (3D) or area (4D). Upstream, CayleyMengerN supplies the dimension-parametric Cayley-Menger matrix and volume infrastructure for an arbitrary $n$-simplex, so edge data can be turned into volumes without expanding a fixed-size determinant by hand.

Sibling objects named in the module are hinge records, full Schläfli data bundles, the identity proposition itself, and the lemma that the identity kills the pure angle term.

proof idea

Definition-and-identity module rather than a long proof script. It introduces abstract hinge data (codimension-two measure), assembles Schläfli data for an $n$-simplex, states the Schläfli identity in that language, and records that the identity cancels the pure angle contribution. Concrete closed forms and pathwise kills for $n=4$ are deferred to the Regge analysis modules that import this file; those sit on top of Cayley-Menger volumes from the imported geometry layer.

why it matters in Recognition Science

Gate-A2 style elevation of the nonlinear Regge action to an edge Hessian needs a Schläfli kill of the angle sector. Downstream, Regge4DSchlaefliPathwise mirrors the 3D tetrahedron closed form at the 4-simplex level ($n_H = n_E = 10$) and proves flat-seed and directional Schläfli kills; Regge4DFlatSecondVariation then elevates the true 4D Regge action to a Schläfli-reduced edge Hessian, analogous to the 3D theorem chain. This module is the shared $n$-parametric hinge/Schläfli vocabulary those gravity analyses import, so 4D work does not hard-code tetrahedron-only types. In the broader Recognition geometry stack it is the bridge from Cayley-Menger volumes to discrete curvature identities used in Regge gravity analysis.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)