IndisputableMonolith.Geometry.ReggeTriangulation3D
Defines a finite 3D Regge triangulation: abstract incidence data plus a nondegenerate squared-edge length assignment on every tetrahedron. Geometers working toward the Regge component theorem and global Schläfli cancellation cite this as the ambient combinatorial-metric object. The module is definitional scaffolding over the Cayley–Menger foundation; no deep proofs live here.
claimA finite 3D Regge triangulation consists of abstract incidence data for a triangulation of a 3-manifold (or 3-complex) together with, on each tetrahedron, a 6-tuple of squared edge lengths that is nondegenerate (positive Cayley–Menger volume, valid triangle inequalities on faces).
background
Regge calculus replaces smooth Riemannian geometry by a piecewise-flat simplicial complex whose metric data are edge lengths. In three dimensions the top simplices are tetrahedra; the six squared edge lengths of each tetrahedron determine its geometry via the Cayley–Menger determinant.
The upstream module ReggeRigorousFoundation supplies that polynomial infrastructure and the genuine Regge component identity $M_{ij}=-\mathrm{area}(f_{ij})$. The present module packages the global object those local identities sit on: a finite collection of tetrahedra with incidence relations and a nondegenerate squared-edge assignment on each.
Sibling names indicate the two main exported notions: the triangulation type itself and a local edge-variation structure used when differentiating deficit angles or areas with respect to edge lengths.
proof idea
This is a definition module. It introduces the combinatorial type of a finite 3D triangulation and the metric data (nondegenerate squared-edge tuples per tetrahedron), drawing real-arithmetic primitives from Mathlib and the Cayley–Menger/nondegeneracy apparatus from the rigorous Regge foundation. No substantial theorems are proved here; the content is type-and-structure setup for downstream identities.
why it matters in Recognition Science
Global 3D Schläfli cancellation is the finite sum of local tetrahedral Schläfli identities over top-dimensional simplices. That argument lives in SchlaefliTriangulation3D, which imports this module as its ambient geometry. Without a clean finite triangulation-plus-edges object, one cannot state the sum or justify term-by-term application of the local identities.
In the broader Recognition geometry stack this sits under the Regge component theorem pathway: once $M_{ij}=-\mathrm{area}(f_{ij})$ is available tetrahedron-wise, the triangulation type lets one assemble curvature (angle defects) and variation formulae on a whole complex. It does not itself force $D=3$ (that is T8 in the forcing chain); it assumes the 3D setting in which Regge calculus is classically cleanest.
scope and limits
- Does not prove the Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$.
- Does not establish global Schläfli cancellation; that is downstream.
- Does not treat Lorentzian signature or 4D Regge calculus.
- Does not force spatial dimension $D=3$; the 3D setting is an assumption.
- Does not construct continuum limits or smooth Riemannian metrics.