indistinguishable_equivalence
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove existence of distinguishable configurations.
- Does not construct or enumerate explicit resolution cells.
- Does not impose conditions on the event space E beyond the recognizer signature.
- Does not address compatibility with the J-cost or phi-ladder mass formulas.
Lean usage
def mySetoid {C E} (r : Recognizer C E) : Setoid C := { r := Indistinguishable r, iseqv := indistinguishable_equivalence r }formal statement (Lean)
56theorem indistinguishable_equivalence : Equivalence (Indistinguishable r) where
57 refl := Indistinguishable.refl r
proof body
Term-mode proof.
58 symm := Indistinguishable.symm' r
59 trans := Indistinguishable.trans r
60
61/-- The indistinguishability setoid -/