idAutomorphism
plain-language theorem explainer
The identity map on configurations supplies the canonical automorphism for any recognizer in recognition geometry. Researchers modeling gauge symmetries cite it to establish reflexivity of equivalence relations on configurations. The definition directly assigns the identity function to both the forward map and its inverse, then confirms event preservation and invertibility by reflexivity.
Claim. Let $r$ be a recognizer on configurations $C$. The identity automorphism is the bijective recognition-preserving map whose action on configurations is the identity function, whose inverse is likewise the identity, and which satisfies the left and right inverse axioms together with event preservation.
background
Recognition geometry treats symmetries as transformations of configurations that leave recognizable events unchanged. A recognition-preserving map $T$ satisfies $R(T(c)) = R(c)$ for recognizer $R$. The automorphism structure extends this by requiring bijectivity: an inverse function obeying left and right inverse properties for every configuration.
proof idea
Direct definition that instantiates the automorphism structure by setting the forward and inverse maps to the identity function and discharging the preservation and invertibility axioms via reflexivity.
why it matters
This supplies the identity element required for the algebraic structure of automorphisms. It is used to prove gauge equivalence is reflexive and to establish that the identity acts as left and right neutral element under composition. Within the framework it realizes the trivial gauge symmetry, matching the interpretation that gauge transformations are precisely those invisible to the recognizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.