IndisputableMonolith.Geometry.Triangulation3DConsistency
Packages strong incidence consistency for finite 3D Regge triangulations: local tetrahedral edge slots match global edge endpoints up to orientation, and the closed-form local Schläfli identity is on hand without caller-supplied data. Anyone assembling global Schläfli cancellation or the concrete Regge action Hessian cites this layer. The module bridges incidence geometry to the tetrahedral Schläfli package and lifts local identities to the full triangulation.
claimA 3D triangulation is incidence-consistent when each tetrahedron's local edge slots agree with a global edge-length assignment up to orientation, and when a closed-form local Schläfli identity is available so the global Schläfli sum holds without external triangulation Schläfli data.
background
In discrete gravity, a finite 3D Regge triangulation assigns edge lengths to a simplicial complex and measures deficit angles at hinges. The local Schläfli identity on each tetrahedron relates variations of dihedral angles to edge-length variations; the global identity is the sum of those local identities over top-dimensional simplices.
Upstream, the tetrahedral package connects explicit Cayley-Menger determinants and dihedral derivatives to a closed-form local Schläfli target ("the hard remaining content is now a single closed-form identity, not an implicit external field"). The triangulation module states that global 3D Schläfli cancellation is exactly that finite sum of local identities.
This module supplies the missing incidence layer: local edge slots must match global edge endpoints up to orientation, and the local closed-form proof must be packaged so global Schläfli can be built without caller-supplied triangulation Schläfli data.
proof idea
Definition-and-lift module, not a single theorem. It introduces incidence geometry and an incidence-consistency predicate whose fields force local tetrahedral edge slots to agree with global endpoints up to orientation, plus the local closed-form Schläfli proof field.
From incidence it constructs triangulation Schläfli data, proves local squared and unsquared edge lengths equal the global assignment, and obtains global Schläfli as the sum of local identities. Parallel constructors start from a full incidence geometry rather than the bare consistency predicate. Non-emptiness of the resulting Schläfli data is recorded so downstream modules need not thread optional packages.
why it matters in Recognition Science
Feeds the concrete Regge action Hessian target: that downstream module "isolates the final analytic Hessian step for a finite 3D Regge triangulation" and turns a concrete action package into the existing Hessian interface. Without incidence-consistent edge matching and a built-in local Schläfli proof, global Schläfli and the second variation under the conformal ansatz cannot be assembled inside the scaffold.
In the Recognition geometry stack this is the glue between closed-form tetrahedral Schläfli and triangulation-level cancellation, clearing the path from local identities to a usable Regge action on finite 3D complexes.
scope and limits
- Does not prove continuum limits or convergence of discrete Regge actions to Einstein-Hilbert.
- Does not treat dimension other than 3 or non-tetrahedral top simplices.
- Does not supply numerical edge lengths, metrics, or curvature spectra.
- Does not derive the Hessian or second variation; that lives downstream.
- Does not address Lorentzian signature or causal structure.
used by (1)
depends on (2)
declarations in this module (11)
-
structure
IncidenceConsistent -
theorem
is -
structure
IncidenceGeometry -
def
globalEdgeLength -
theorem
localSqEdge_eq_globalSqEdge -
theorem
localEdgeLength_eq_globalEdgeLength -
def
triangulationSchlaefliData_of_incidence -
theorem
global_schlaefli_from_incidence -
theorem
nonempty_triangulationSchlaefliData_of_incidence -
def
triangulationSchlaefliData_of_geometry -
theorem
global_schlaefli_from_geometry