idSymmetry_toFun
plain-language theorem explainer
The identity recognition-preserving map acts as the identity function on configurations. Researchers formalizing gauge symmetries in recognition geometry cite this to anchor the trivial case in the symmetry group. The proof is a direct reflexivity check on the definition that sets the map's action to the identity function.
Claim. Let $C$ be the space of configurations and $r$ a recognition structure. The identity recognition-preserving map satisfies $T(c) = c$ for every $c$ in $C$, where $T$ is the function component of the identity symmetry.
background
Recognition geometry defines symmetries as recognition-preserving maps $T: C → C$ such that $R(T(c)) = R(c)$ for all configurations $c$, inducing well-defined maps on the recognition quotient $C_R$. The module establishes that these maps capture gauge-like redundancies invisible to the recognizer, with algebraic structure including composition, identity, and inverses. Upstream, the Identity definition states that comparing a thing with itself costs zero, while the identity event sits at the J-cost minimum where the state equals 1.
proof idea
This is a one-line term-mode proof that applies reflexivity directly to the definition of the identity symmetry, whose function component is set to the identity function id.
why it matters
This declaration supplies the identity element for the algebraic structure of symmetries (composition, identity, inverses) described in the module documentation. It anchors the trivial case in the construction of recognition-preserving maps that model gauge symmetries. No downstream uses are recorded yet, and it does not touch open questions in the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.