isFinerThan_refl
plain-language theorem explainer
Reflexivity of the refinement relation on recognizers follows directly from the definition of indistinguishability. Researchers applying Zorn's Lemma to the lattice of recognizer-induced setoids in Recognition Geometry cite this when confirming the preorder structure. The proof is a one-line term that returns the input indistinguishability hypothesis unchanged.
Claim. For any recognizer $r : C → E$, $r$ is at least as fine as itself: $∀ c_1, c_2 ∈ C$, Indistinguishable $r$ $c_1$ $c_2$ implies Indistinguishable $r$ $c_1$ $c_2$.
background
Recognition Geometry equips each recognizer with an equivalence relation on configuration space C via the RG3 indistinguishability axiom. The module orders these relations by refinement, with composition serving as the meet operation, and invokes Zorn's Lemma to obtain maximal elements. IsFinerThan encodes the heterogeneous preorder: R₁ is at least as fine as R₂ precisely when the equivalence induced by R₁ is contained in that induced by R₂.
proof idea
The proof is a term-mode identity. It constructs the function that accepts two configurations and an indistinguishability hypothesis under r, then returns that same hypothesis. No lemmas are applied; the term directly inhabits the universal quantifier in the definition of IsFinerThan.
why it matters
Reflexivity completes the preorder properties alongside transitivity, enabling the meet-semilattice structure required for Zorn's Lemma. It is referenced by the zorn_refinement_status definition that summarizes the lattice results. The module cites this as part of the formalization of Theorem 4.1 and Theorem 5.1 on maximal recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.