canonicalPeriodic_noSelfLoopEdges
plain-language theorem explainer
For side length N>2, the canonical periodic Freudenthal triangulation on the N×N×N torus has no self-loop edges. Anyone deriving the Regge Hessian stencil identity cites this to justify Dirichlet-to-stencil reindexing. The proof rewrites endpoints via the canonical edge-vertex identification and applies the periodic-edge non-equality lemma under the N>2 wraparound bound.
Claim. If $N>2$, then the canonical periodic Freudenthal triangulation of the $N\times N\times N$ torus has no self-loop edges: every edge joins two distinct vertices.
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign: the exact general-$N$ stencil identity for the frozen quadratic Regge energy on the canonical Freudenthal family. The underlying complex is the concrete finite periodic skeleton whose vertices are $(\mathbb{Z}/N)^3$ and whose edges are positive-displacement periodic edges (a base vertex together with one of the seven cube displacements: three axis, three face-diagonal, one body-diagonal).
A self-loop is an edge whose two endpoints coincide. On a periodic lattice that can happen by wraparound when a displacement is a multiple of the period. The seven Freudenthal displacements have components in ${0,1}$, so the side-length hypothesis $N>2$ rules that out. The no-self-loop predicate is the graph-theoretic side condition demanded by the ReggeActionConcrete edge-stencil reindexing that turns graph Dirichlet energy into a sum over distinct endpoint pairs.
proof idea
Short term proof. Fix an edge index $e$ and assume its two endpoints agree under the triangulation edge-vertex map. Rewrite that equality by the sibling identification of canonical edge vertices with the endpoints of the corresponding periodic edge. Transport across the vertex finite-index equivalence, using injectivity of the inverse map, and discharge the goal by the lemma that any positive-displacement periodic edge on side lengths $(N,N,N)$ has distinct endpoints whenever $N>2$.
why it matters
Preflight lemma for the Stage-1 core identity equating the frozen quadratic form of the canonical Regge Hessian on this triangulation to the seven-class nearest-displacement stencil energy $\sum_x\sum_d c_d(u(x+d)-u(x))^2$. Downstream, that identity's derivation chain is: Hessian quadratic equals graph Dirichlet energy; no-self-loop edge-stencil reindexing from ReggeActionConcrete; then periodic-edge / (base, displacement) product reindexing. Without no self-loops the stencil sum is ill-posed (diagonal terms would be dropped or double-counted). The module is scoped partial (pillar-2 path-sum flag stays red), but this fact is axiom-clean and holds for every $N>2$, not only the $N=5$ certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.