pith. machine review for the scientific record. sign in
def definition def or abbrev high

RecognitionQuotient

show as:
view Lean formalization →

Recognition geometry begins with the quotient space obtained by collapsing configurations that produce identical outputs under a recognizer r : C → E. Researchers constructing charts, atlases, or composition maps on recognition data cite this as the base space C_R. The definition is realized by a direct application of the quotient constructor to the indistinguishability setoid.

claimFor a recognizer $r : C → E$, the recognition quotient $C_R$ is the quotient set $C / ∼_r$, where $c_1 ∼_r c_2$ if and only if $r(c_1) = r(c_2)$.

background

The module constructs the recognition quotient as the space of equivalence classes under indistinguishability. Two configurations are identified precisely when the recognizer maps them to the same event in E. This rests on the upstream indistinguishability setoid, which supplies the equivalence relation and its reflexivity, symmetry, and transitivity properties.

proof idea

One-line wrapper that applies the Quotient constructor to the indistinguishableSetoid induced by the recognizer.

why it matters in Recognition Science

This supplies the base space for atlas and chart constructions in recognition geometry. It is invoked by atlas_covers_quotient to guarantee covering, by chartOnQuotient to descend local coordinates, and by quotientMapLeft and quotientMapRight to project composite quotients. In the Recognition Science framework it enacts the collapse of states that cannot be told apart, consistent with the uniqueness step in the forcing chain.

scope and limits

formal statement (Lean)

  26def RecognitionQuotient {C E : Type*} (r : Recognizer C E) :=

proof body

Definition body.

  27  Quotient (indistinguishableSetoid r)
  28
  29/-- The canonical projection π : C → C_R -/

used by (17)

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

depends on (5)

Lean names referenced from this declaration's body.