module module high

`IndisputableMonolith.RecogGeom.Symmetry`

The Symmetry module defines recognition-preserving maps as transformations that preserve events under the indistinguishability relation. It would be cited when establishing invariance in the recognition quotient. The module supplies core definitions and preservation lemmas that support later integration of the geometry framework.

claimA recognition-preserving map $f: C o C$ satisfies $x \sim y o f(x) \sim f(y)$ where $\sim$ is the indistinguishability relation on the recognition quotient $C_R = C / \sim$.

background

The upstream Quotient module constructs the recognition quotient $C_R = C / \sim$ by collapsing configurations that cannot be told apart by the recognizer. This module builds directly on that construction to introduce symmetries. The central object is the recognition-preserving map, defined as a transformation that preserves events and serves as the fundamental symmetry concept in recognition geometry.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the symmetry definitions that feed into the complete integration of Recognition Geometry provided by the downstream Integration module. It fills the role of establishing the core symmetry concept required for the overall framework summary.

scope and limits

Does not derive physical constants or the forcing chain.
Does not address mass formulas or the alpha band.
Does not perform numerical verification of predictions.

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