module module high

`IndisputableMonolith.RecogGeom.Symmetry`

This module defines recognition-preserving maps on the recognition quotient as the fundamental symmetries of recognition geometry. It builds on the indistinguishability quotient from the upstream Quotient module to introduce maps that leave events invariant. Researchers analyzing invariance in geometric physics foundations would cite these definitions when extending to integration or dynamics. The module supplies core definitions plus basic preservation properties with no complex proofs.

claimA map $f: C_R → C_R$ on the recognition quotient $C_R = C/∼$ is recognition-preserving when it preserves events, i.e., $x ∼ y$ implies $f(x) ∼ f(y)$ for the indistinguishability relation $∼$.

background

Recognition Geometry begins with the quotient construction $C_R = C/∼$ from the upstream Quotient module, where $∼$ collapses configurations indistinguishable to the recognizer. This module introduces recognition-preserving maps on $C_R$ as the symmetries that fix events. Sibling definitions include preservation lemmas for indistinguishable and distinguishable pairs plus cell mappings under these maps.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the symmetry definitions that feed the complete integration summary in the downstream Integration module. It establishes the core symmetry concept for the framework, enabling later invariance arguments. The Integration module draws on these to assemble the full Recognition Geometry picture.

scope and limits

Does not construct explicit non-identity examples of such maps.
Does not prove the collection forms a group under composition.
Does not link to continuous or Lie-group symmetries.
Does not address dimension-specific cases beyond the base quotient.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RecogGeom.Integration module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Quotient module_import

declarations in this module (31)

structure RecognitionPreservingMap L44
theorem symmetry_preserves_indistinguishable L59
theorem symmetry_preserves_distinguishable L67
theorem symmetry_maps_cells L75
def symmetryQuotientMap L86
theorem symmetryQuotientMap_mk L92
def idSymmetry L98
theorem idSymmetry_toFun L102
theorem idSymmetry_quotient_action L105
def compSymmetry L113
theorem compSymmetry_toFun L119
theorem compSymmetry_assoc L123
theorem idSymmetry_comp_left L128
theorem idSymmetry_comp_right L133
theorem compSymmetry_quotient_action L138
structure RecognitionAutomorphism L148
def idAutomorphism L172
def compAutomorphism L180
theorem compAutomorphism_assoc_toFun L200
theorem idAutomorphism_comp_left_toFun L206
theorem idAutomorphism_comp_right_toFun L211
theorem compAutomorphism_inv_right_toFun L216
theorem compAutomorphism_inv_left_toFun L222
theorem compAutomorphism_inv_right_eq_id L228
theorem compAutomorphism_inv_left_eq_id L234
def GaugeEquivalent L244
theorem gauge_implies_indistinguishable L248
theorem gaugeEquivalent_refl L254
theorem gaugeEquivalent_symm L258
theorem gaugeEquivalent_trans L266
def symmetry_status L277