forced_iff
plain-language theorem explainer
Two states land in the same physical class under the forced quotient exactly when every admissible observable agrees on them. Anyone citing gauge-from-indistinguishability, signature quotients, or objecthood classification uses this biconditional. The proof is the standard Mathlib fact that quotient classes coincide iff the generating setoid relates the representatives.
Claim. For a family $F$ of maps $X\to C$ and states $x,y\in X$, the projections to the physical quotient agree, $\pi_F(x)=\pi_F(y)$, if and only if $x$ and $y$ are observationally equivalent under $F$: $\forall f\in F,\, f(x)=f(y)$.
background
In the Primitive Recognition Calculus, physical identity is not primitive: it is forced by what can be recognized. Given a type of states $X$ and codomain $C$, an observable family $F\subseteq(X\to C)$ induces observational equivalence $\mathrm{ObsEquiv}_F$: $x\sim y$ when every $f\in F$ returns the same value. That relation is packaged as a setoid obsSetoid, and the physical quotient is the corresponding quotient type.
The projection $\pi_F$ sends each state to its class. The module's claim is that this construction is exactly the indistinguishability collapse: it adds no extra identifications and omits none. Upstream, ObsEquiv is the pointwise agreement predicate, and proj is Quotient.mk for that setoid. Downstream headlines treat the same biconditional as the definition of gauge forced by recognition rather than by an a priori group action.
proof idea
One-line term proof: apply Mathlib's Quotient.eq, which states that two quotient classes are equal precisely when the underlying setoid relates the representatives. Here the setoid is observational equivalence under $F$, so $\pi_F(x)=\pi_F(y)$ unfolds directly to $\mathrm{ObsEquiv}_F,x,y$. No custom lemmas are needed beyond the setoid/quotient infrastructure already fixed by obsSetoid and proj.
why it matters
This is the kernel fact for Phase 7 "gauge from indistinguishability." The parent theorem gauge_from_indistinguishability packages it with descent of every observable and injectivity when $F$ separates points. Local corollaries identified_of_obsEquiv and proj_injective_of_separating are one-direction specializations. Downstream, classify_quotient re-exports it into the objecthood registry; signature_forced_quotient_iff identifies the physical quotient with equality of full recognition signatures; projective_state_display instantiates the same collapse for projective observables; and RecognitionCore.forced_quotient_iff surfaces it at the core API.
In Recognition Science terms, quotient is not a native distinction operation: it is forced exactly by the absence of a distinguishing recognition act. That stance feeds the broader forcing chain's treatment of gauge and physical identity without importing external gauge groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.