triangulationSchlaefliData_of_geometry
plain-language theorem explainer
From pure incidence geometry on a finite 3D Regge triangulation and the global closed-form tetrahedral Schläfli theorem, build local Schläfli derivative data on every tetrahedron with no stored local field. Anyone assembling global Schläfli cancellation from incidence alone cites this constructor. The body is a one-line pointwise application of the closed-form local package.
Claim. Given a finite 3D Regge triangulation $K$, an incidence-geometry witness on $K$ (global squared edge lengths compatible with every tetrahedron), and the closed-form tetrahedral Schläfli theorem (every nondegenerate tetrahedron satisfies the six edge-coordinate closed identities), produce local Schläfli derivative data on each tetrahedron of $K$ by applying the closed-form local package pointwise.
background
The module strengthens abstract finite 3D Regge triangulations with the incidence and local-Schläfli data needed for global Schläfli cancellation. A Triangulation3D carries vertex/edge/tet counts, edge endpoints, tet vertex maps, and a nondegenerate squared-edge tuple on every tetrahedron.
IncidenceGeometry is pure geometric incidence consistency: a global squared-edge assignment together with vertex-matching and local-to-global edge-length equalities, without storing local Schläfli proofs as fields. Once the tetrahedral closed-form theorem is available globally, this is the intended input.
Upstream, SchlaefliTetrahedronClosedFormTarget asserts that every nondegenerate tetrahedron satisfies the six edge-coordinate closed-form Schläfli identities left after the squared-edge algebraic reduction. From any such identity, tetraSchlaefliDerivativeData_closedForm builds the local derivative package (dihedral and volume derivatives) with no caller-supplied data. TriangulationSchlaefliData is simply that package indexed over all tetrahedra of $K$.
proof idea
Definitional constructor, not a proof. The tetData field is the pointwise map $\tau \mapsto$ tetraSchlaefliDerivativeData_closedForm applied to the tetrahedron $K.\mathrm{tet},\tau$ and to the closed-form identity supplied by the global target hypothesis on that tetrahedron. The incidence witness is accepted in the signature (for downstream consumers) but is not used in the body; local data come only from the closed-form theorem.
why it matters
This is the bridge from pure incidence geometry plus the local closed-form theorem to a full triangulation-level Schläfli data bundle. The immediate parent is global_schlaefli_from_geometry, whose doc-comment states: "Pure incidence geometry plus the local theorem gives global Schläfli." That theorem feeds the constructed data into the existing global-from-local cancellation lemma, equating the summed left- and right-hand sides of the global Schläfli identity on each abstract edge coordinate.
In the Recognition geometry stack this closes the path from the finite algebraic core of tetrahedral Schläfli (the closed-form target) to triangulation-wide cancellation without carrying a stored local Schläfli field on the incidence structure. It sits in the 3D Regge / discrete-curvature layer that supports hinge-aware and zero-mode analysis downstream, consistent with the framework's forced $D=3$ spatial setting (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.