classify_observable
plain-language theorem explainer
Every admissible observable on a state space factors through the physical quotient by indistinguishability, so the quotient loses no observable information. Anyone building the objecthood registry or arguing that gauge collapse is observationally faithful will cite this. The proof is a one-line term wrapper around the universal property of the physical quotient.
Claim. For any types $X$ and $C$, any set $F$ of maps $X\to C$, and any $f\in F$, there exists $g$ on the physical quotient of $F$ such that $g(\pi_F(x))=f(x)$ for all $x\in X$, where $\pi_F$ is the projection to physical (gauge) classes.
background
In the Primitive Recognition Calculus, admissible observables are the maps in a fixed family $F\subseteq(X\to C)$. Two states are identified when no member of $F$ separates them; the resulting equivalence is the observation setoid, and the physical quotient is the quotient type by that setoid. The projection $\pi_F$ sends each state to its physical class.
The upstream universal property states that every admissible observable descends: there is a function on physical classes agreeing with the observable on every state, so the quotient loses no observable information. That is exactly the content packaged here under the objecthood-registry label observable.
The local module builds a periodic-table style classification of what counts as an RS object (forced rationals, scale, display, completion, convention, quotient, observable, permitted). This entry records that observables are quotient-faithful.
proof idea
One-line term wrapper: the proof is the lambda that, given $F$, $f$, and membership $f\in F$, returns the existential witness from observable_descends. That upstream lemma constructs the descended map by Quotient.lift of $f$ along the observation setoid (well-defined because setoid-related states agree on every admissible observable) and checks the projection identity by rfl.
why it matters
Inside the objecthood registry this is the formal stamp that the physical quotient is observationally complete: collapsing indistinguishable states does not discard any admissible measurement. That underwrites the claim that the forced quotient is exactly the indistinguishability collapse (no extra identifications, none omitted).
Sibling classifiers cover forced rationals, scale, display values, completions, conventions, and the quotient itself; together they feed the periodic table of objecthood. Even with no direct downstream edges yet, the entry is the registry hook any later argument needs when it treats observables as living on gauge classes rather than raw states.
In the broader Recognition Science foundation this is the measurement-side counterpart of quotient selection: physics is read off the physical quotient, and this theorem says that reading is lossless for every admissible observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.