TriangulationSchlaefliData

The module treats the classical 3D Schläfli identity on a finite triangulation: the global cancellation is the sum of local tetrahedral identities over top-dimensional simplices. A finite 3D Regge triangulation supplies vertex, edge, and tetrahedron counts, incidence maps, and a nondegenerate squared-edge 6-tuple on every tetrahedron.

Local tetrahedral Schläfli derivative data (from the tetrahedron module) records the first-order response of dihedral angles to edge-length variations that enters the classical Schläfli formula. The present structure simply indexes one such local package by every tetrahedron of $K$.

Downstream, the global left-hand side sums $\sqrt{\ell_e},\partial\theta_e/\partial\ell_{e'}$ over tetrahedra and local edges; the global right-hand side is identically zero in the Euclidean setting.

Definitional structure, not a proved statement. The single field is a dependent function: for each tetrahedron index $\tau : \mathrm{Fin}, n_T$, a value of local tetrahedral Schläfli derivative data on $K$'s $\tau$-th tetrahedron. No tactics, no lemmas, no sorry. Inhabiting instances are built later from incidence consistency or from a closed-form local Schläfli hypothesis.

This is the data spine for the global finite Schläfli theorem in the module. The global left- and right-hand sides are defined over it, and global_schlaefli_of_local states that summing local tetrahedral identities yields the global identity (RHS vanishes).

The consistency module constructs packages from incidence data and from pure incidence geometry once a closed-form local Schläfli target is available, and proves nonemptiness under incidence consistency. In the Recognition geometry stack this is the bookkeeping step that lifts tetrahedron-level Schläfli calculus to a finite 3D complex, the discrete setting underlying Regge-type curvature bookkeeping in $D=3$ (forcing chain T8).