translateEdge
plain-language theorem explainer
Translation by a lattice vector t acts on positive-displacement periodic edges by shifting the base vertex and leaving the seven-class displacement fixed. The result is an equivalence of the edge set of the N×N×N periodic Freudenthal torus. Anyone building Aut(T_N) or checking that Z_N^3 embeds into relabelings cites this. The construction is a three-step equivalence sandwich through the (base, disp) product.
Claim. For $N \ge 1$ and any lattice vector $t \in (\mathbb{Z}/N\mathbb{Z})^3$, there is a bijection of the set of positive-displacement periodic edges that sends an edge with base $b$ and displacement class $d \in \{0,\ldots,6\}$ to the edge with base $b+t$ and the same class $d$.
background
The ambient geometry is the periodic Freudenthal torus: vertices are the cubic lattice $(\mathrm{Fin},N)^3$, and a positive-displacement periodic edge is a pair (base vertex, displacement class in $\mathrm{Fin},7$), one of the seven positive cube directions. The module packages this torus as a path-sum BoundedComplex (Probe C3) and checks that lattice translations embed into its relabeling automorphisms (Probe C6).
periodicEdgeEquivProd identifies each such edge with the product of a vertex and a displacement class, definitionally. translateVertex t is componentwise addition of $t$ on $(\mathrm{Fin},N)^3$, an equivalence with inverse subtraction. Together they give a typed translation on edges that moves only the base.
The module is explicitly non-flag-bearing: it records provenance and an Aut-vacuity landmine check, and makes no continuum or measure claim.
proof idea
One-line equivalence composition. Transport across periodicEdgeEquivProd to the product Vertex × Fin 7, apply Equiv.prodCongr (translateVertex t) (Equiv.refl (Fin 7)) so only the base moves, then transport back by the inverse product equivalence. No case split on the seven displacements is needed.
why it matters
This is the edge half of the typed translation used to build Probe C6. Downstream, translationAut conjugates translateEdge t through the canonical Fin-indexing of edges to obtain an element of Aut(freudenthalBoundedComplex N). The companion lemmas translateEdge_apply, translateEdge_endpoints, translateEdge_trans, and translateEdge_zero feed the proofs that translations form a group homomorphism, fix the identity at $0$, and act compatibly on endpoints.
Those facts yield translationAut_injective, hence autCard_ge_translations ($N^3 \le |\mathrm{Aut}(T_N)|$) and the measure bound $\mu(T_N) \le 1/N^3$. In the Seven Gaps gravity lane this is the concrete check that the translation branch of Aut is non-vacuous on the embedded torus, not a continuum or path-sum evaluation claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.