global_schlaefli_of_local
plain-language theorem explainer
Summing local tetrahedral Schläfli identities over all top simplices of a finite 3D triangulation yields the global cancellation identity for any fixed edge-variation index. Discrete-gravity and Regge-calculus workers in the Recognition stack cite this when lifting per-tetrahedron closed forms to the whole complex. The proof is a finite double-sum collapse: each local identity vanishes, so both global sides reduce to zero.
Claim. Let $K$ be a finite 3D Regge triangulation and let $D$ supply, on every tetrahedron of $K$, local Schläfli derivative data. Then for every local edge index $e'\in\{0,\ldots,5\}$, the global left-hand side $\sum_\tau\sum_e \sqrt{\ell_e(\tau)^2}\,\partial\theta_e/\partial\ell_{e'}$ equals the corresponding global right-hand side.
background
The module treats the global 3D Schläfli cancellation as the finite sum of local tetrahedral Schläfli identities over top-dimensional simplices. A Triangulation3D is a finite Regge complex: vertex/edge/tet counts, abstract incidence, and a nondegenerate squared-edge 6-tuple on every tetrahedron.
TriangulationSchlaefliData packages, for each tetrahedron $\tau$, a TetraSchlaefliDerivativeData record whose field schlaefli is the local identity: for each variation index $e'$, $\sum_{e=0}^{5}\sqrt{\ell_e^2},\partial\theta_e/\partial\ell_{e'}=0$. The global left-hand side is exactly the double sum of those local summands over all tetrahedra and all six local edges; the global right-hand side is the matching global expression that the local identities force to match.
Spatial dimension $D=3$ is the forced value from the Recognition forcing chain (T8), so the ambient setting is genuinely three-dimensional Regge geometry rather than a formal $n$-complex.
proof idea
Unfold both global sides to their defining double sums. For each tetrahedron $\tau$, invoke the local field `(D.tetData $\tau$).schlaefli $e'$, which states that the inner sum over the six local edges vanishes. Rewrite the double sum with that family of zeros, then simplify: every summand is zero, so both sides are identically zero and therefore equal. No incidence or closed-form hypothesis is used here; the argument is pure finite summation of the packaged local identities.
why it matters
This is the single lifting step from local tetrahedron calculus to the whole complex. Downstream, global_schlaefli_from_geometry applies it after building Schläfli data from pure incidence geometry plus a local closed-form target; global_schlaefli_from_incidence does the same from strong incidence consistency. Both are one-line wrappers around this theorem.
In the Recognition framework the result sits inside the $D=3$ geometry forced by T8: global Schläfli cancellation is the discrete-curvature bookkeeping identity needed before continuum or continuum-limit claims about Regge action stationarity. It does not itself derive the local identity or force dimension; it only aggregates what the local data already certify.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.