IncidenceGeometry
plain-language theorem explainer
Pure incidence consistency for a 3D triangulation: a global squared-edge chart that agrees with every tetrahedron's local edge lengths, with endpoint matching and full coverage of local edges. Anyone assembling global Schläfli cancellation or incidence-defined dual/hinge weights in 3D Regge calculus cites this bundle. It is a structure definition packing four fields, not a proved identity.
Claim. An incidence geometry on a 3D triangulation $K$ is a global squared-edge map $L^2:E(K)\to\mathbb{R}$ such that: (i) if global edge $e$ appears in tetrahedron $\tau$ as local edge $f$, the endpoints of $e$ match those of $f$ up to order under $\tau$'s vertex chart; (ii) the local squared length of $f$ equals $L^2(e)$; (iii) every local edge of every tetrahedron is hit by some global edge.
background
The module strengthens the abstract 3D triangulation scaffold with the incidence data needed for global Schläfli cancellation. A triangulation here carries a finite set of tetrahedra, global edges and vertices, an edge-in-tet incidence map, and per-tetrahedron squared-edge charts.
Schläfli identities relate edge-length variations to dihedral-angle variations on each tetrahedron. Once a closed-form local Schläfli theorem is available for every tetrahedron, one no longer needs to store local Schläfli proofs as fields; pure geometric incidence plus that global local theorem suffice.
The structure isolates exactly that pure incidence layer: a single global squared-edge chart, vertex-matching of incidences, agreement of local and global squared lengths, and surjectivity of the incidence map onto every local edge.
proof idea
No proof: this is a structure definition. It packages four fields on a fixed 3D triangulation $K$: the global squared-edge chart; the endpoint-matching axiom for every successful edge-in-tet lookup; the equality of local and global squared lengths on those lookups; and the completeness axiom that every local tetrahedron edge is realized by some global edge. Downstream constructors inhabit the structure and then project the fields.
why it matters
This is the preferred input once the tetrahedral Schläfli theorem is global. The constructor that builds triangulation Schläfli data from pure incidence geometry uses it, and the theorem that pure incidence plus the local closed-form target yields global Schläfli cancellation is stated directly over it.
On the gravity side it supplies the incidence-level edge-length chart for edge-pair incidence weights, their symmetry, vertex-pair hinge weights (and nonnegativity/symmetry), and the independent dual-weight package used in the 3D Regge component theorem. That path defines dual/hinge weights from geometry rather than by negating a Regge Hessian coefficient.
In the broader Recognition geometry stack it sits between the bare triangulation scaffold and global curvature identities needed for discrete gravity components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.