triangulationSchlaefliData_of_incidence
plain-language theorem explainer
From incidence consistency alone, build the full package of local Schläfli derivative data on every tetrahedron of a finite 3D Regge triangulation. Cited by anyone assembling global Schläfli cancellation or the first variation of the Regge action under conformal length changes. The body is a one-line field constructor: apply the closed-form tetrahedron Schläfli package to each tet via the incidence mixin's local proof.
Claim. Let $K$ be a finite 3D Regge triangulation that is incidence-consistent: local tetrahedral edge slots agree with global edge endpoints up to orientation, squared edge lengths match a global assignment, and every tetrahedron carries a closed-form Schläfli identity. Then there is a canonical package of local Schläfli derivative data on every tetrahedron of $K$, obtained by instantiating the closed-form tetrahedron derivative package on each cell.
background
The ambient object is a finite 3D Regge triangulation: finitely many vertices, edges, and tetrahedra, with abstract incidence maps and a nondegenerate squared-edge 6-tuple on every tet. Incidence consistency strengthens that scaffold. Its first fields force local edge slots inside each tet to match the global edge's endpoints up to orientation and force local squared lengths to equal a single global assignment. Its last field supplies, for every tet, a proof of the closed-form Schläfli equation (dihedral and volume derivatives with respect to edge lengths).
TriangulationSchlaefliData is the global package: one local Schläfli derivative record per tetrahedron. Upstream, once a single nondegenerate tet satisfies the closed-form Schläfli equation, tetraSchlaefliDerivativeData_closedForm builds that tet's derivative package with no caller-supplied tables. The module's purpose is to turn incidence plus those local closed forms into global Schläfli cancellation without hand-fed data.
proof idea
Pure structure construction, not a tactic proof. The single field tetData is defined by sending each tetrahedron index $\tau$ to the closed-form local package on $K$'s $\tau$-th tet, using the incidence hypothesis's local Schläfli proof at $\tau$. No further algebra: the heavy lifting lives in the upstream closed-form tetrahedron constructor.
why it matters
This is the bridge from local closed-form Schläfli to everything global in the 3D Regge scaffold. Immediately downstream, global_schlaefli_from_incidence equates the global Schläfli LHS and RHS by feeding this package into the already-proved local-to-global identity, and nonempty_triangulationSchlaefliData_of_incidence records that the type is inhabited. In the first-variation module it supplies the dihedral derivative tables inside localAngleLengthChainDeriv, which then yields local conformal Schläfli cancellation on each tet (finite-sum algebra plus the local identity). Gravity instances (periodic six-tet cubic Dirichlet) reuse it to pin dihedral derivatives to the Freudenthal closed-form table at flatness. Within RS geometry this is scaffolding for discrete curvature identities that feed continuum limits, not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.