pith. sign in
module module high

IndisputableMonolith.RecogGeom.Indistinguishable

show as:
view Lean formalization →

This module defines the indistinguishability equivalence relation on configurations induced by a recognizer, where two configurations are equivalent precisely when they produce the same event. Recognition geometry researchers cite it as the source of the core equivalence used throughout the framework. The module consists of definitions establishing the relation, its setoid, resolution cells, and local resolutions.

claimFor recognizer $R: C o E$, configurations $c_1, c_2 \in C$ satisfy $c_1 \sim_R c_2$ if and only if $R(c_1) = R(c_2)$. The relation $\sim_R$ is an equivalence on $C$, with resolution cells as its fibers and local resolutions as covers by such cells.

background

The upstream Recognizer module defines recognition maps $R: C o E$ that connect configurations to observable events under axiom RG2. The current module builds directly on this by introducing the kernel equivalence of any such map. Its doc-comment states that two configurations are indistinguishable under a recognizer if they produce the same event, calling this the fundamental equivalence relation of recognition geometry. Sibling definitions include the setoid, resolution cells as fibers, and local resolutions as covers.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The indistinguishability relation supplies the equivalence used by the Quotient module to form the recognition quotient $C_R = C/\sim$. It is imported by Dimension for recognition dimension, by Foundations for the three pillars of recognition geometry, by Examples for concrete cases, by Integration for the complete framework, and by ZornRefinement for the refinement lattice under RG3.

scope and limits

used by (6)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)