ObsEquiv
plain-language theorem explainer
Two states are observationally equivalent under a family F of observables when every map in F returns the same value on both. This is the kernel relation of the forced physical quotient: anyone citing gauge-from-indistinguishability, forced_iff, or the objecthood registry quotient classifier depends on it. The body is a one-line Prop definition, not a derived theorem.
Claim. Fix types $X$ and $C$ and a family $F$ of maps $X \to C$. States $x, y \in X$ are observationally equivalent under $F$ when $f(x) = f(y)$ for every $f \in F$.
background
In the Primitive Recognition Calculus, physical content is what admissible observables can distinguish. A family $F \subseteq {X \to C}$ is the admitted set of recognition acts (readouts) on a state space $X$ with value type $C$. Two states that no member of $F$ separates are interchangeable for every physical purpose licensed by $F$.
This module builds the forced physical quotient from that relation: the setoid of observational equivalence, the projection onto classes, and the universal property that every $f \in F$ descends. Downstream headlines package the same idea as "gauge from indistinguishability": the quotient is not an extra structure imposed on distinction; it is exactly the collapse of states that no recognition act can tell apart.
(The parameter name $F$ collides with the RS display function $F(Z)=\log(1+Z/\varphi)/\log(\varphi)$ elsewhere in the monolith; here $F$ is only the observable family.)
proof idea
Definition, not a proof. The predicate is the pointwise agreement condition $\forall f \in F,, f,x = f,y$. Reflexivity, symmetry, and transitivity are established separately so the relation can be packaged as a setoid and quotiented.
why it matters
This relation is the mathematical content of "indistinguishability" in Phase 7 of the foundation chain. The parent theorem forced_iff states that the physical projection identifies $x$ and $y$ if and only if observational equivalence holds; identified_of_obsEquiv is the one-direction corollary. The Phase 7 headline gauge_from_indistinguishability packages that biconditional with descent of every observable and injectivity when $F$ separates points.
ObjecthoodRegistry.classify_quotient re-exports the same biconditional as the registry's quotient clause. QuotientExamples specializes it to projective-state display and to the empty/separating extremes (total collapse vs. trivial quotient). Without this predicate there is no precise meaning for "the quotient forced by absence of a distinguishing recognition act."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.