conj_trans
plain-language theorem explainer
Conjugation of two self-equivalences through a common indexing equivalence preserves composition: conjugating σ then τ equals conjugating the composite. Cited wherever a group action is packaged by conjugation into relabeling automorphisms (here, torus translations). Proof is pointwise cancellation via Equiv.ext and one apply_symm_apply rewrite.
Claim. Let $E:\alpha\simeq\beta$ and $\sigma,\tau:\beta\simeq\beta$ be equivalences. Writing conjugation as $c_E(\rho):=E^{-1}\circ\rho\circ E$ (Lean `trans` order: apply $E$, then $\rho$, then $E^{-1}$), one has $c_E(\sigma)\circ c_E(\tau)=c_E(\sigma\circ\tau)$ as equivalences $\alpha\simeq\alpha$.
background
The ambient module is Seven Gaps Phase 2b, lane O: path-sum probes C3 and C6. It is explicitly non-flag-bearing. It records cheap honest facts tying the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex, and makes no claim about measures, limits, continuum behavior, or path-sum values.
Probe C6 asks whether the translation group $Z_N^3$ (componentwise mod-$N$ addition on $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$) embeds into the relabeling automorphisms of the torus image. The construction conjugates typed translations through the canonical Fin-indexings that identify abstract vertices with the bounded-complex vertex type. Conjugation $c_E(\rho)=E^{-1}\circ\rho\circ E$ is the change-of-indexing map that turns a $\beta$-automorphism into an $\alpha$-automorphism.
This lemma is pure equivalence algebra: composition of two conjugated maps equals conjugation of the composite. The long depends-on list is ambient import noise (calibration dressings, lattice edge sets, arithmetic embeddings); the proof itself uses only the Equiv API.
proof idea
Reduce equality of equivalences to pointwise equality with Equiv.ext, then introduce an arbitrary $x:\alpha$. Unfolding the two sides yields the goal
$E^{-1}(\tau(E(E^{-1}(\sigma(E,x)))))=E^{-1}(\tau(\sigma(E,x)))$.
One rewrite Equiv.apply_symm_apply cancels the inner $E\circ E^{-1}$ pair on the left; both sides match and the proof closes. No induction, no finiteness, no case split.
why it matters
Sole downstream consumer in-module is translationAut_add, the group-hom law: translation by $t+s$ is the composite relabeling of the two summands. That proof unfolds the vertex equivalences of translationAut, applies this conjugation identity, then finishes with translateVertex_trans.
Together with translationAut_zero and injectivity, the hom law packages $Z_N^3\to\mathrm{Aut}(T_N)$ as a monoid embedding. Documented consequences are the cardinality lower bound $N^3\le|\mathrm{Aut}(T_N)|$ and the crude measure bound $\mu(T_N)\le 1/N^3$. Within Recognition Gravity this is a landmine check (Aut is not vacuous: translations really embed), not a continuum or path-sum evaluation. No T0–T8 forcing step is discharged here; the lemma is infrastructure under probe C6 branch (a).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.