GaugeEquivalent
plain-language theorem explainer
GaugeEquivalent declares two configurations c1 and c2 gauge equivalent under recognizer r exactly when a recognition automorphism maps one to the other. Researchers formalizing gauge symmetries in recognition geometry cite this to equate physical configurations invisible to the recognizer. The definition is a direct existential quantification over the RecognitionAutomorphism structure with no auxiliary lemmas.
Claim. Two configurations $c_1$ and $c_2$ are gauge equivalent with respect to recognizer $r$ if there exists a bijective recognition-preserving map $T$ such that $T(c_1) = c_2$.
background
Recognition geometry treats symmetries as transformations of configurations that preserve recognizable structure. A recognition-preserving map satisfies R(T(c)) = R(c) for the recognizer R, inducing well-defined maps on the recognition quotient. RecognitionAutomorphism extends this to a bijective map equipped with an inverse satisfying left and right inverse properties, as defined in the upstream structure. The module develops algebraic closure under composition and identity to capture gauge redundancies invisible to the recognizer.
proof idea
This is a direct definition. GaugeEquivalent r c1 c2 holds precisely when the existential quantifier over RecognitionAutomorphism r is witnessed by some T with T.toFun c1 = c2. No lemmas or tactics are invoked; the body is the primitive clause used by all downstream results.
why it matters
The definition supplies the relation whose reflexive, symmetric, and transitive properties are established in gaugeEquivalent_refl, gaugeEquivalent_symm, and gaugeEquivalent_trans. It realizes the module's physical interpretation that gauge symmetries are recognition symmetries producing identical observable events. Within the Recognition Science framework it supplies the symmetry structure required for quotient maps and indistinguishability preservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.