conj_refl
plain-language theorem explainer
Conjugating the identity through any type equivalence recovers the identity on the source type. Cited when building relabeling automorphisms of the periodic Freudenthal torus image, especially to show the zero translation is the identity automorphism. Proof is extensionality plus the left-inverse law for equivalences.
Claim. For types $\alpha,\beta$ and any equivalence $E:\alpha\simeq\beta$, the composite $E^{-1}\circ\mathrm{id}_{\beta}\circ E$ equals $\mathrm{id}_{\alpha}$.
background
Module PathSumProbes 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 two cheap structural facts (probes C3 and C6). It claims nothing about measures, limits, or continuum path sums.
Probe C6 checks that the translation group $\mathbb{Z}_N^3$ (additive group of vertices $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$) embeds into the relabeling automorphisms of the torus image. Relabelings are assembled by conjugating incidence data through indexing equivalences on vertices, edges, and tets. The identity relabeling is conjugation of the identity maps, so one needs the elementary fact that conjugating $\mathrm{id}$ through any equivalence recovers $\mathrm{id}$.
The named upstream E symbols in the dependency graph are incidental collisions with the theorem's parameter name; the argument uses only Mathlib Equiv infrastructure.
proof idea
Apply equivalence extensionality. Pointwise, the claim reduces to $E^{-1}(E,x)=x$ for every $x:\alpha$, which is the standard left-inverse identity Equiv.symm_apply_apply. No geometry or path-sum structure enters.
why it matters
Directly feeds translationAut_zero: the zero translation is the identity relabeling of freudenthalBoundedComplex N. That zero-preservation, together with injectivity and additivity of translationAut, is the Aut-vacuity landmine check (probe C6, branch (a): translations embed). Downstream consequences already proved in-module are $|\mathrm{Aut}(T_N)|\ge N^3$ and the measure bound $\mu(T_N)\le 1/N^3$. The lemma itself is pure equivalence algebra; its place in the Recognition gravity stack is as the identity case inside the translation embedding that underwrites those Aut-cardinality and measure inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.