identified_of_obsEquiv

In this module the physical quotient is the setoid quotient of a state space $X$ by observational equivalence relative to an admitted family $F$ of maps $X\to C$. Two states are observationally equivalent when every $f\in F$ returns the same value on them; that relation is the setoid, and $\pi_F$ is the canonical projection onto the quotient of classes.

The companion characterization states that $\pi_F(x)=\pi_F(y)$ if and only if no admitted observable distinguishes $x$ from $y$. That biconditional is the local engine: the present lemma is exactly its reverse direction, packaged for citation. The surrounding Phase 7 headline records the intended reading: the quotient is not a native operation of distinction; it is forced by the absence of a distinguishing recognition act.

Downstream examples instantiate the same pattern on concrete state spaces (e.g. phase states with an empty observable family), where every pair is observationally equivalent and therefore collapses under $\pi_F$.

One-line term proof. Apply the reverse half of the forced-iff characterization of the physical quotient: observational equivalence of $x$ and $y$ under $F$ is exactly the hypothesis needed to conclude $\pi_F(x)=\pi_F(y)$. No extra setoid or quotient machinery is unfolded here.

This is the "indistinguishable implies identified" half of the Phase 7 gauge package. The module headline ties three facts together: the forced-iff characterization, descent of every observable to the quotient, and injectivity of the projection when the family separates points. The present lemma is the direction used whenever one already knows observational equivalence and needs equality of classes.

It is consumed directly by the empty-observable phase-quotient example: with $F=\emptyset$, every pair of phase states is observationally equivalent, so the projection collapses the whole space to a point. That example is the extreme case of gauge from indistinguishability.

In the broader Recognition foundation, the move matches the stance that physical identification is forced by missing recognition acts rather than imposed by hand. It sits upstream of any later claim that gauge orbits are exactly the fibers of $\pi_F$.