gaugeEquivalent_refl
plain-language theorem explainer
Gauge equivalence is reflexive for any configuration c under recognizer r. Researchers formalizing symmetry in recognition geometry cite this as the base case establishing that every configuration is gauge-equivalent to itself. The proof is a one-line term that directly supplies the identity automorphism and applies reflexivity.
Claim. For any configuration $c$, there exists a recognition automorphism $T$ such that $T(c)=c$.
background
Recognition geometry treats symmetries as recognition-preserving maps on configurations $C$ that leave events $R(c)$ unchanged. GaugeEquivalent is the relation holding precisely when some RecognitionAutomorphism $T$ satisfies $T.toFun c_1 = c_2$. The identity automorphism is the canonical example whose toFun is the identity function and whose event-preservation clause is immediate reflexivity.
proof idea
The proof is a term-mode construction that instantiates the existential in GaugeEquivalent by supplying idAutomorphism together with the reflexivity witness rfl.
why it matters
This supplies the reflexive leg of gauge equivalence, enabling the relation to serve as the kernel of the quotient map onto the recognition space $C_R$. It completes the algebraic skeleton (identity, composition, inverses) required for the symmetry structure described in the module. The result sits at the base of the recognition-preserving map hierarchy and supports the physical reading of gauge symmetries as unobservable redundancies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.