refl_eEquiv
plain-language theorem explainer
The edge bijection of the identity relabeling of the periodic Freudenthal torus (as a bounded complex at side N) is definitionally the identity equivalence on edges. Anyone checking that the zero lattice translation is the identity automorphism cites this. The proof is pure reflexivity: both sides reduce to the same term.
Claim. For every positive integer $N$, if $K$ is the canonical periodic Freudenthal torus of side $N$ packaged as a bounded complex of edge-cap $7N^3$, then the edge-index bijection of the identity relabeling of $K$ equals the identity equivalence on the edge index set of $K$.
background
This module records path-sum probes only: it attaches the canonical periodic Freudenthal torus to the scoped path-sum state space and checks that lattice translations embed into relabeling automorphisms. It makes no continuum, measure, or path-sum value claims.
A relabeling between two bounded complexes is a triple of bijections on vertex, edge, and tetrahedron index sets that commute with the edge-endpoint incidence map. The identity relabeling is the one whose three components are identity equivalences.
The complex in play is the PROBE C3 packaging: side-$N$ periodic Freudenthal torus written as a BoundedComplex with $nV=N^3$, $nE=7N^3$, $nT=6N^3$, inheriting edge and tet incidence from the canonical periodic triangulation and dropping edge-in-tet slots and per-tet metrics.
proof idea
One-line term proof by rfl. By definition the identity relabeling has edge component equal to the identity equivalence on the edge index type, so the stated equality is definitional.
why it matters
Local helper for PROBE C6 (Aut vacuity / translation embedding). Downstream, translationAut_zero uses it (with the matching vertex and tet projections) to show that the zero element of $\mathbb{Z}_N^3$ maps to the identity relabeling of the Freudenthal image. That identity-at-zero fact is part of the chain that the translation group embeds into Aut, yielding $|\mathrm{Aut}(T_N)|\ge N^3$ and the measure bound $\mu(T_N)\le 1/N^3$. No flag-bearing gravity claim; provenance and landmine check only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.