observable_descends
plain-language theorem explainer
Every admissible observable on the raw state space factors through the physical quotient by indistinguishability: there is a well-defined map on gauge classes agreeing with the original observable on every state. Anyone proving that the forced quotient loses no measurable information cites this universal property. The proof is a one-line Quotient.lift using that members of the family are constant on ObsEquiv classes.
Claim. Let $F$ be a family of maps $X\to C$ (admissible observables) and let $f\in F$. Write $Q_F$ for the quotient of $X$ by the relation of $F$-indistinguishability, and $\pi_F:X\to Q_F$ for the canonical projection. Then there exists $g:Q_F\to C$ such that $g(\pi_F(x))=f(x)$ for every $x\in X$.
background
In QuotientSelection the raw carrier is a type $X$ of states and $C$ a codomain of readings. An admissible family $F\subseteq(X\to C)$ induces the relation ObsEquiv: $x\sim_F y$ iff every $f\in F$ satisfies $f(x)=f(y)$. That relation is packaged as the setoid obsSetoid $F$, and PhysicalQuotient $F$ is the corresponding quotient type. The map proj $F$ sends each state to its physical (gauge) class.
The module's forced_iff records that two states land in the same class exactly when they are $F$-indistinguishable: the quotient adds no extra identifications and omits none. The present theorem is the dual half of that story: observables themselves still make sense on classes.
Upstream, proj is just Quotient.mk for obsSetoid, so the universal property of quotients applies once one checks that each $f\in F$ is constant on related pairs.
proof idea
Term-mode construction via Quotient.lift. Because $f\in F$, the defining property of ObsEquiv immediately gives $f(a)=f(b)$ whenever $a\sim_F b$, so $f$ respects the setoid. Lift produces $g:$ PhysicalQuotient $F\to C$; the second component of the refine is the computation rule of lift, which is definitional (rfl) on representatives: $g(\mathrm{proj},F,x)=f,x$.
why it matters
This is the "no information loss" half of Phase 7 gauge-from-indistinguishability. The headline theorem gauge_from_indistinguishability packages three facts: forced_iff (classes = indistinguishability), this descent lemma for every $f\in F$, and injectivity of proj when $F$ separates points. Downstream, ObjecthoodRegistry.classify_observable is a thin re-export used to tag a family as an "observable" registry entry, and RecognitionSignatureGauge.signature_observable_descends specializes the same fact to recognition-coordinate families. Together they justify treating the forced quotient as the physical state space without discarding measurable content: gauge appears only where recognition fails to separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.