Pith. sign in
module module high

IndisputableMonolith.Geometry.SchlaefliN

show as:
view Lean formalization →

Dimension-parametric Schläfli data for an n-simplex: hinges are codimension-two faces with (n-2)-volume measure, paired with dihedral angles so the classical Schläfli identity can be stated uniformly in n. Gravity analysts working the 4D Regge second-variation gates cite it. The module packages hinge/Schläfli records and the angle-term cancellation identity on top of the n-simplex Cayley-Menger infrastructure.

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, full Schläfli data (hinge measures and conjugate dihedral angles), the Schläfli identity in $n$ dimensions, and the statement that the pure angle variation term vanishes under that identity.

background

Classical Schläfli calculus relates the differential of simplex volume to a sum over hinges of (hinge measure) times (dihedral-angle differential). In Regge gravity the same identity kills pure-angle contributions to the action variation, leaving an edge-length Hessian. Here the setting is dimension-parametric: after the 3D tetrahedral closure, geometry is lifted to an arbitrary $n$-simplex.

Upstream, CayleyMengerN defines the full Cayley-Menger matrix for an $n$-simplex via Mathlib matrices and determinants rather than expanding a fixed-degree polynomial. That supplies the metric/volume backbone on which hinge measures live. A hinge is codimension two, so its measure is an $(n-2)$-volume; the module's opening doc states exactly that abstraction.

Sibling objects package the data: hinge records, full Schläfli records (measures plus angles), the identity itself, and the lemma that Schläfli cancels the bare angle term.

proof idea

This is primarily a definitions-and-identity module, not a long derivation. It introduces abstract hinge and Schläfli data structures for general $n$, states the Schläfli identity at that level of generality, and records the standard corollary that the pure angle-variation contribution is killed once the identity is imposed. Concrete volume and angle formulae are expected to come from the Cayley-Menger layer and from specialized 3D/4D closings downstream; the n-module keeps the bookkeeping uniform.

why it matters in Recognition Science

4D Regge analysis imports this module to elevate the nonlinear Regge action to a Schläfli-reduced edge Hessian. Downstream, Regge4DSchlaefliPathwise mirrors the 3D Gate-A2 input (tetrahedral six-edge closed form) at the 4-simplex level ($n_H = n_E = 10$), proving flat-seed Freudenthal closed form and flat directional Schläfli kill. Regge4DFlatSecondVariation then uses that pathwise kill so Gate A2 can treat the true 4D Regge second variation as a Schläfli-reduced edge Hessian, parallel to the 3D theorem chain.

Without a uniform n-dimensional hinge/Schläfli language, the 3D and 4D gates would each re-encode codimension-two measures ad hoc. This module is the shared geometric contract those gravity modules rely on.

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)