Pith. sign in
module module high

IndisputableMonolith.Geometry.SchlaefliTriangulation3D

show as:
view Lean formalization →

Packages local Schläfli derivative data on every tetrahedron of a finite 3D Regge triangulation and lifts the single-simplex identity to a global left- and right-hand side. Anyone proving first variation or Hessian statements for the nonlinear Regge action cites this scaffold. The main theorem is the global identity obtained by summing local Schläfli contributions over the triangulation.

claimOn a finite 3D Regge triangulation $T$, assign to each tetrahedron $\tau$ its local Schläfli derivative data. Define the global left-hand side $\mathrm{LHS}(T)$ and right-hand side $\mathrm{RHS}(T)$ by summing the local contributions. Then $\mathrm{LHS}(T)=\mathrm{RHS}(T)$ whenever every tetrahedron satisfies the local Schläfli identity.

background

Regge calculus replaces smooth 3-geometry by a piecewise-flat triangulation whose curvature is concentrated on hinges (edges in 3D). The classical Schläfli identity relates the differential of tetrahedron volume to edge lengths and dihedral angles; it is the geometric engine behind stationarity of the Regge action.

The upstream module on a single tetrahedron fixes the local calculus: volume-squared $V^2=\mathrm{cm}_3/288$ and the local Schläfli form used by the Regge component theorem. The finite triangulation scaffold supplies incidence data so those local identities can be summed over an arbitrary closed or bounded complex.

This module sits between those two layers. It records, for every tetrahedron of a finite triangulation, the local Schläfli derivative payload and defines the global LHS and RHS that appear in cancellation arguments.

proof idea

Definition-heavy module with one structural theorem. It introduces a data bundle attaching local Schläfli fields to each tetrahedron of a Triangulation3D, then defines global LHS and RHS as Finset sums of the local contributions. The theorem global_schlaefli_of_local is the standard sum-of-locals argument: if every tetrahedron obeys the single-simplex Schläfli identity, the summed identity holds on the whole complex. No new differential geometry is proved here; the work is bookkeeping and the lift from local to global.

why it matters in Recognition Science

Global Schläfli cancellation is the geometric half of the first-variation theorem for the nonlinear Regge action: at a flat conformal potential the deficits vanish and the summed Schläfli terms cancel, so the first variation is zero. Downstream, ReggeActionFirstVariation records that target and names this module's identities as the required analytic input. ReggeHessian3D needs the same global structure to justify the quadratic Taylor coefficient of the genuine Regge action. Triangulation3DConsistency strengthens the abstract incidence scaffold precisely so that this global cancellation can be stated. In the Recognition geometry stack this is the bridge from the single-tetrahedron Schläfli calculus to triangulation-level variational statements.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)