projective_state_display
plain-language theorem explainer
Two states share a physical class under the forced quotient by a family of observables exactly when no admitted observable separates them. Workers on the projective-state and gauge-quotient layer of Recognition Science cite this as the display form of the indistinguishability collapse. The proof is a one-line application of the general forced-quotient equivalence.
Claim. For arbitrary state and observable types, and any family $F$ of maps from states to observables, the forced projections of states $x$ and $y$ coincide if and only if $x$ and $y$ are observationally equivalent under $F$: no $f \in F$ separates them.
background
In the Primitive Recognition Calculus, physical classes are obtained by quotienting the raw state space by observational indistinguishability. Given a family $F$ of admissible observables (maps from states to some codomain), two states are observationally equivalent when every $f \in F$ returns the same value on both. The forced projection sends each state to its class in that quotient.
The parent module QuotientSelection packages this construction and proves that the quotient is exactly the indistinguishability collapse: "Two states map to the same physical class iff no admissible observable separates them. The forced quotient adds no identifications beyond indistinguishability and omits none." The present declaration is the same statement, named for the projective-state display setting used by the quotient-examples suite.
Local siblings treat the empty-observable phase collapse and the injective case of a fully separating gauge family; together they illustrate how the forced quotient behaves under extreme choices of $F$.
proof idea
One-line term wrapper: apply the general forced-quotient equivalence from QuotientSelection, which itself is just Quotient.eq for the observational equivalence relation. No extra algebraic work; the projective-state naming is purely presentational specialization of the same biconditional.
why it matters
This is the third leg of the quotient-examples headline: phase with no readable observable collapses, a separating gauge family has trivial quotient, and projective-state display is the quotient theorem specialized to projective observables. Downstream, quotient_examples_headline conjoins those three facts, and the Delta-native strong-closure certificate pulls the same display form into the closed theorem surface for the primitive recognition calculus.
In framework terms it records that physical classes are forced by observables alone: the quotient neither invents nor omits identifications. That is the selection principle behind projective-state displays before any Hilbert or Clifford structure is attached. It does not itself force dimension, the eight-tick octave, or J-uniqueness; those live upstream in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.