RecognitionAutomorphism
plain-language theorem explainer
RecognitionAutomorphism defines a bijective recognition-preserving map on configurations that leaves events invariant under a given recognizer. Physicists formalizing gauge symmetries or recognition geometry invariances cite this structure when building composition and inverse operations. The definition extends the base preserving map by adjoining an explicit inverse function together with the two standard inverse axioms.
Claim. A recognition automorphism for recognizer $r$ is a map $T: C → C$ satisfying $r.R(T(c)) = r.R(c)$ for every configuration $c$, equipped with an inverse function $T^{-1}: C → C$ such that $T^{-1}(T(c)) = c$ and $T(T^{-1}(c)) = c$.
background
Recognition geometry treats symmetries as transformations of configurations that preserve the events recognized by $r$. The sibling structure RecognitionPreservingMap supplies the base data: a function toFun together with the axiom that the recognizer returns the same event after the map is applied. The module places this construction in the setting of gauge-like redundancies, where maps that leave events unchanged induce well-defined actions on the recognition quotient.
proof idea
The structure extends RecognitionPreservingMap by adding the inverse function field and the two inverse axioms. The accompanying lemmas then verify that the inverse preserves events by substituting the right-inverse axiom into the preservation property and obtain the inverse automorphism by swapping the forward and inverse functions while exchanging the two inverse axioms.
why it matters
This definition supplies the algebraic carrier for the groupoid of symmetries used by compAutomorphism and the left/right inverse theorems. It realizes the module's physical reading that gauge transformations are precisely the maps invisible to the recognizer, thereby closing the symmetry structure needed for quotient maps and equivalence relations in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.