module module moderate

`IndisputableMonolith.RecogGeom.ZornRefinement`

This module defines the recognizer setoid from RG3, equating configurations that produce identical events under a recognizer. It introduces the IsFinerThan partial order on recognizers and establishes that composites form infima under this order. These structures supply the equivalence and refinement tools required by the Refinement Theorem in the Composition module.

claimLet $R$ be a recognizer on configuration space $X$. The recognizer setoid is the equivalence relation $x sim_R y$ on $X$ iff $R(x) = R(y)$. The relation $R preceq S$ (IsFinerThan) holds when the partition induced by $R$ refines the partition induced by $S$. For composite recognizers the glb property asserts that the composite is the greatest lower bound in this order.

background

Recognition Geometry RG3 defines indistinguishability: two configurations are related when a recognizer maps them to the same event, so that equivalence classes form resolution cells. The supplied doc-comment states: Recognition is inherently lossy: multiple configurations may give rise to the same event. The equivalence classes are the resolution cells. This module aliases that relation to the recognizer setoid. The Composition module (RG6) develops composite recognizers acting jointly on the same space; its doc-comment notes: Physical measurement does not happen in isolation. Multiple recognizers can act on the same configuration space. This module develops the theory of composite recognizers and proves the fundamental Refinement Theorem. The current module supplies the IsFinerThan ordering and its lattice operations to support that theorem.

proof idea

This is a definition module, no proofs. It declares the setoid alias drawn from the Indistinguishable module, the IsFinerThan predicate, and the basic properties of reflexivity, transitivity, and the glb behavior of composites.

why it matters in Recognition Science

The setoid and ordering primitives defined here feed the Refinement Theorem in the Composition module by furnishing the equivalence relation and partial order needed to compare recognizers. It bridges RG3 indistinguishability with the composite structures of RG6, providing the interface that lets the Refinement Theorem assert that composites refine their factors.

scope and limits

Does not prove the Refinement Theorem itself.
Does not introduce new physical axioms beyond RG3.
Does not compute explicit resolution cells for concrete recognizers.
Does not extend the ordering to continuous or infinite-dimensional spaces.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Composition module_import
IndisputableMonolith.RecogGeom.Indistinguishable module_import

declarations in this module (20)

def recognizerSetoid L39
theorem recognizerSetoid_iff L43
theorem composite_setoid_iff L55
theorem composite_setoid_le_left L62
theorem composite_setoid_le_right L68
theorem composite_setoid_is_inf L80
def IsFinerThan L101
theorem isFinerThan_refl L105
theorem isFinerThan_trans L109
theorem composite_isFinerThan_left L116
theorem composite_isFinerThan_right L121
theorem composite_isFinerThan_glb L127
def IsRecognizerInduced L144
def ChainInfClosed L153
theorem maximal_recognizer_setoid_exists L165
def IsMaximalRecognizer L186
theorem maximal_cells_unsplittable L193
theorem maximal_unique_setoid L205
theorem recognizer_meet_semilattice L224
def zorn_refinement_status L242