gauge_implies_indistinguishable
plain-language theorem explainer
Gauge equivalence between configurations under a recognizer implies they produce identical recognition events. Researchers modeling gauge redundancies in geometric theories would cite this to equate symmetry transformations with observational equivalence. The proof extracts the automorphism from the equivalence hypothesis and applies its event-preservation property in a direct rewrite.
Claim. If configurations $c_1$ and $c_2$ are gauge equivalent under recognizer $r$ (i.e., there exists a recognition automorphism $T$ with $T(c_1)=c_2$), then $c_1$ and $c_2$ are indistinguishable under $r$ (i.e., they yield the same events).
background
Recognition geometry treats symmetries as recognition-preserving maps: automorphisms $T$ of the configuration space $C$ that satisfy $R(T(c))=R(c)$ for the recognition function $R$ associated to recognizer $r$. Gauge equivalence is the relation generated by such maps, capturing transformations invisible to the recognizer. Indistinguishability is the direct equality of events assigned to two configurations. The module develops this as the geometric counterpart of gauge symmetries, where underlying states map to identical observables and induce well-defined actions on the recognition quotient.
proof idea
The term proof destructures the gauge-equivalence hypothesis to obtain the automorphism $T$ together with the equality $T(c_1)=c_2$. It then rewrites the indistinguishability goal by substituting the equality and invoking the event-preservation property of $T$.
why it matters
The result closes the link between gauge equivalence and indistinguishability, confirming that symmetry transformations leave the recognizer's output unchanged. It supports the module's physical reading of gauge symmetries as recognition redundancies and feeds the constructions of symmetry quotient maps and preservation lemmas listed among the module siblings. No open questions are flagged in the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.