symmetry_maps_cells
plain-language theorem explainer
Recognition-preserving maps send resolution cells into the resolution cell of the image configuration. Researchers constructing quotient actions or gauge symmetries in recognition geometry cite this to confirm that symmetries descend consistently to equivalence classes. The proof is a short tactic sequence that unfolds the cell definition and applies the preservation of indistinguishability.
Claim. Let $T$ be a recognition-preserving map for recognizer $r$ and let $c$ be a configuration. Then the image $T''$ of the resolution cell of $c$ is contained in the resolution cell of $T(c)$.
background
Recognition geometry equips a recognizer $r$ with events $r.R$ and defines symmetries as maps that leave those events unchanged. The structure RecognitionPreservingMap consists of a function toFun together with the axiom that $r.R$ (toFun $c$) equals $r.R$ $c$ for every configuration. Resolution cells are the level sets of $r.R$, i.e., the sets of configurations that produce identical recognition events. The module develops how such maps induce well-defined actions on the recognition quotient $C_R$, interpreting them as gauge redundancies invisible to the recognizer.
proof idea
The term proof introduces an arbitrary point $x$ in the image, obtains the witnessing preimage $c'$ together with the membership hypothesis, unfolds the definition of ResolutionCell, simplifies the set-membership predicate, and concludes by exact application of the sibling lemma symmetry_preserves_indistinguishable.
why it matters
The result supplies the cell-mapping property required by the downstream construction symmetryQuotientMap, which turns a recognition-preserving map into a well-defined function on the quotient. It therefore closes the step that lets recognition symmetries act on the geometric structure, matching the module's physical reading of gauge transformations as event-preserving redundancies. No open scaffolding remains for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.