periodicEdge_endpoints_eq
plain-language theorem explainer
On the periodic N³ Freudenthal torus, every positive-displacement edge has endpoints definitionally equal to its base vertex paired with that base shifted by its Fin-7 displacement class. Reindexing proofs that turn the canonical Regge edge stencil into the seven-class Freudenthal sum cite this identity. The argument is pure reflexivity: endpoints are defined exactly that way.
Claim. For every positive-displacement periodic edge $e$ on the $N\times N\times N$ torus, the ordered endpoint pair of $e$ equals $(b,\, b+d)$, where $b$ is the base vertex of $e$ and $d\in\{0,\ldots,6\}$ is its cube displacement class (one of the seven positive Freudenthal displacements).
background
This module is Stage 1 of panel-locked Test G (QG full-theory campaign, Phase 2b): it identifies the frozen quadratic form of the canonical Regge Hessian on the periodic Freudenthal triangulation with a seven-class nearest-displacement stencil energy, for every side length $N>2$.
A PeriodicEdge is the geometry package's positive-displacement edge on the $N_x\times N_y\times N_z$ torus: a base vertex together with one of seven cube displacements (three axis, three face-diagonal, one body-diagonal). Its endpoints field is the ordered pair of that base and the base shifted by the displacement. The local helper shiftVertex applies a Fin-7 displacement to a vertex with toroidal wrap.
Spatial dimension is the forced $D=3$ of the Recognition chain (T8), so the lattice is genuinely cubic and the seven positive displacements exhaust the Freudenthal nearest-neighbor classes used downstream.
proof idea
One-line term proof by rfl. The endpoints projection on PeriodicEdge is defined to be exactly (base, shiftVertex N base disp), so the equality is definitional and needs no lemmas beyond the structure fields.
why it matters
This is a tiny but load-bearing reindexing fact in the Stage-1 chain that proves the canonical Regge Hessian quadratic form equals the seven-class Freudenthal stencil $\sum_x\sum_{d\in D} c_d,(u(x+d)-u(x))^2$ with weights $c_d=\sqrt{\ell_d^2}$ read from incidence duals ($\ell^2\in{1,1,1,2,2,2,3}$).
Its sole direct consumer is canonicalEdgeStencil_eq_freudenthalStencil, which rewrites the canonical edge-stencil Dirichlet energy as freudenthalStencilEnergy for every $N$. That identity sits under hessianQuadratic_canonical_eq_freudenthalStencil and the normalized stencil identity $\rho(N)\cdot Q_N(u)=h^3\sum c_d((u(x+d)-u(x))/h)^2$ with $h=1/N$, $\rho(N)=1/N$. Without matching endpoints to (base, shifted base), the product reindexing over edges versus (vertex, displacement) pairs does not typecheck.
Scoped partial: pillar-2 path-sum remains red; this only closes the action-level stencil bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.