classify_quotient
plain-language theorem explainer
Two states land in the same physical class under the observable family F exactly when no member of F separates them. Anyone working the objecthood registry or gauge-quotient layer cites this as the forced-identification criterion. The proof is a one-line term wrapper of the QuotientSelection indistinguishability lemma.
Claim. For any types $X,C$, any family $F$ of maps $X\to C$, and any states $x,y\in X$, the projections of $x$ and $y$ to the physical quotient of $F$ coincide if and only if $x$ and $y$ are observationally equivalent under $F$ (every $f\in F$ satisfies $f(x)=f(y)$).
background
In the Primitive Recognition Calculus, physical content is what admissible observables can distinguish. Given a family $F\subseteq(X\to C)$, two states are observationally equivalent when every $f\in F$ returns the same value on them. The physical quotient is the setoid quotient by that relation; its projection sends each state to its gauge class.
The upstream lemma forced_iff states the exactness of that construction: the quotient adds no identifications beyond indistinguishability and omits none. The present module (ObjecthoodRegistry) classifies how various constructions sit relative to objecthood: forced rationals, scale, display, completion, convention, quotient, observable, and permitted entries in a periodic table of commitments.
Local setting: a registry of RS objects and commitments, with each classify_* theorem pinning one construction to its objecthood status.
proof idea
One-line term wrapper. The proof is the lambda fun F x y => QuotientSelection.forced_iff F x y, which is definitionally the biconditional between equality of projections and observational equivalence. No extra rewriting or case analysis is required; the setoid equality Quotient.eq already supplies the equivalence in the upstream lemma.
why it matters
This entry records that the physical quotient is forced by indistinguishability, not chosen by convention. In the objecthood registry it sits beside the other classify_* results that feed the periodic table of commitments: forced constructions versus displays, completions, and conventions.
Downstream use is not yet wired in this graph (used_by is empty), but the sibling layout makes the role clear: objecthood classification needs a clean statement that the quotient loses no observable information and invents none. That is the gauge principle at the foundation layer, before mass ladders, eight-tick structure, or dimension forcing enter.
It does not itself invoke T5–T8 or the Recognition Composition Law; it is prior scaffolding for what counts as a physical state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.