refl_tEquiv
plain-language theorem explainer
The tetrahedron-index map of the identity relabeling on the side-N Freudenthal bounded complex is definitionally the identity equivalence. Anyone checking that the zero lattice translation is the identity automorphism cites this projection fact. The proof is a one-line reflexivity check against the structure fields of the identity relabeling.
Claim. For every positive integer $N$, if $K_N$ is the periodic Freudenthal complex of side $N$ viewed as a bounded complex, then the tetrahedron-index component of the identity relabeling of $K_N$ equals the identity equivalence on the tetrahedron index set of $K_N$.
background
Lane O of the Seven Gaps path-sum probes attaches the canonical periodic Freudenthal torus at side $N$ to the scoped path-sum state space BoundedComplex, with cap $B = 7N^3$. That packaging (probe C3) preserves vertex, edge, and tet counts and the two incidence maps, and drops edge-in-tet slots and per-tet metrics by shape mismatch.
A relabeling between two bounded complexes is a triple of bijections on vertex, edge, and tetrahedron index sets that commute with the edge-endpoint and tet-corner incidence maps. The identity relabeling is the triple of identity equivalences on those finite index sets. Probe C6 then asks whether the translation group $\mathbb{Z}_N^3$ embeds into the automorphism monoid of the packaged torus; the zero translation must land on that identity relabeling.
proof idea
Term-mode reflexivity. Unfolding the identity relabeling on the Freudenthal bounded complex, its tetrahedron field is definitionally Equiv.refl on the tet index type, so the equality holds by rfl. No lemmas are invoked beyond the structure definition of the identity relabeling.
why it matters
Local helper for probe C6 (Aut vacuity landmine check). Downstream, translationAut_zero uses the three component projections of the identity relabeling (vertex, edge, tet) when proving that the zero element of Vertex N N N maps to the identity relabeling under the translation embedding. That zero-identity fact, together with injectivity and additivity of the translation map, yields $|\mathrm{Aut}(T_N)| \ge N^3$ and the path-sum mass bound $\mu(T_N) \le 1/N^3$. The module itself is non-flag-bearing: it records provenance and the embedding branch only, with no continuum or measure-limit claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.