IncidenceConsistent
plain-language theorem explainer
Packages the incidence and local Schläfli data that turn an abstract 3D triangulation into a globally consistent Regge complex: global squared edge lengths, endpoint agreement up to orientation, length matching, surjectivity of the edge-incidence map, and a closed Schläfli identity on every tetrahedron. Geometry and curvature-cost authors cite it as the hypothesis that unlocks global Schläfli cancellation and the Dirichlet bulk zero-mode. It is a structure definition, not a proved theorem.
Claim. For a 3D triangulation $K$, an incidence-consistency witness consists of a global squared-edge map $e \mapsto \ell_e^2$ such that: (i) whenever global edge $e$ sits in tetrahedron $\tau$ as local slot $f$, the two endpoints agree up to orientation; (ii) the local squared length of $f$ equals $\ell_e^2$; (iii) every local edge slot of every tetrahedron is hit by some global edge; (iv) each tetrahedron satisfies the closed tetrahedral Schläfli equation.
background
The module strengthens the bare Triangulation3D scaffold so that local tetrahedral data glue to a single global edge metric and support global Schläfli cancellation. A triangulation here carries vertices, global edges, tetrahedra, an incidence map from (global edge, tetrahedron) to an optional local edge slot, and per-tetrahedron Regge data (squared edge lengths, dihedral data).
Incidence consistency demands that this incidence map respect endpoints up to orientation, that local and global squared lengths coincide on incident pairs, and that every local slot is realized. The final field requires each tetrahedron to obey the closed-form tetrahedral Schläfli identity, so global cancellation can be assembled without a separate caller-supplied Schläfli package.
Upstream geometry supplies concrete incidence maps (e.g. Freudenthal cube edgeInTet) and edge-vertex projections; the continuum bridge identifies Dirichlet edge sums with angle-defect actions, which is why a coherent global edge metric matters for curvature cost.
proof idea
No proof: this is a structure bundling five fields. Inhabitants are built by supplying a global squared-edge function and discharging the four propositional fields, typically by case analysis on a concrete incidence table (as in the Freudenthal cube and two-cube strip witnesses) together with a per-tetrahedron Schläfli lemma already proved in the Schläfli tetrahedron module.
why it matters
This is the standard hypothesis for global Schläfli and curvature-cost results on 3D Regge complexes. Downstream, constant potentials are zero modes of the canonical Dirichlet energy precisely when incidence consistency holds, which feeds the M2B certificate that bulk uniform scaling is a Regge zero mode while the boundary angle-defect quadratic matches $J_{\mathrm{curv}}$. The same hypothesis appears in the T5-to-nonlinear-Regge $J$-cost bridge in the unified forcing chain, linking J-uniqueness (T5) to discrete curvature actions.
Concrete models (Freudenthal cube, two-cube strip, periodic Freudenthal tori) package themselves as incidence-consistent, so global Schläfli and encoded torus constructions inherit the structure rather than re-proving gluing. In the RS geometry stack this is the gate between local tetrahedral identities and continuum-style curvature cost on the phi-ladder side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.