is
plain-language theorem explainer
In the incidence-consistent 3D Regge setting, a local incidence or Schläfli identity lifts so the corresponding statement holds on the whole triangulation. Geometers working on global Schläfli cancellation for Regge triangulations would cite it. The supplied extract has an empty proof body and no dependency edges, so the argument shape cannot be recovered from the page data.
Claim. For an incidence-consistent 3D Regge triangulation, the relevant local incidence/Schläfli identity holds globally: edge lengths and local square-edge data agree with a single global edge-length assignment, so the Schläfli contribution cancels on the whole complex rather than only simplex-by-simplex.
background
The module strengthens the abstract 3D triangulation scaffold with incidence and local-Schläfli data aimed at global Schläfli cancellation. In Regge calculus, curvature lives on hinges; the Schläfli identity relates variations of dihedral angles and edge lengths so the action is consistent under subdivision.
Sibling material in the same file introduces incidence-consistency predicates, an incidence geometry bundle, global edge length, and equalities identifying local edge (and squared-edge) data with that global assignment. From those one builds triangulation Schläfli data from incidence or from geometry, and derives global Schläfli statements.
Imports are the 3D Schläfli triangulation scaffold and the tetrahedron-level Schläfli proof. The forcing-chain landmarks (J-cost, $\varphi$, eight-tick, $D=3$) are ambient RS geometry context; this file is the discrete 3D consistency layer on top of that dimension count.
proof idea
The page records an empty proof body, zero depends_on edges, and proof style other. No lemmas or tactics are recoverable from the extract. Treat the declaration as a named claim in the incidence-consistency API whose justification is not visible here; inspect the source module and the sibling equalities (localEdgeLength_eq_globalEdgeLength, localSqEdge_eq_globalSqEdge) and the global_schlaefli_from_incidence constructors for the actual argument.
why it matters
Global Schläfli cancellation is the discrete integrability condition that lets local tetrahedron identities assemble into a well-defined Regge action on a closed 3D complex. The module doc states the goal explicitly: incidence plus local-Schläfli data sufficient for that cancellation.
Downstream use is not listed on this page (used_by_count = 0), but the sibling constructors global_schlaefli_from_incidence and global_schlaefli_from_geometry are the natural consumers: they package incidence-consistent data into triangulation-level Schläfli data. In the broader RS geometry stack this sits under the $D=3$ landmark (T8) as discrete consistency infrastructure, not as a new forcing step.
Open risk: the extract is malformed (signature reads as comment text, claim status other), so the precise proposition may differ from the reading above until the source is checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.