translateEdge_zero
plain-language theorem explainer
Translation by the zero lattice vector acts as the identity equivalence on positive-displacement periodic edges of the N×N×N Freudenthal torus. Cited when checking that the discrete translation group embeds into Aut of the packaged bounded complex (PROBE C6 unit law). Proof is equivalence extensionality plus the additive identity on the edge base.
Claim. For every positive integer $N$, if $0$ denotes the zero vertex in $(\mathbb{Z}/N\mathbb{Z})^3$, then translation of periodic edges by $0$ equals the identity equivalence on the set of positive-displacement periodic edges.
background
The ambient module is a non-flag-bearing probe lane: it attaches the canonical periodic Freudenthal torus at side $N$ to the scoped path-sum state space BoundedComplex and records cheap structural facts only. Vertices are triples in $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$ under componentwise mod-$N$ addition. A periodic edge is a pair (base vertex, displacement in $\mathrm{Fin},7$) encoding one of the seven positive cube directions.
PROBE C6 asks whether the translation group $\mathbb{Z}_N^3$ embeds into the relabeling automorphisms of that packaged complex. Translation acts on edges by shifting the base while freezing the displacement index. The zero vector is the group unit, so its edge action must be the identity map before the full automorphism embedding can be stated.
Foundation arithmetic supplies the additive identity $v+0=v$ used on bases; the geometry layer supplies the PeriodicEdge and Vertex carriers.
proof idea
Term/tactic hybrid via equivalence extensionality: reduce to pointwise equality on an arbitrary periodic edge $e$. Unfolding the translated edge produces the structure with base $e.\mathrm{base}+0$ and the same displacement. A single rewrite by the additive identity closes the equality, so both sides are the identity equivalence.
why it matters
Direct input to translationAut_zero, which states that the zero translation is the identity relabeling of the Freudenthal complex packaged as a bounded complex. That unit law, with injectivity and additivity of the translation-to-Aut map, is the embedding half of PROBE C6 (branch (a): translations embed). Documented consequences in the same module are $|\mathrm{Aut}(T_N)|\ge N^3$ and the measure upper bound $\mu(T_N)\le 1/N^3$. The module explicitly drops continuum, measure-limit, and simpliciality claims; this lemma only seals the identity case of the discrete translation action on edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.