nonempty_triangulationSchlaefliData_of_incidence

The module strengthens the abstract finite 3D Regge scaffold Triangulation3D (vertex/edge/tet counts, edge endpoints, tet vertex maps, and a nondegenerate squared-edge tuple on each tetrahedron) with the incidence and local-Schläfli data needed for global Schläfli cancellation.

Incidence consistency packages a global squared-edge assignment, agreement of local tetrahedral edge slots with global edge endpoints up to orientation, matching of local and global squared lengths, and a closed-form local Schläfli proof on every tetrahedron. That last field is what lets one build global Schläfli without a caller-supplied local data field.

TriangulationSchlaefliData is the package of local Schläfli derivative data on every tetrahedron. The sibling constructor triangulationSchlaefliData_of_incidence builds it by applying the closed-form local theorem tetrahedron-wise from the incidence mixin.

One-line term proof. The sibling constructor already returns a concrete TriangulationSchlaefliData K from any incidence-consistent triangulation. Wrapping that term in angle brackets inhabits Nonempty, so existence follows immediately from the constructive builder.

This is the existence form of the incidence-to-Schläfli bridge in the 3D Regge geometry stack. The module goal is global Schläfli cancellation from pure incidence geometry once the local closed-form Schläfli theorem is available on every tetrahedron; the companion doc notes that incidence then constructs local data with no stored local Schläfli field.

No downstream consumers are wired yet in the graph. The declaration sits beside global_schlaefli_from_incidence and the geometry-flavored twin constructors, closing the Nonempty interface so later global cancellation lemmas can assume data without threading an explicit package. It is geometry scaffolding for Regge-style curvature bookkeeping, not a forcing-chain (T0–T8) step.