PeriodicEdge
plain-language theorem explainer
A periodic edge on the Nx×Ny×Nz cubic torus is a base vertex plus one of seven positive cube displacements (axis, face-diagonal, or space-diagonal steps). It is the typed edge carrier for the scalable Freudenthal torus skeleton. Downstream incidence and Regge first-variation work indexes edges by this type. The companion endpoints map and non-degeneracy proof reduce to modular bit-flip inequalities when each side length exceeds 2.
Claim. For positive integers $N_x,N_y,N_z$, a periodic edge is a pair $(v,d)$ where $v\in\mathbb{Z}/N_x\times\mathbb{Z}/N_y\times\mathbb{Z}/N_z$ is the base vertex and $d\in\{0,\ldots,6\}$ labels one of the seven nonzero positive cube displacements. Its endpoints are $(v,\,v+\delta(d))$, with $\delta(d)\in\{0,1\}^3\setminus\{(0,0,0)\}$. If $N_x,N_y,N_z>2$, the two endpoints are distinct.
background
The module builds a typed periodic model of a Freudenthal triangulation on a 3-torus, without yet encoding a concrete finite mesh into Fin indices. Vertices are the product lattice $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. Bit flips addBit and their product addBits implement wrapping coordinate steps by $0$ or $1$ modulo each side length.
The seven positive displacements (dispBits on Fin 7) are exactly the nonzero vectors in ${0,1}^3$. That matches the one-cube Freudenthal edge set: three axis edges, three face diagonals, and one space diagonal, each taken in the positive orthant so each geometric edge has a unique lower base.
The module goal is the global incidence/edge-slot partition required by the nonlinear Regge first-variation theorem on any finite triangulation that realizes this periodic skeleton.
proof idea
The structure itself is data: base vertex plus Fin 7 displacement, with decidable equality and a finite type instance. Endpoints unpack the displacement bits and apply addBits to the base.
Non-degeneracy (endpoints_ne) is a seven-way fin_cases on the displacement. Each case simplifies endpoints to a single true bit-flip in one or more coordinates and invokes addBit_true_ne_self on a coordinate with side length $>2$, which is the modular fact $(i+1)\bmod N\neq i$ when $N>2$. Multi-bit displacements still force inequality because at least one flipped coordinate differs.
why it matters
Periodic edges are the edge sort for the entire periodic Freudenthal torus. Downstream definitions (canonicalEdgeSlot?, canonicalEdgeInTet, canonicalEdgeVerts, canonicalGlobalSqEdge) treat this type as the global edge identifier and build local edge-in-tetrahedron slot maps from it.
Those maps feed the incidence edge-slot partition that the module promises for any finite encoder into a Triangulation3D. That partition is the geometric input to the nonlinear Regge first-variation theorem on the periodic skeleton. In the broader Recognition geometry stack this is the scalable D=3 cubic/Freudenthal carrier (forcing chain T8), not a one-off mesh.
The remaining open work named in the module doc is a finite encoder from this typed torus into concrete Fin nV, Fin nE, Fin nT indices; the edge type is what that encoder must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.