obsSetoid
plain-language theorem explainer
Packages observational equivalence under a family of observables as a Lean Setoid on the state space. Anyone building the physical quotient (states modulo gauge/indistinguishability) cites this. The body is a three-field structure: relation is pointwise agreement of all observables in F, and equivalence is the reflexivity, symmetry, and transitivity lemmas already proved for that relation.
Claim. For a set $F$ of maps $X\to C$, the relation "$x\sim_F y$ iff $f(x)=f(y)$ for every $f\in F$" is an equivalence relation on $X$, and therefore defines a setoid on $X$.
background
In the Primitive Recognition Calculus, physical content is what admissible observables can distinguish. Two states $x,y\in X$ are observationally equivalent under a family $F\subseteq{X\to C}$ when every $f\in F$ returns the same value: $\forall f\in F,, f(x)=f(y)$. That relation is the in-module predicate packaged here.
A Lean Setoid is exactly an equivalence relation together with proofs of refl/symm/trans. The same pattern appears in the DeltaReal development, where observational equality on protocols is turned into a setoid whose quotient is the display real line. Here the construction is parametric in the observable family $F$, so the quotient can be specialized once $F$ is fixed by the recognition cost or projector data.
Local setting is quotient selection: collapse the raw state space by indistinguishability before talking about forced physical classes or gauge projections.
proof idea
Definitional packaging, not a deep argument. The relation field is set to observational equivalence under $F$. The iseqv triple is filled by the three already-proved lemmas: reflexivity (every $f$ agrees with itself by rfl), symmetry (equality of values is symmetric), and transitivity (equality of values is transitive). No further rewriting or case analysis.
why it matters
This setoid is the carrier for the physically forced quotient: the abbreviation that forms the state space modulo indistinguishability is exactly the quotient by this setoid, and the projection map is Quotient.mk of it. Downstream, that projection is what makes the slogan precise: two states land in the same physical class if and only if no admissible observable separates them; the forced quotient adds no extra identifications and omits none.
In the Recognition foundation this is the formal step that turns "gauge from indistinguishability" into a type. It sits upstream of injectivity-when-separating and of the identification lemmas that connect observational equivalence to forced classes. Parallel to the DeltaReal observational setoid, it is the general $X$-level version used when selecting which quotient the calculus treats as physical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.