IndisputableMonolith.Geometry.SchlaefliTriangulation3D
Packages local Schläfli derivative data on every tetrahedron of a finite 3D Regge triangulation and lifts the single-tetrahedron identity to a global left/right-hand side. Anyone proving first-variation vanishing or global Schläfli cancellation cites this scaffold. The main theorem is the sum of local identities over the triangulation.
claimOn a finite 3D Regge triangulation $T$, assign to each tetrahedron $\tau$ its local Schläfli derivative data. The global left-hand side $\sum_{\tau} \mathrm{LHS}(\tau)$ equals the global right-hand side $\sum_{\tau} \mathrm{RHS}(\tau)$, obtained by summing the single-tetrahedron Schläfli identity over all tetrahedra of $T$.
background
Regge calculus replaces smooth curvature by deficit angles on a piecewise-flat triangulation. In three dimensions the elementary cell is a tetrahedron; the classical Schläfli identity relates the differential of its volume to edge lengths and dihedral angles.
The upstream single-tetrahedron module pins that local identity (including the volume-squared relation $V^2 = \mathrm{cm}_3/288$) in the notation used by the Regge component theorem. The finite-incidence module supplies the abstract triangulation scaffold: vertices, edges, faces, tetrahedra, and incidence maps needed to sum over cells.
This module sits between those two layers. It attaches local Schläfli derivative data to every tetrahedron and defines the global left- and right-hand sides as the corresponding sums, so that local identities become a single global cancellation statement.
proof idea
Definition-heavy module with one structural theorem. It introduces a data bundle holding, for each tetrahedron, the local Schläfli inputs already proved for a single cell. Global LHS and RHS are defined by Finset summation over the tetrahedron set of the triangulation. The theorem global_schlaefli_of_local is the termwise sum of the local identities: once every tetrahedron satisfies Schläfli, the summed identity holds by linearity of finite sums. No new differential geometry is proved here; the work is bookkeeping and incidence-safe aggregation.
why it matters in Recognition Science
Global Schläfli cancellation is the geometric engine behind the vanishing of the first variation of the nonlinear Regge action at the flat conformal potential. Downstream, ReggeActionFirstVariation records that target and names this module's summed identity as the required input until the full derivative expansion is written out.
ReggeHessian3D consumes the same triangulation-level Schläfli data when building the Hessian interface under the 3D conformal ansatz. Triangulation3DConsistency strengthens the bare incidence scaffold precisely by demanding the local-Schläfli package defined here, so that global cancellation is well-typed.
In the Recognition geometry stack this is the bridge from one-cell calculus to triangulation-scale variational statements used in the discrete gravity sector.
scope and limits
- Does not prove the single-tetrahedron Schläfli identity; that is imported.
- Does not establish vanishing of the Regge first variation; only supplies the summed identity.
- Does not construct the Regge Hessian or its quadratic Taylor coefficient.
- Does not treat continuum limits, 4D triangulations, or Lorentzian signature.
- Does not verify metric realizability or positive volume of the input triangulation.