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 map from configurations to events. Researchers building recognition quotients or dimension theory cite it as the source of the fundamental equivalence. The module supplies the core definitions of the relation, its setoid, resolution cells as fibers, and the distinguishable complement.

claimLet $R: C → E$ be a recognizer. Configurations $x, y ∈ C$ satisfy $x ∼_R y$ iff $R(x) = R(y)$. The relation ∼_R is an equivalence, the resolution cells are its fibers, and distinguishable pairs are those with distinct images under $R$.

background

Recognition geometry starts from a recognizer, a map $R: C → E$ sending configurations to observable events, as supplied by the upstream Recognizer module. This module introduces the induced equivalence: two configurations are indistinguishable precisely when they produce the same event. It equips the configuration space with the corresponding setoid and defines resolution cells as the equivalence classes (fibers of $R$).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the indistinguishability relation required by the recognition quotient $C_R = C/∼$ and by dimension theory. It directly implements the RG3 axiom on indistinguishability and feeds the fundamental theorems in Foundations, the refinement lattice in ZornRefinement, and the concrete examples and integration modules.

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)