global_schlaefli_from_geometry
plain-language theorem explainer
On any finite 3D Regge triangulation whose edge incidences are geometrically consistent, the local closed-form tetrahedral Schläfli identities assemble into a global edge-indexed Schläfli identity. Anyone working on discrete curvature cancellation or Regge calculus in Recognition geometry would cite it. The proof is a one-line application of the local-to-global summation lemma after packaging incidence data into triangulation Schläfli data.
Claim. Let $K$ be a finite 3D Regge triangulation with pure incidence geometry (global squared edge lengths compatible with every tetrahedron's local edges). Assume the closed-form local Schläfli identity holds for every nondegenerate tetrahedron. Then for each of the six local edge coordinates $e'$, the global left-hand side (sum over tetrahedra of $\sqrt{\ell_e^2}\,\partial\theta_e/\partial\ell_{e'}$) equals the corresponding global right-hand side.
background
The module strengthens the abstract Triangulation3D scaffold (finite vertex/edge/tetrahedron counts, incidence maps, and nondegenerate squared-edge data on each tet) with the incidence and local-Schläfli ingredients needed for global cancellation.
IncidenceGeometry K is pure geometric consistency: a global squared-edge assignment together with vertex-matching and local-to-global edge-length agreement whenever an abstract edge sits in a tetrahedron. It deliberately omits local Schläfli proofs as fields, once the tetrahedral theorem is available globally.
SchlaefliTetrahedronClosedFormTarget is the finite algebraic core left by the closed-form reduction: every nondegenerate tetrahedron satisfies the six edge-coordinate Schläfli identities. Upstream, globalSchlaefliLHS/RHS sum local dihedral-derivative terms over all tets, and global_schlaefli_of_local states that summing those local identities yields the global finite-triangulation identity.
proof idea
One-line term proof. Build triangulation Schläfli data from the incidence geometry hypothesis and the local closed-form target via triangulationSchlaefliData_of_geometry, then apply global_schlaefli_of_local at the given edge coordinate $e'$. No extra algebraic work: the local-to-global summation lemma does the rest.
why it matters
Closes the incidence-geometry path to global Schläfli cancellation in 3D Regge triangulations: pure incidence plus the local tetrahedral theorem is enough. The module doc frames this as the data needed to construct global Schläfli cancellation; the declaration is the terminal statement of that path in the consistency layer.
No downstream consumers are recorded yet, so it currently stands as an endpoint rather than an intermediate lemma. In the broader Recognition geometry stack it is the natural bridge from the single-tetrahedron closed-form target to mesh-level curvature identities, which sit under the discrete-geometry side of the forcing chain (spatial dimension $D=3$, eight-tick structure). It does not itself touch constants, mass ladders, or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.