NoSelfLoopEdges
plain-language theorem explainer
A finite 3D Regge triangulation is free of self-loop edges when every edge joins two distinct vertices. Geometry and gravity lemmas cite this hypothesis before reindexing edge-pair weights or assembling periodic Freudenthal stencils. The declaration is a pure Prop definition: it names the condition, it does not prove it for any particular mesh.
Claim. For a finite 3D Regge triangulation $K$, write $\mathrm{edgeVerts}(e)=(v_1,v_2)$ for the ordered endpoints of edge $e$. The no-self-loop predicate holds iff $v_1\neq v_2$ for every edge index $e$.
background
The module isolates the analytic Hessian step for a finite 3D Regge triangulation under a conformal ansatz, packaging the second variation into the existing Hessian data interface.
A Triangulation3D is abstract incidence data: counts of vertices, edges, and tetrahedra, plus maps sending each edge to an ordered pair of vertex indices and each tet to four vertices, together with a nondegenerate squared-edge tuple on every tet. The edge map need not a priori forbid loops; nothing in the structure forces the two components of an edge pair to differ.
Self-loops break ordinary edge-pair bookkeeping. Downstream reindexing of canonical edge-pair weights and periodic stencil targets assume each edge contributes two distinct endpoints, so the condition is carved out as an explicit hypothesis rather than baked into the triangulation type.
proof idea
Definitional, not a proof. The body is the single universal statement that for every edge index the first and second components of the edge-endpoint pair are unequal. No lemmas are applied; consumers unfold or introduce the predicate as a named hypothesis.
why it matters
The predicate is the gate on concrete Regge edge algebra in this module: the theorem that builds the canonical edge-pair weight reindex target takes incidence consistency plus no self-loops and produces the reindex interface used by the Hessian package.
On the gravity side it is discharged for canonical periodic Freudenthal triangulations when each period is larger than 2 (side-length assumptions rule out wraparound fixed points), and it is the hypothesis that turns an encoded periodic torus into a Dirichlet edge-stencil target. Without it, periodic stencil and six-tet cubic Dirichlet instances cannot quote the reindex or stencil equalities.
It is scaffolding hygiene for the concrete Regge action path, not a forcing-chain landmark (T0–T8). It simply keeps mesh combinatorics honest before second-variation identities run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.