idSymmetry_quotient_action
plain-language theorem explainer
The identity recognition-preserving map induces the identity function on the recognition quotient. Researchers modeling gauge redundancies cite this to confirm that the trivial transformation leaves all equivalence classes of observables fixed. The proof extracts a representative configuration from the quotient class via existence of representatives and concludes by reflexivity.
Claim. Let $T$ be the identity recognition-preserving map on configurations. For any equivalence class $q$ in the recognition quotient $C_R$, the induced map satisfies $T_*(q) = q$.
background
Recognition geometry defines a recognition-preserving map as a transformation $T: C → C$ that satisfies $R(T(c)) = R(c)$ for the recognition function $R$, thereby inducing a well-defined action on the quotient $C_R$ by indistinguishability classes. The module establishes the algebraic structure of such maps, including the identity, composition, and their induced quotient actions, with physical reading as gauge redundancies invisible to the recognizer. Upstream results supply the quotient construction (RecognitionQuotient) and the underlying cost axioms (Composition) that ensure multiplicative consistency of the recognition cost $J$.
proof idea
One-line wrapper that obtains a representative configuration $c$ from the quotient class $q$ by the existence-of-representatives lemma, then applies reflexivity to equate the image under the identity map with the original class.
why it matters
This theorem verifies that the identity element of the symmetry monoid acts trivially on the quotient, completing the basic algebraic structure described in the module doc-comment. It directly supports the gauge-symmetry interpretation in Recognition Science by confirming that trivial transformations preserve all observable classes. No downstream uses are recorded yet; the result closes a foundational verification step in the symmetry algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.