periodicEdgeEquivProd
plain-language theorem explainer
Positive-displacement periodic edges on the cubic torus are identified with pairs (base vertex, one of seven cube displacements). Cardinality and translation constructions on the Freudenthal torus cite this equivalence. The proof is purely definitional: the structure fields are exactly those two components, so both inverse laws reduce to rfl.
Claim. For positive integers $N_x,N_y,N_z$, the set of positive-displacement periodic edges on the $N_x\times N_y\times N_z$ torus is canonically bijective with the product of the vertex set and the seven cube displacement classes: $E_{\mathrm{per}}(N_x,N_y,N_z)\simeq V(N_x,N_y,N_z)\times\{0,\ldots,6\}$.
background
The ambient geometry is the periodic Freudenthal torus: vertices are the finite cubic lattice $V=\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$, and a positive-displacement periodic edge is the structure with a base vertex and a displacement class in $\mathrm{Fin},7$ (the seven positive cube directions). That structure is exactly the data of the pair, which this equivalence records.
The module is Phase 2b lane O of the Seven Gaps gravity work: non-flag-bearing path-sum probes only. It attaches the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex (probe C3) and checks that lattice translations embed into relabeling automorphisms (probe C6). No continuum, measure, or path-sum value is claimed.
Upstream, the edge structure and vertex abbreviation come from PeriodicFreudenthalTorus; the seven-displacement packaging is the combinatorial input later counted and translated.
proof idea
Definitional structure equivalence. The forward map sends an edge to the pair of its base vertex and its displacement class. The inverse rebuilds the edge constructor from that pair. Both left and right inverse identities hold by rfl because the structure fields are definitionally those two components; no lemmas are needed.
why it matters
This equivalence is the bookkeeping hinge for the edge side of the Freudenthal packaging used in the path-sum probes. Downstream, card_periodicEdge rewrites through it and the product card formula to obtain $|E_{\mathrm{per}}(N,N,N)|=7N^3$, which matches the nE field of the bounded complex image. translateEdge conjugates lattice translation on vertices with the identity on displacement classes through the same equivalence, so the translation automorphism action on edges is well-defined and compatible with the Aut-embedding check (probe C6).
In the Seven Gaps gravity lane this keeps the periodic edge set aligned with the canonical triangulation counts while remaining inside the non-flag-bearing probe regime: incidence and count facts only, no measure or continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.