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 R: C to E. Recognition geometers cite it when forming quotients or deriving dimension from event equivalence. It is a definition module that introduces the core relation, resolution cells, and the distinguishable complement without proofs.

claimFor recognizer $R: C o E$, configurations satisfy $c_1 \sim_R c_2$ precisely when $R(c_1)=R(c_2)$. The relation partitions $C$ into resolution cells (fibers of $R$), with distinguishable pairs defined by negation of the relation.

background

Recognition geometry begins with the Recognizer module, which introduces axiom RG2: a recognizer is any function $R: C o E$ from configuration space to observable events. The present module supplies the induced equivalence on $C$ that follows directly from this map. It also defines resolution cells as the fibers of $R$ and the complementary distinguishable relation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The indistinguishability relation is the input to the Quotient module, which forms the recognition quotient $C_R = C / \sim_R$. It is also imported by Dimension, Foundations, Integration, Examples, and ZornRefinement to support their theorems on recognition dimension and refinement lattices.

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)