RecognitionPreservingMap
plain-language theorem explainer
Recognition-preserving maps are transformations of configurations that leave the recognizer's event predicate invariant. They form the basic symmetry objects in recognition geometry and are used to build the induced action on the recognition quotient. The declaration introduces this concept directly as a structure consisting of a function and its preservation property.
Claim. Let $r$ be a recognizer on configuration space $C$. A recognition-preserving map is a function $f : C → C$ such that the recognizer's event predicate satisfies $r.R(f(c)) = r.R(c)$ for all $c ∈ C$.
background
Recognition geometry equips a recognizer with a configuration space $C$ and an event predicate $R$. A symmetry is any transformation of $C$ that leaves $R$ unchanged, thereby inducing a well-defined map on the quotient space of indistinguishable configurations. The module develops the algebraic properties of these maps, including composition and identity, which mirror the structure of symmetry groups in physics.
proof idea
The declaration is a structure definition. It packages the function field toFun with the predicate preserves_event that asserts invariance of the recognition predicate under the map. No further lemmas or tactics are required for the definition.
why it matters
This definition anchors the symmetry theory in the module and is referenced by the composition operation, the identity map, and the quotient action theorems. It directly implements the physical interpretation of gauge symmetries as recognition-preserving transformations. Within the Recognition Science framework it supplies the geometric layer needed to quotient out unobservable degrees of freedom before applying the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.