gaugeEquivalent_symm
plain-language theorem explainer
Gauge equivalence of configurations under a recognizer is symmetric. If a recognition automorphism maps c1 to c2 then its inverse maps c2 back to c1. Researchers formalizing gauge symmetries in recognition geometry cite this to confirm the relation behaves as an equivalence. The proof extracts the witnessing automorphism and substitutes its inverse using the left inverse property.
Claim. Let $r$ be a recognizer and let $c_1, c_2$ be configurations. If there exists a recognition automorphism $T$ such that $T(c_1) = c_2$, then there exists a recognition automorphism $T'$ such that $T'(c_2) = c_1$.
background
Recognition geometry treats symmetries as recognition-preserving maps: transformations of configurations that leave events unchanged under the recognizer. GaugeEquivalent holds precisely when such an automorphism exists mapping one configuration to the other. The module develops the algebraic structure of these maps, including inverses, composition, and the induced action on the recognition quotient, with the physical reading that gauge symmetries are exactly the redundancies invisible to recognition.
proof idea
The term proof obtains the witnessing automorphism T from the hypothesis, replaces it by T.inv, and rewrites the target equality using the original mapping together with the left inverse property of T.
why it matters
The result supplies the symmetry leg of gauge equivalence, a prerequisite for treating gauge orbits as equivalence classes and forming the recognition quotient. It directly supports the module's claim that gauge symmetries coincide with recognition symmetries. No downstream uses appear in the current graph, but the property is presupposed by symmetryQuotientMap and related quotient constructions in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.