obsEquiv_refl
plain-language theorem explainer
Any state is observationally equivalent to itself under every family of observables: every f in F returns the same value on x and x. Anyone building the physical quotient by indistinguishability cites this as the reflexivity leg of the setoid. The proof is a one-line term that applies equality reflexivity pointwise.
Claim. For any set $F$ of maps $X \to C$ and any $x \in X$, observational equivalence holds between $x$ and itself: $\forall f \in F,\, f(x) = f(x)$.
background
In the Primitive Recognition Calculus quotient-selection layer, two states are observationally equivalent under a family $F$ of observables when every $f \in F$ returns the same value on them. Formally, $\mathrm{ObsEquiv}, F, x, y$ means $\forall f \in F,, f(x) = f(y)$. The family $F$ is an arbitrary set of maps $X \to C$; no further structure on $C$ is required beyond equality.
The local goal is to package this relation as a Lean Setoid so that the state space can be quotiented by indistinguishability. That setoid needs the three equivalence laws; reflexivity is the first and simplest of them.
proof idea
One-line term proof. Unfolding observational equivalence, the goal is $\forall f \in F,, f(x) = f(x)$. The term fun _ _ => rfl supplies equality reflexivity for each observable and each membership witness. No lemmas are invoked beyond the definition of the relation.
why it matters
This is the reflexivity witness fed into obsSetoid, which packages observational equivalence as a Setoid via ⟨obsEquiv_refl F, obsEquiv_symm F, obsEquiv_trans F⟩. That setoid defines the physically forced quotient: the state space modulo indistinguishability. Downstream constructions (projection, descent of observables, gauge-from-indistinguishability) all sit on top of this equivalence. In Recognition terms it is pure foundation scaffolding for quotient selection, not a forcing-chain step (T0–T8), but without it the physical quotient cannot be formed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.