idSymmetry
plain-language theorem explainer
The identity function supplies the neutral recognition-preserving map for any recognizer. Researchers establishing the monoid structure of symmetries or verifying gauge equivalence in recognition geometry cite this definition when composing transformations. The construction directly equips the RecognitionPreservingMap structure with the identity function and discharges the event-preservation obligation by reflexivity.
Claim. Let $r$ be a recognizer on configurations $C$. The identity map $id: C → C$ is a recognition-preserving map, i.e., $r.R(id(c)) = r.R(c)$ for every configuration $c$.
background
Recognition geometry defines a recognizer that assigns events to configurations. A recognition-preserving map consists of a function toFun together with the requirement that the recognizer's event assignment remains invariant under toFun. The module treats such maps as the symmetries of the theory, inducing well-defined actions on the recognition quotient.
proof idea
The declaration is a structure instance that sets toFun to the identity function and supplies the single field preserves_event by the lambda expression fun _ => rfl.
why it matters
idSymmetry is the identity element for composition of recognition-preserving maps and is invoked to prove left and right neutrality under compSymmetry as well as the fixed-point property of the quotient action. It corresponds to the trivial gauge symmetry in the physical interpretation and aligns with the identity morphisms supplied by the upstream cost-algebra, arithmetic, and octave constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.