gaugeEquivalent_trans
plain-language theorem explainer
Gauge equivalence of configurations under a fixed recognizer is transitive. Researchers modeling symmetries in recognition geometry cite this to chain transformations when building quotients. The proof extracts the two witnessing automorphisms, composes them, and verifies the composite maps the first configuration to the third by direct substitution.
Claim. Let $r$ be a recognizer on configurations $C$. If there exists a recognition automorphism $T_1$ such that $T_1(c_1)=c_2$ and an automorphism $T_2$ such that $T_2(c_2)=c_3$, then there exists an automorphism $T$ such that $T(c_1)=c_3$.
background
In recognition geometry a symmetry is a recognition-preserving map: a bijection on configurations that leaves the recognizer's event assignment unchanged. Gauge equivalence is the induced relation: two configurations are gauge equivalent when one is the image of the other under such a symmetry. The module equips these symmetries with algebraic structure, including a composition operation that preserves the event-preservation property. The upstream composition theorem states that the composite of two automorphisms is again an automorphism and acts by pointwise function composition.
proof idea
The term proof obtains the two automorphisms witnessing the hypotheses, applies the composition operator to them, then rewrites the action of the composite using the pointwise definition of composition and the two given mapping equations.
why it matters
Transitivity completes the equivalence-relation structure on configurations that is required before the recognition quotient can be formed. It therefore supports the module's main construction of symmetry-induced maps on the quotient and the physical reading of gauge symmetries as redundancies invisible to the recognizer. No downstream theorems are listed, indicating the result is treated as a basic algebraic fact rather than a specialized lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.