translationAut_zero
plain-language theorem explainer
Zero translation on the N×N×N periodic cubic lattice acts as the identity relabeling of the embedded Freudenthal bounded complex. Anyone packaging Z_N^3 as a monoid homomorphism into Aut of that complex cites this unit law. The proof extends equality of relabelings componentwise, reducing vertex, edge, and tetrahedron maps via the zero-translation identities and conjugation of the identity.
Claim. For every positive integer $N$, translation by the zero vertex of the periodic cubic lattice $\mathrm{Fin}\,N\times\mathrm{Fin}\,N\times\mathrm{Fin}\,N$ equals the identity relabeling automorphism of the Freudenthal bounded complex of side $N$.
background
Lane O of Seven Gaps Phase 2b records path-sum probes only: no measures, limits, or continuum claims. Probe C6 checks whether lattice translations embed into the relabeling automorphisms of the torus image inside the scoped path-sum state space.
Vertices of the periodic cubic lattice are triples in $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$. The Freudenthal bounded complex packages the canonical periodic triangulation at side $N$ as a BoundedComplex with $nV=N^3$, $nE=7N^3$, $nT=6N^3$. A relabeling is a triple of bijections on vertex, edge, and tetrahedron indices that commute with the incidence maps (edge endpoints and tet corners).
Translation by a lattice vector induces such a relabeling by conjugating the translated vertex/edge/tet maps. The identity relabeling has all three equivalences equal to Equiv.refl, as recorded by the simp facts for the reflection maps.
proof idea
Apply extensionality for relabelings: equality of two relabelings reduces to equality of the three component equivalences (vertices, edges, tets).
On vertices: unfold the translation automorphism's vertex map and the identity's vertex map, rewrite by the fact that translating by zero is the identity on vertices, then by conjugation of the identity, and close by rfl.
Edges and tets follow the same pattern: unfold, apply the corresponding zero-translation identity (translateEdge_zero, translateTet_zero), conjugate the identity, and finish by reflexivity.
why it matters
This is the unit law in the monoid-hom package from $Z_N^3$ into Aut under relabeling composition. The headline probe C6 theorem translations_embed_in_aut packages injectivity, this zero law, and the add-to-composite law as a single existence statement that translations embed.
Downstream, nontriviality of nonzero translations (translationAut_ne_refl) is an immediate corollary: if a nonzero vector mapped to the identity, injectivity plus this zero law would force the vector to be zero. Those facts feed the cardinality lower bound $|\mathrm{Aut}(T_N)|\ge N^3$ and the path-sum mass upper bound $\mu(T_N)\le 1/N^3$.
Within Recognition gravity, this is a landmine check on the discrete torus geometry before any continuum or measure claim: the translation group really sits inside Aut, so Aut is not vacuously trivial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.