Triangulation3D
plain-language theorem explainer
A finite 3D Regge triangulation packages vertex, edge, and tetrahedron counts with abstract incidence maps and a nondegenerate squared-edge length tuple on each tet. Anyone building bulk curvature costs, Freudenthal cubes, or periodic tori cites this carrier type. It is a pure data structure: no proof obligations beyond field types.
Claim. A finite 3D Regge triangulation consists of natural numbers $n_V$, $n_E$, $n_T$ together with maps sending each edge to an ordered pair of vertices, each tetrahedron to four vertices, each (edge, tet) pair to an optional local edge slot in $\{0,\ldots,5\}$, and each tetrahedron to a nondegenerate squared-edge 6-tuple.
background
The module supplies the finite incidence scaffold that lifts local tetrahedral identities to arbitrary 3D Regge triangulations. In classical Regge calculus one discretizes a 3-manifold by tetrahedra whose edge lengths determine deficit angles; here the combinatorial skeleton is separated from metric data so global length charts need not be chosen early.
Incidence is encoded abstractly: edgeVerts names the two endpoints of each global edge; tetVerts lists the four vertices of each tet; edgeInTet returns some k when a global edge occupies local slot $k\in{0,\ldots,5}$ inside a given tet, else none. Each tet also carries a NonDegenerateTet, i.e. a squared-edge 6-tuple that realizes a nondegenerate Euclidean tetrahedron.
Concrete models (Freudenthal cube: 8 vertices, 19 edges, 6 tets; two-cube strip; periodic tori) instantiate this same carrier. Upstream edge and tet tables from the Freudenthal modules are the typical field fillers.
proof idea
No proof: this is a structure declaration. The seven fields fix the combinatorial and metric interface. Downstream objects fill the fields by supplying concrete finite maps (as in the Freudenthal cube and two-cube strip constructors) and discharge any later incidence-consistency predicates separately.
why it matters
This is the ambient type for the whole 3D Regge layer. Downstream, the Freudenthal cube and two-cube strip are values of it; periodic Freudenthal tori build canonical triangulations and prove incidence consistency over it. Curvature-cost certificates quantify over it: constant vertex potentials are zero modes of the canonical Dirichlet energy precisely because that quadratic sees only edge differences $\xi_i-\xi_j$, so bulk uniform scale drops out and the boundary angle-defect cost can be matched to $J_{\mathrm{curv}}$. The T5-to-nonlinear-Regge bridge likewise threads through this carrier when lifting J-uniqueness to discrete curvature actions. In the forcing chain it is the geometric stage that lets local tet identities become global statements in $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.