Recog Geom Indistinguishable

Resolution cells

In Recognition Science, a recognizer is any process that maps a set of configurations to a set of events. The mapping is lossy: two different configurations can produce the same event. The indistinguishability relation captures this loss exactly. Two configurations are indistinguishable under a recognizer when the recognizer assigns them the same event. This is an equivalence relation, meaning it is reflexive, symmetric, and transitive, so it partitions the space of configurations into disjoint classes.

Each equivalence class is a resolution cell: the set of all configurations that map to a single event. A resolution cell is the smallest unit of configuration that the recognizer can tell apart. The recognizer cannot distinguish anything inside a cell; it can only distinguish between cells. The formal development proves that every configuration belongs to exactly one resolution cell, and that the cells cover the entire configuration space. It also proves that two configurations are indistinguishable exactly when their resolution cells are equal.

The recognizer is defined as a structure with a map from configurations to events. The indistinguishability relation is defined directly from this map: c1 and c2 are indistinguishable when the recognizer's outputs are equal. The formal development proves the relation is an equivalence, defines resolution cells as the equivalence classes, and proves they partition the space. It also defines a local resolution: the restriction of resolution cells to a subset of configurations, which covers that subset.

In Recognition Science, this structure establishes the foundational way a recognizer organizes the world. The recognizer's lossy mapping creates a coarse-grained view of configuration space, where the resolution cells are the atoms of that view. This is the starting point for further geometry: the recognizer's inability to distinguish within a cell is the source of its resolution limit. The formal development proves that this limit is structured, not arbitrary: it is always a partition into equivalence classes.

/-- Two configurations are indistinguishable under a recognizer if they
    produce the same event. This is the fundamental equivalence relation
    of recognition geometry. -/
def Indistinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
  r.R c₁ = r.R c₂

/-- Indistinguishability is an equivalence relation -/
theorem indistinguishable_equivalence : Equivalence (Indistinguishable r) where
  refl := Indistinguishable.refl r
  symm := Indistinguishable.symm' r
  trans := Indistinguishable.trans r

/-- The resolution cell of a configuration c is its equivalence class
    under indistinguishability. This is the set of all configurations
    that produce the same event as c. -/
def ResolutionCell {C E : Type*} (r : Recognizer C E) (c : C) : Set C :=
  {c' : C | c' ~[r] c}

/-- Resolution cells partition the configuration space -/
theorem resolutionCells_partition (c : C) :
    ∃! cell : Set C, c ∈ cell ∧ cell = ResolutionCell r c := by
  use ResolutionCell r c
  constructor
  · exact ⟨mem_resolutionCell_self r c, rfl⟩
  · intro cell ⟨_, hcell⟩
    exact hcell

/-- Two configurations have the same resolution cell iff they're indistinguishable -/
theorem resolutionCell_eq_iff {c₁ c₂ : C} :
    ResolutionCell r c₁ = ResolutionCell r c₂ ↔ c₁ ~[r] c₂ := by
  constructor
  · intro h
    have : c₂ ∈ ResolutionCell r c₁ := by
      rw [h]
      exact mem_resolutionCell_self r c₂
    exact (Indistinguishable.symm' r this)
  · intro h
    ext c
    simp [ResolutionCell, Indistinguishable]
    constructor
    · intro hc
      exact Eq.trans hc h
    · intro hc
      exact Eq.trans hc (Eq.symm h)

What this page does not claim

This structure does not define a metric or distance between configurations. This structure does not specify what the recognizer's map is for any particular physical system. This structure does not claim that resolution cells are the same as points in physical space.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/RecogGeom/Indistinguishable.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: