quotient_examples_headline
plain-language theorem explainer
Three elementary quotient facts are packaged as one headline: with no observables every phase is identified; with a fully separating integer gauge family the quotient is injective (trivial); and in general two states share a projective class exactly when every admitted observable agrees on them. Anyone citing the primitive recognition quotient calculus would point here for the worked examples. The proof is a three-component term that assembles the three sibling lemmas.
Claim. For toy phase states $X=\mathbb{Z}$, the empty observable family collapses every pair: $\mathrm{proj}_{\emptyset}(x)=\mathrm{proj}_{\emptyset}(y)$ for all $x,y$. With the full family of integer-valued maps, $\mathrm{proj}_{\mathrm{univ}}:\mathbb{Z}\to Q$ is injective. In general, for any state type, observation type, and family $F$, one has $\mathrm{proj}_F(x)=\mathrm{proj}_F(y)$ if and only if $x$ and $y$ are observationally equivalent under $F$ (every $f\in F$ agrees on $x$ and $y$).
background
Primitive recognition treats physical identity as a quotient of raw states by observational equivalence. Given a family $F$ of maps $X\to C$, two states are observationally equivalent when every $f\in F$ returns the same value; the projection $\mathrm{proj}_F$ sends each state to its class in that quotient.
The module supplies three toy illustrations. Phase states are just integers. The empty family admits no readable observable, so every pair is equivalent and the quotient is a single point. The universal family of all integer maps separates points, so the quotient map is injective. The third fact is the generic display theorem: equality of projective classes is exactly observational equivalence.
Upstream, ObsEquiv is the pointwise agreement predicate, and the general forced-iff lemma identifies class equality with that predicate. The sibling lemmas discharge the empty-family collapse, the separating-family injectivity, and the generic display respectively.
proof idea
Term-mode packaging of three already-proved siblings. The first conjunct is empty_observable_phase_quotient (empty family forces observational equivalence of every pair, hence equal projections). The second is separating_gauge_family_injective (the identity map is in the universal family, so the family separates integers and the projection is injective). The third is the generic projective_state_display, which is itself a one-line application of the forced-iff lemma relating projection equality to observational equivalence. No new reasoning is introduced; the headline is the conjunction.
why it matters
In the Recognition foundation, physical content is what survives the observational quotient: gauge and unread degrees of freedom are collapsed, while separating observables keep states distinct. This headline records the two extremal regimes (no observables vs fully separating gauges) and the generic display identity that the rest of the quotient calculus relies on.
It sits in PrimitiveRecognitionCalculus as worked examples of quotient selection, not as a forcing-chain step (T0–T8). No downstream theorems currently cite it; its role is didactic and interface-level, making the meaning of proj and ObsEquiv concrete before heavier constructions. It does not touch mass ladders, the eight-tick octave, or the $\alpha$ band; it only clarifies how recognition quotients behave on toy state spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.