indistinguishable_equivalence
plain-language theorem explainer
The theorem shows that indistinguishability under a recognizer is an equivalence relation on the configuration space. Recognition geometers cite it when partitioning configurations into resolution cells via the RG3 axiom. The proof is a term-mode construction that directly supplies the three required fields of the Equivalence structure from the underlying recognizer lemmas.
Claim. For any recognizer $r : C → E$, the relation $∼_r$ on $C$ defined by $c_1 ∼_r c_2$ if and only if $r(c_1) = r(c_2)$ is an equivalence relation.
background
The module establishes Recognition Geometry axiom RG3: given a recognition map $R : C → E$, two configurations are related when they produce identical events. The core definition states that configurations $c_1$ and $c_2$ satisfy $c_1 ~[r] c_2$ precisely when $r.R c_1 = r.R c_2$. This relation is the fundamental equivalence of recognition geometry, with its classes called resolution cells. Upstream setoid instances on logic integers and rationals supply the general pattern for equipping types with equivalence data, but the present result rests directly on the recognizer definition itself.
proof idea
The term-mode proof constructs an Equivalence instance by supplying three fields. Reflexivity is taken from the refl lemma attached to the Indistinguishable definition. Symmetry uses the symm' lemma. Transitivity uses the trans lemma. No additional tactics or reductions are required; the construction simply assembles the three properties already proved for the relation.
why it matters
This result directly enables the indistinguishability setoid definition, which in turn supplies the equivalence classes used throughout the module. It appears in the module status string and the complete Recognition Geometry summary. The theorem therefore closes the RG3 axiom by confirming that the lossy recognition map induces a genuine partition of configuration space into resolution cells, consistent with the eight-tick octave and phi-ladder structures elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.